Certificate for #6686 ⟨a, b | aab=b, abba=aa⟩

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

Completion settings:

[1] aab=b

Axiom: aab=b.

Defines rule #1.

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

[2] abba=aa

Axiom: abba=aa.

Referenced by [3], [5].

[3] bba=aaa

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

a ab abba

Critical pair: aaa=bba.

Flip LHS and RHS.

Defines rule #2.

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

[4] bbb=b

Overlap of [3] bba=aaa with [1] aab=b:

bb a aab

Critical pair: bbb=aaaab.

Reduce RHS:

[1]aa(aab)
[1]⇒ (aab)
⇒ b

Defines rule #3.

Referenced by [6].

[5] aaaa=aa

Overlap of [3] bba=aaa with [2] abba=aa:

bb a abba

Critical pair: bbaa=aaabba.

Reduce LHS:

[3](bba)a
⇒ aaaa

Reduce RHS:

[1]a(aab)ba
[2]⇒ (abba)
⇒ aa

Defines rule #4.

[6] baaa=ba

Overlap of [4] bbb=b with [3] bba=aaa:

b bb bba

Critical pair: baaa=ba.

Defines rule #5.