Certificate for #5662 ⟨a, b | aabaab=baaab⟩

Back:⟨a, b | aabaab=baaab⟩

Completion settings:

[1] aabaab=baaab

Axiom: aabaab=baaab.

Referenced by [3].

[2] baaab=c

Axiom: baaab=c.

Defines rule #5.

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

[3] aabaab=c

Simplify [1] aabaab=baaab.

Reduce RHS:

[2](baaab)
⇒ c

Defines rule #6.

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

[4] baaac=caaab

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

baaa b baaab

Critical pair: baaac=caaab.

Defines rule #2.

[5] aabc=caab

Overlap of [3] aabaab=c with [3] aabaab=c:

aab aab aabaab

Critical pair: aabc=caab.

Defines rule #3.

[6] aabaac=caaab

Overlap of [3] aabaab=c with [2] baaab=c:

aabaa b baaab

Critical pair: aabaac=caaab.

Defines rule #4.

[7] bac=caab

Overlap of [2] baaab=c with [3] aabaab=c:

ba aab aabaab

Critical pair: bac=caab.

Defines rule #1.