Certificate for #5033 ⟨a, b | aaa=aa, abba=b⟩

Back:⟨a, b | aaa=aa, abba=b⟩

Completion settings:

[1] aaa=aa

Axiom: aaa=aa.

Defines rule #4.

Referenced by [3], [4].

[2] abba=b

Axiom: abba=b.

Referenced by [3], [4], [5], [6], [7], [8].

[3] aab=ab

Overlap of [1] aaa=aa with [2] abba=b:

aa a abba

Critical pair: aab=aabba.

Reduce RHS:

[2]a(abba)
⇒ ab

Referenced by [5].

[4] baa=ba

Overlap of [2] abba=b with [1] aaa=aa:

abb a aaa

Critical pair: abbaa=baa.

Reduce LHS:

[2](abba)a
⇒ ba

Flip LHS and RHS.

Referenced by [8].

[5] ab=b

Overlap of [3] aab=ab with [2] abba=b:

a ab abba

Critical pair: ab=abba.

Reduce RHS:

[2](abba)
⇒ b

Defines rule #1.

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

[6] bba=b

Overlap of [2] abba=b with [5] ab=b:

abba ab

Critical pair: bba=b.

Referenced by [8], [9].

[7] bbb=bb

Overlap of [2] abba=b with [5] ab=b:

abb a ab

Critical pair: abbb=bb.

Reduce LHS:

[5](ab)bb
⇒ bbb

Referenced by [9].

[8] ba=b

Overlap of [2] abba=b with [4] baa=ba:

ab ba baa

Critical pair: abba=ba.

Reduce LHS:

[5](ab)ba
[6]⇒ (bba)
⇒ b

Flip LHS and RHS.

Defines rule #2.

[9] bb=b

Overlap of [7] bbb=bb with [6] bba=b:

b bb bba

Critical pair: bb=bba.

Reduce RHS:

[6](bba)
⇒ b

Defines rule #3.