Certificate for #4800 ⟨a, b | abaabbab=aab⟩

Back:⟨a, b | abaabbab=aab⟩

Completion settings:

[1] abaabbab=aab

Axiom: abaabbab=aab.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #3.

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

[3] abaabbab=c

Simplify [1] abaabbab=aab.

Reduce RHS:

[2](aab)
⇒ c

Referenced by [4].

[4] abcbab=c

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

ab aabbab aab

Critical pair: abcbab=c.

Defines rule #4.

Referenced by [5], [6].

[5] ac=ccbab

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

a ab abcbab

Critical pair: ac=ccbab.

Defines rule #1.

[6] abcbc=ccbab

Overlap of [4] abcbab=c with [4] abcbab=c:

abcb ab abcbab

Critical pair: abcbc=ccbab.

Defines rule #2.