Certificate for #1997 ⟨a, b | aabbabba=ab⟩

Back:⟨a, b | aabbabba=ab⟩

Completion settings:

[1] aabbabba=ab

Axiom: aabbabba=ab.

Referenced by [3].

[2] abbabba=c

Axiom: abbabba=c.

Referenced by [3], [4].

[3] ab=ac

Overlap of [1] aabbabba=ab with [2] abbabba=c:

a abbabba abbabba

Critical pair: ac=ab.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] acbacba=c

Overlap of [2] abbabba=c with [3] ab=ac:

abbabba ab

Critical pair: acbabba=c.

Reduce LHS:

[3]acb(ab)ba
⇒ acbacba

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

[5] cb=cc

Overlap of [4] acbacba=c with [3] ab=ac:

acbacb a ab

Critical pair: acbacbac=cb.

Reduce LHS:

[4](acbacba)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

Referenced by [6], [7].

[6] accc=ccca

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

acb acba acbacba

Critical pair: acbc=ccba.

Reduce LHS:

[5]a(cb)c
⇒ accc

Reduce RHS:

[5]c(cb)a
⇒ ccca

Defines rule #3.

[7] accacca=c

Overlap of [4] acbacba=c with [5] cb=cc:

a cbacba cb

Critical pair: accacba=c.

Reduce LHS:

[5]acca(cb)a
⇒ accacca

Defines rule #4.