Certificate for #5939 ⟨a, b | abbbba=baaab⟩

Back:⟨a, b | abbbba=baaab⟩

Completion settings:

[1] abbbba=baaab

Axiom: abbbba=baaab.

Referenced by [3].

[2] bb=c

Axiom: bb=c.

Defines rule #2.

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

[3] baaab=acca

Overlap of [1] abbbba=baaab with [2] bb=c:

a bbbba bb

Critical pair: acbba=baaab.

Reduce LHS:

[2]ac(bb)a
⇒ acca

Flip LHS and RHS.

Defines rule #4.

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

[4] bc=cb

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

b b bb

Critical pair: bc=cb.

Defines rule #1.

[5] bacca=caaab

Overlap of [2] bb=c with [3] baaab=acca:

b b baaab

Critical pair: bacca=caaab.

Defines rule #5.

[6] baaac=accab

Overlap of [3] baaab=acca with [2] bb=c:

baaa b bb

Critical pair: baaac=accab.

Defines rule #3.

[7] baaaacca=accaaaab

Overlap of [3] baaab=acca with [3] baaab=acca:

baaa b baaab

Critical pair: baaaacca=accaaaab.

Defines rule #6.