Certificate for #2310 ⟨a, b | abaabab=bab⟩

Back:⟨a, b | abaabab=bab⟩

Completion settings:

[1] abaabab=bab

Axiom: abaabab=bab.

Referenced by [3].

[2] bab=c

Axiom: bab=c.

Defines rule #4.

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

[3] abaabab=c

Simplify [1] abaabab=bab.

Reduce RHS:

[2](bab)
⇒ c

Referenced by [4].

[4] abaac=c

Overlap of [3] abaabab=c with [2] bab=c:

abaa bab bab

Critical pair: abaac=c.

Defines rule #3.

Referenced by [6].

[5] bac=cab

Overlap of [2] bab=c with [2] bab=c:

ba b bab

Critical pair: bac=cab.

Defines rule #2.

[6] bc=caac

Overlap of [2] bab=c with [4] abaac=c:

b ab abaac

Critical pair: bc=caac.

Defines rule #1.