Certificate for #4688 ⟨a, b | aabbaaba=aab⟩

Back:⟨a, b | aabbaaba=aab⟩

Completion settings:

[1] aabbaaba=aab

Axiom: aabbaaba=aab.

Referenced by [3].

[2] bbaaba=c

Axiom: bbaaba=c.

Referenced by [3], [4].

[3] aab=aac

Overlap of [1] aabbaaba=aab with [2] bbaaba=c:

aa bbaaba bbaaba

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] bbaaca=c

Overlap of [2] bbaaba=c with [3] aab=aac:

bb aaba aab

Critical pair: bbaaca=c.

Defines rule #4.

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

[5] aacbaaca=aac

Overlap of [3] aab=aac with [4] bbaaca=c:

aa b bbaaca

Critical pair: aac=aacbaaca.

Flip LHS and RHS.

Referenced by [10].

[6] cab=cac

Overlap of [4] bbaaca=c with [3] aab=aac:

bbaac a aab

Critical pair: bbaacaac=cab.

Reduce LHS:

[4](bbaaca)ac
⇒ cac

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8].

[7] cb=cc

Overlap of [4] bbaaca=c with [6] cab=cac:

bbaa ca cab

Critical pair: bbaacac=cb.

Reduce LHS:

[4](bbaaca)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

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

[8] caccaaca=cac

Overlap of [6] cab=cac with [4] bbaaca=c:

ca b bbaaca

Critical pair: cac=cacbaaca.

Reduce RHS:

[7]ca(cb)aaca
⇒ caccaaca

Flip LHS and RHS.

Defines rule #7.

[9] cccaaca=cc

Overlap of [7] cb=cc with [4] bbaaca=c:

c b bbaaca

Critical pair: cc=ccbaaca.

Reduce RHS:

[7]c(cb)aaca
⇒ cccaaca

Flip LHS and RHS.

Defines rule #5.

[10] aaccaaca=aac

Simplify [5] aacbaaca=aac.

Reduce LHS:

[7]aa(cb)aaca
⇒ aaccaaca

Defines rule #6.