Certificate for #5550 ⟨a, b | aaabaa=baaab⟩

Back:⟨a, b | aaabaa=baaab⟩

Completion settings:

[1] aaabaa=baaab

Axiom: aaabaa=baaab.

Referenced by [4].

[2] aa=c

Axiom: aa=c.

Defines rule #1.

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

[3] ab=d

Axiom: ab=d.

Defines rule #2.

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

[4] aaabaa=bcd

Simplify [1] aaabaa=baaab.

Reduce RHS:

[2]b(aa)ab
[3]⇒ bc(ab)
⇒ bcd

Referenced by [5].

[5] bcd=cdc

Overlap of [4] aaabaa=bcd with [2] aa=c:

aaabaa aa

Critical pair: cabaa=bcd.

Reduce LHS:

[3]c(ab)aa
[2]⇒ cd(aa)
⇒ cdc

Flip LHS and RHS.

Defines rule #5.

Referenced by [8], [9].

[6] ac=ca

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

a a aa

Critical pair: ac=ca.

Defines rule #3.

Referenced by [8].

[7] ad=cb

Overlap of [2] aa=c with [3] ab=d:

a a ab

Critical pair: ad=cb.

Defines rule #4.

Referenced by [8].

[8] ccbc=dcd

Overlap of [3] ab=d with [5] bcd=cdc:

a b bcd

Critical pair: acdc=dcd.

Reduce LHS:

[6](ac)dc
[7]⇒ c(ad)c
⇒ ccbc

Defines rule #6.

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

[9] cccdc=dcdd

Overlap of [8] ccbc=dcd with [5] bcd=cdc:

cc bc bcd

Critical pair: cccdc=dcdd.

Defines rule #7.

Referenced by [11].

[10] ccbdcd=dcdcbc

Overlap of [8] ccbc=dcd with [8] ccbc=dcd:

ccb c ccbc

Critical pair: ccbdcd=dcdcbc.

Defines rule #8.

[11] cccddcd=dcddcbc

Overlap of [9] cccdc=dcdd with [8] ccbc=dcd:

cccd c ccbc

Critical pair: cccddcd=dcddcbc.

Defines rule #9.