Certificate for #2220 ⟨a, b | bb=aa, aaab=a⟩

Back:⟨a, b | bb=aa, aaab=a⟩

Completion settings:

[1] bb=aa

Axiom: bb=aa.

Defines rule #2.

Referenced by [3], [4], [7].

[2] aaab=a

Axiom: aaab=a.

Defines rule #3.

Referenced by [4], [5].

[3] baa=aab

Overlap of [1] bb=aa with [1] bb=aa:

b b bb

Critical pair: baa=aab.

Referenced by [5], [7].

[4] aaaaa=ab

Overlap of [2] aaab=a with [1] bb=aa:

aaa b bb

Critical pair: aaaaa=ab.

Defines rule #4.

Referenced by [6], [7].

[5] aabab=ba

Overlap of [3] baa=aab with [2] aaab=a:

b aa aaab

Critical pair: ba=aabab.

Flip LHS and RHS.

Referenced by [7].

[6] aba=aab

Overlap of [4] aaaaa=ab with [4] aaaaa=ab:

a aaaa aaaaa

Critical pair: aab=aba.

Flip LHS and RHS.

Referenced by [7].

[7] ba=ab

Overlap of [3] baa=aab with [6] aba=aab:

ba a aba

Critical pair: baaab=aabba.

Reduce LHS:

[3](baa)ab
[5]⇒ (aabab)
⇒ ba

Reduce RHS:

[1]aa(bb)a
[4]⇒ (aaaaa)
⇒ ab

Defines rule #1.