Certificate for #4788 ⟨a, b | abaabaab=bab⟩

Back:⟨a, b | abaabaab=bab⟩

Completion settings:

[1] abaabaab=bab

Axiom: abaabaab=bab.

Referenced by [3].

[2] ab=c

Axiom: ab=c.

Defines rule #4.

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

[3] abaabaab=bc

Simplify [1] abaabaab=bab.

Reduce RHS:

[2]b(ab)
⇒ bc

Referenced by [4].

[4] bc=cacac

Overlap of [3] abaabaab=bc with [2] ab=c:

abaabaab ab

Critical pair: caabaab=bc.

Reduce LHS:

[2]ca(ab)aab
[2]⇒ caca(ab)
⇒ cacac

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] acacac=cc

Overlap of [2] ab=c with [4] bc=cacac:

a b bc

Critical pair: acacac=cc.

Defines rule #2.

Referenced by [6].

[6] accc=ccac

Overlap of [5] acacac=cc with [5] acacac=cc:

ac acac acacac

Critical pair: accc=ccac.

Defines rule #1.