Certificate for #6746 ⟨a, b | aba=a, abba=ab⟩

Back:⟨a, b | aba=a, abba=ab⟩

Completion settings:

[1] aba=a

Axiom: aba=a.

Defines rule #3.

Referenced by [5].

[2] abba=ab

Axiom: abba=ab.

Referenced by [4].

[3] abb=c

Axiom: abb=c.

Defines rule #5.

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

[4] ca=ab

Overlap of [2] abba=ab with [3] abb=c:

abba abb

Critical pair: ca=ab.

Defines rule #1.

Referenced by [6].

[5] abc=c

Overlap of [1] aba=a with [3] abb=c:

ab a abb

Critical pair: abc=abb.

Reduce RHS:

[3](abb)
⇒ c

Defines rule #4.

[6] cb=cc

Overlap of [4] ca=ab with [3] abb=c:

c a abb

Critical pair: cc=abbb.

Reduce RHS:

[3](abb)b
⇒ cb

Flip LHS and RHS.

Defines rule #2.