Certificate for #1204 ⟨a, b | aabaa=baab⟩

Back:⟨a, b | aabaa=baab⟩

Completion settings:

[1] aabaa=baab

Axiom: aabaa=baab.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #1.

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

[3] cb=d

Axiom: cb=d.

Defines rule #4.

Referenced by [4], [5], [7], [8], [10].

[4] aabaa=bd

Simplify [1] aabaa=baab.

Reduce RHS:

[2]b(aa)b
[3]⇒ b(cb)
⇒ bd

Referenced by [5].

[5] bd=dc

Overlap of [4] aabaa=bd with [2] aa=c:

aabaa aa

Critical pair: cbaa=bd.

Reduce LHS:

[3](cb)aa
[2]⇒ d(aa)
⇒ dc

Flip LHS and RHS.

Defines rule #2.

Referenced by [7].

[6] ca=ac

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

a a aa

Critical pair: ac=ca.

Flip LHS and RHS.

Defines rule #3.

Referenced by [9].

[7] cdc=dd

Overlap of [3] cb=d with [5] bd=dc:

c b bd

Critical pair: cdc=dd.

Defines rule #6.

Referenced by [8], [9].

[8] cdd=ddb

Overlap of [7] cdc=dd with [3] cb=d:

cd c cb

Critical pair: cdd=ddb.

Defines rule #5.

[9] cdac=dda

Overlap of [7] cdc=dd with [6] ca=ac:

cd c ca

Critical pair: cdac=dda.

Defines rule #8.

Referenced by [10].

[10] cdad=ddab

Overlap of [9] cdac=dda with [3] cb=d:

cda c cb

Critical pair: cdad=ddab.

Defines rule #7.