Certificate for #4784 ⟨a, b | abaabaab=aab⟩

Back:⟨a, b | abaabaab=aab⟩

Completion settings:

[1] abaabaab=aab

Axiom: abaabaab=aab.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #3.

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

[3] abaabaab=c

Simplify [1] abaabaab=aab.

Reduce RHS:

[2](aab)
⇒ c

Referenced by [4].

[4] abcc=c

Overlap of [3] abaabaab=c with [2] aab=c:

ab aabaab aab

Critical pair: abcaab=c.

Reduce LHS:

[2]abc(aab)
⇒ abcc

Defines rule #2.

Referenced by [5].

[5] ac=ccc

Overlap of [2] aab=c with [4] abcc=c:

a ab abcc

Critical pair: ac=ccc.

Defines rule #1.