Certificate for #555 ⟨a, b | abbba=bab⟩

Back:⟨a, b | abbba=bab⟩

Completion settings:

[1] abbba=bab

Axiom: abbba=bab.

Referenced by [5].

[2] ab=c

Axiom: ab=c.

Defines rule #1.

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

[3] cb=d

Axiom: cb=d.

Defines rule #2.

Referenced by [6], [7], [8], [11].

[4] db=e

Axiom: db=e.

Defines rule #3.

Referenced by [6], [8], [9], [12].

[5] abbba=bc

Simplify [1] abbba=bab.

Reduce RHS:

[2]b(ab)
⇒ bc

Referenced by [6].

[6] ea=bc

Overlap of [5] abbba=bc with [2] ab=c:

abbba ab

Critical pair: cbba=bc.

Reduce LHS:

[3](cb)ba
[4]⇒ (db)a
⇒ ea

Defines rule #4.

Referenced by [7].

[7] ec=bd

Overlap of [6] ea=bc with [2] ab=c:

e a ab

Critical pair: ec=bcb.

Reduce RHS:

[3]b(cb)
⇒ bd

Defines rule #5.

Referenced by [8].

[8] ed=be

Overlap of [7] ec=bd with [3] cb=d:

e c cb

Critical pair: ed=bdb.

Reduce RHS:

[4]b(db)
⇒ be

Defines rule #6.

Referenced by [9].

[9] beb=ee

Overlap of [8] ed=be with [4] db=e:

e d db

Critical pair: ee=beb.

Flip LHS and RHS.

Defines rule #7.

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

[10] ceb=aee

Overlap of [2] ab=c with [9] beb=ee:

a b beb

Critical pair: aee=ceb.

Flip LHS and RHS.

Defines rule #8.

[11] deb=cee

Overlap of [3] cb=d with [9] beb=ee:

c b beb

Critical pair: cee=deb.

Flip LHS and RHS.

Defines rule #9.

[12] eeb=dee

Overlap of [4] db=e with [9] beb=ee:

d b beb

Critical pair: dee=eeb.

Flip LHS and RHS.

Defines rule #10.