Certificate for #6664 ⟨a, b | aab=b, aaaa=ba⟩

Back:⟨a, b | aab=b, aaaa=ba⟩

Completion settings:

[1] aab=b

Axiom: aab=b.

Referenced by [3], [5], [6].

[2] aaaa=ba

Axiom: aaaa=ba.

Defines rule #4.

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

[3] bab=b

Overlap of [2] aaaa=ba with [1] aab=b:

aa aa aab

Critical pair: aab=bab.

Reduce LHS:

[1](aab)
⇒ b

Flip LHS and RHS.

Referenced by [5], [6].

[4] aba=baa

Overlap of [2] aaaa=ba with [2] aaaa=ba:

a aaa aaaa

Critical pair: aba=baa.

Referenced by [5], [7].

[5] ab=bb

Overlap of [4] aba=baa with [3] bab=b:

a ba bab

Critical pair: ab=baab.

Reduce RHS:

[1]b(aab)
⇒ bb

Defines rule #1.

Referenced by [6], [7].

[6] bbb=b

Overlap of [2] aaaa=ba with [5] ab=bb:

aaa a ab

Critical pair: aaabb=bab.

Reduce LHS:

[1]a(aab)b
[5]⇒ (ab)b
⇒ bbb

Reduce RHS:

[3](bab)
⇒ b

Defines rule #2.

[7] baa=bba

Overlap of [4] aba=baa with [5] ab=bb:

aba ab

Critical pair: bba=baa.

Flip LHS and RHS.

Defines rule #3.