Certificate for #5943 ⟨a, b | abbbba=bbabb⟩

Back:⟨a, b | abbbba=bbabb⟩

Completion settings:

[1] abbbba=bbabb

Axiom: abbbba=bbabb.

Referenced by [5].

[2] bb=c

Axiom: bb=c.

Defines rule #3.

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

[3] ac=d

Axiom: ac=d.

Defines rule #1.

Referenced by [5], [6], [8], [10], [13].

[4] dc=e

Axiom: dc=e.

Defines rule #4.

Referenced by [6], [8], [9], [11], [14].

[5] abbbba=cd

Simplify [1] abbbba=bbabb.

Reduce RHS:

[2](bb)abb
[2]⇒ ca(bb)
[3]⇒ c(ac)
⇒ cd

Referenced by [6].

[6] ea=cd

Overlap of [5] abbbba=cd with [2] bb=c:

a bbbba bb

Critical pair: acbba=cd.

Reduce LHS:

[3](ac)bba
[2]⇒ d(bb)a
[4]⇒ (dc)a
⇒ ea

Defines rule #5.

Referenced by [8].

[7] bc=cb

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

b b bb

Critical pair: bc=cb.

Defines rule #2.

Referenced by [12].

[8] ed=ce

Overlap of [6] ea=cd with [3] ac=d:

e a ac

Critical pair: ed=cdc.

Reduce RHS:

[4]c(dc)
⇒ ce

Defines rule #6.

Referenced by [9].

[9] cec=ee

Overlap of [8] ed=ce with [4] dc=e:

e d dc

Critical pair: ee=cec.

Flip LHS and RHS.

Defines rule #7.

Referenced by [10], [11], [12].

[10] dec=aee

Overlap of [3] ac=d with [9] cec=ee:

a c cec

Critical pair: aee=dec.

Flip LHS and RHS.

Defines rule #8.

[11] eec=dee

Overlap of [4] dc=e with [9] cec=ee:

d c cec

Critical pair: dee=eec.

Flip LHS and RHS.

Defines rule #9.

[12] cbec=bee

Overlap of [7] bc=cb with [9] cec=ee:

b c cec

Critical pair: bee=cbec.

Flip LHS and RHS.

Defines rule #10.

Referenced by [13], [14].

[13] dbec=abee

Overlap of [3] ac=d with [12] cbec=bee:

a c cbec

Critical pair: abee=dbec.

Flip LHS and RHS.

Defines rule #11.

[14] ebec=dbee

Overlap of [4] dc=e with [12] cbec=bee:

d c cbec

Critical pair: dbee=ebec.

Flip LHS and RHS.

Defines rule #12.