Certificate for #2168 ⟨a, b | aaababa=aab⟩

Back:⟨a, b | aaababa=aab⟩

Completion settings:

[1] aaababa=aab

Axiom: aaababa=aab.

Referenced by [3].

[2] aabab=c

Axiom: aabab=c.

Referenced by [3], [4].

[3] aab=aca

Overlap of [1] aaababa=aab with [2] aabab=c:

a aababa aabab

Critical pair: aca=aab.

Flip LHS and RHS.

Defines rule #4.

Referenced by [4], [6].

[4] acaca=c

Overlap of [2] aabab=c with [3] aab=aca:

aabab aab

Critical pair: acaab=c.

Reduce LHS:

[3]ac(aab)
⇒ acaca

Defines rule #2.

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

[5] acc=cca

Overlap of [4] acaca=c with [4] acaca=c:

ac aca acaca

Critical pair: acc=cca.

Defines rule #1.

Referenced by [7].

[6] cab=cca

Overlap of [4] acaca=c with [3] aab=aca:

acac a aab

Critical pair: acacaca=cab.

Reduce LHS:

[4](acaca)ca
⇒ cca

Flip LHS and RHS.

Defines rule #5.

Referenced by [7].

[7] cb=ccacaa

Overlap of [4] acaca=c with [6] cab=cca:

aca ca cab

Critical pair: acacca=cb.

Reduce LHS:

[5]ac(acc)a
[5]⇒ (acc)caa
⇒ ccacaa

Flip LHS and RHS.

Defines rule #3.