Certificate for #2483 ⟨a, b | aabaab=abaa⟩

Back:⟨a, b | aabaab=abaa⟩

Completion settings:

[1] aabaab=abaa

Axiom: aabaab=abaa.

Referenced by [3].

[2] aba=c

Axiom: aba=c.

Defines rule #1.

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

[3] aabaab=ca

Simplify [1] aabaab=abaa.

Reduce RHS:

[2](aba)a
⇒ ca

Referenced by [4].

[4] acab=ca

Overlap of [3] aabaab=ca with [2] aba=c:

a abaab aba

Critical pair: acab=ca.

Defines rule #4.

Referenced by [6], [7].

[5] cba=abc

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

ab a aba

Critical pair: abc=cba.

Flip LHS and RHS.

Defines rule #2.

[6] ccab=abca

Overlap of [2] aba=c with [4] acab=ca:

ab a acab

Critical pair: abca=ccab.

Flip LHS and RHS.

Defines rule #5.

[7] caa=acc

Overlap of [4] acab=ca with [2] aba=c:

ac ab aba

Critical pair: acc=caa.

Flip LHS and RHS.

Defines rule #3.