Certificate for #6347 ⟨a, b | aab=a, abbba=b⟩

Back:⟨a, b | aab=a, abbba=b⟩

Completion settings:

[1] aab=a

Axiom: aab=a.

Defines rule #2.

Referenced by [3], [4].

[2] abbba=b

Axiom: abbba=b.

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

[3] abba=ab

Overlap of [1] aab=a with [2] abbba=b:

a ab abbba

Critical pair: ab=abba.

Flip LHS and RHS.

Referenced by [6], [8].

[4] bab=b

Overlap of [2] abbba=b with [1] aab=a:

abbb a aab

Critical pair: abbba=bab.

Reduce LHS:

[2](abbba)
⇒ b

Flip LHS and RHS.

Referenced by [5], [6].

[5] abbb=bb

Overlap of [2] abbba=b with [4] bab=b:

abb ba bab

Critical pair: abbb=bb.

Referenced by [7].

[6] bba=b

Overlap of [4] bab=b with [3] abba=ab:

b ab abba

Critical pair: bab=bba.

Reduce LHS:

[4](bab)
⇒ b

Flip LHS and RHS.

Referenced by [7].

[7] abb=b

Overlap of [5] abbb=bb with [6] bba=b:

ab bb bba

Critical pair: abb=bba.

Reduce RHS:

[6](bba)
⇒ b

Defines rule #3.

Referenced by [8].

[8] ba=ab

Overlap of [3] abba=ab with [7] abb=b:

abba abb

Critical pair: ba=ab.

Defines rule #1.