Certificate for #13054 ⟨a, b | baa=aab, abba=a⟩

Completion settings:

Auxiliary generators:
1. c = aabbbbb
Reduction order:
- Left-to-right shortlex with a < c < b

[1] baa=aab

Axiom: baa=aab.

Referenced by [4], [5], [6], [9], [12], [14].

[2] abba=a

Axiom: abba=a.

Defines rule #8.

Referenced by [4], [5].

[3] aabbbbb=c

Axiom: aabbbbb=c.

Referenced by [6], [7], [8], [10], [13].

[4] aabbba=aab

Overlap of [1] baa=aab with [2] abba=a:

ba a abba

Critical pair: baa=aabbba.

Reduce LHS:

[1]	(baa)
	⇒ aab

Flip LHS and RHS.

Referenced by [15].

[5] aaabb=aa

Overlap of [2] abba=a with [1] baa=aab:

ab ba baa

Critical pair: abaab=aa.

Reduce LHS:

[1]	a(baa)b
	⇒ aaabb

Referenced by [7], [11], [17].

[6] bc=cb

Overlap of [1] baa=aab with [3] aabbbbb=c:

b aa aabbbbb

Critical pair: bc=aabbbbbb.

Reduce RHS:

[3]	(aabbbbb)b
	⇒ cb

Referenced by [8], [23].

[7] aabbb=ac

Overlap of [5] aaabb=aa with [3] aabbbbb=c:

a aabb aabbbbb

Critical pair: ac=aabbb.

Flip LHS and RHS.

Referenced by [8], [9], [10], [11].

[8] accbb=cc

Overlap of [3] aabbbbb=c with [6] bc=cb:

aabbbb b bc

Critical pair: aabbbbcb=cc.

Reduce LHS:

[7]	(aabbb)bcb
[6]	⇒ ac(bc)b
	⇒ accbb

Referenced by [12], [13], [18].

[9] bac=acb

Overlap of [1] baa=aab with [7] aabbb=ac:

b aa aabbb

Critical pair: bac=aabbbb.

Reduce RHS:

[7]	(aabbb)b
	⇒ acb

Referenced by [12], [19].

[10] acbb=c

Overlap of [3] aabbbbb=c with [7] aabbb=ac:

aabbbbb aabbb

Critical pair: acbb=c.

Referenced by [12].

[11] aab=aac

Overlap of [5] aaabb=aa with [7] aabbb=ac:

a aabb aabbb

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [12], [13], [14], [15], [16], [17].

[12] acb=acc

Overlap of [1] baa=aab with [10] acbb=c:

ba a acbb

Critical pair: bac=aabcbb.

Reduce LHS:

[9]	(bac)
	⇒ acb

Reduce RHS:

[11]	(aab)cbb
[8]	⇒ a(accbb)
	⇒ acc

Referenced by [13], [16], [17], [19].

[13] accb=c

Overlap of [3] aabbbbb=c with [11] aab=aac:

aabbbbb aab

Critical pair: aacbbbb=c.

Reduce LHS:

[12]	a(acb)bbb
[8]	⇒ a(accbb)b
	⇒ accb

Referenced by [16], [18], [20].

[14] baa=aac

Simplify [1] baa=aab.

Reduce RHS:

[11]	(aab)
	⇒ aac

Defines rule #5.

Referenced by [21], [22].

[15] aabbba=aac

Simplify [4] aabbba=aab.

Reduce RHS:

[11]	(aab)
	⇒ aac

Referenced by [16].

[16] aca=aac

Overlap of [15] aabbba=aac with [11] aab=aac:

aabbba aab

Critical pair: aacbba=aac.

Reduce LHS:

[12]	a(acb)ba
[13]	⇒ a(accb)a
	⇒ aca

Referenced by [21].

[17] aaacc=aa

Overlap of [5] aaabb=aa with [11] aab=aac:

a aabb aab

Critical pair: aaacb=aa.

Reduce LHS:

[12]	aa(acb)
	⇒ aaacc

Defines rule #9.

[18] cb=cc

Overlap of [8] accbb=cc with [13] accb=c:

accbb accb

Critical pair: cb=cc.

Defines rule #2.

Referenced by [20], [23].

[19] bac=acc

Simplify [9] bac=acb.

Reduce RHS:

[12]	(acb)
	⇒ acc

Defines rule #6.

Referenced by [21], [22].

[20] accc=c

Overlap of [13] accb=c with [18] cb=cc:

ac cb cb

Critical pair: accc=c.

Defines rule #7.

Referenced by [22].

[21] acca=aacc

Overlap of [19] bac=acc with [16] aca=aac:

b ac aca

Critical pair: baac=acca.

Reduce LHS:

[14]	(baa)c
	⇒ aacc

Flip LHS and RHS.

Referenced by [22].

[22] ca=ac

Overlap of [19] bac=acc with [21] acca=aacc:

b ac acca

Critical pair: baacc=accca.

Reduce LHS:

[14]	(baa)cc
[20]	⇒ a(accc)
	⇒ ac

Reduce RHS:

[20]	(accc)a
	⇒ ca

Flip LHS and RHS.

Defines rule #1.

[23] bc=cc

Simplify [6] bc=cb.

Reduce RHS:

[18]	(cb)
	⇒ cc

Defines rule #3.