Certificate for #25201 ⟨a, b | aa=a, abbab=abb⟩

Back:⟨a, b | aa=a, abbab=abb⟩

Completion settings:

[1] aa=a

Axiom: aa=a.

Defines rule #1.

Referenced by [6].

[2] abbab=abb

Axiom: abbab=abb.

Referenced by [4].

[3] abb=c

Axiom: abb=c.

Defines rule #4.

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

[4] abbab=c

Simplify [2] abbab=abb.

Reduce RHS:

[3](abb)
⇒ c

Referenced by [5].

[5] cab=c

Overlap of [4] abbab=c with [3] abb=c:

abbab abb

Critical pair: cab=c.

Defines rule #5.

Referenced by [7].

[6] ac=c

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

a a abb

Critical pair: ac=abb.

Reduce RHS:

[3](abb)
⇒ c

Defines rule #2.

[7] cb=cc

Overlap of [5] cab=c with [3] abb=c:

c ab abb

Critical pair: cc=cb.

Flip LHS and RHS.

Defines rule #3.