Certificate for #4755 ⟨a, b | abaaaaab=aba⟩

Back:⟨a, b | abaaaaab=aba⟩

Completion settings:

[1] abaaaaab=aba

Axiom: abaaaaab=aba.

Referenced by [3].

[2] abaaaa=c

Axiom: abaaaa=c.

Referenced by [3], [4].

[3] aba=cab

Overlap of [1] abaaaaab=aba with [2] abaaaa=c:

abaaaaab abaaaa

Critical pair: cab=aba.

Flip LHS and RHS.

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

[4] ccccab=c

Overlap of [2] abaaaa=c with [3] aba=cab:

abaaaa aba

Critical pair: cabaaa=c.

Reduce LHS:

[3]c(aba)aa
[3]⇒ cc(aba)a
[3]⇒ ccc(aba)
⇒ ccccab

Referenced by [6], [9].

[5] cabba=abcab

Overlap of [3] aba=cab with [3] aba=cab:

ab a aba

Critical pair: abcab=cabba.

Flip LHS and RHS.

Referenced by [7].

[6] ca=cc

Overlap of [4] ccccab=c with [3] aba=cab:

cccc ab aba

Critical pair: cccccab=ca.

Reduce LHS:

[4]c(ccccab)
⇒ cc

Flip LHS and RHS.

Defines rule #2.

Referenced by [7], [8], [9], [10].

[7] ccbba=abccb

Simplify [5] cabba=abcab.

Reduce LHS:

[6](ca)bba
⇒ ccbba

Reduce RHS:

[6]ab(ca)b
⇒ abccb

Defines rule #4.

Referenced by [10].

[8] aba=ccb

Simplify [3] aba=cab.

Reduce RHS:

[6](ca)b
⇒ ccb

Defines rule #5.

[9] cccccb=c

Overlap of [4] ccccab=c with [6] ca=cc:

ccc cab ca

Critical pair: cccccb=c.

Defines rule #1.

Referenced by [10].

[10] cba=ccccbccb

Overlap of [9] cccccb=c with [7] ccbba=abccb:

ccc ccb ccbba

Critical pair: cccabccb=cba.

Reduce LHS:

[6]cc(ca)bccb
⇒ ccccbccb

Flip LHS and RHS.

Defines rule #3.