Certificate for #4273 ⟨a, b | abaabbaab=ba⟩

Back:⟨a, b | abaabbaab=ba⟩

Completion settings:

[1] abaabbaab=ba

Axiom: abaabbaab=ba.

Referenced by [3].

[2] baa=c

Axiom: baa=c.

Referenced by [3], [4].

[3] ba=acbcb

Overlap of [1] abaabbaab=ba with [2] baa=c:

a baabbaab baa

Critical pair: acbbaab=ba.

Reduce LHS:

[2]acb(baa)b
⇒ acbcb

Flip LHS and RHS.

Defines rule #2.

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

[4] acbcacbcb=c

Overlap of [2] baa=c with [3] ba=acbcb:

baa ba

Critical pair: acbcba=c.

Reduce LHS:

[3]acbc(ba)
⇒ acbcacbcb

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

[5] acbcbcbcacbcb=bc

Overlap of [3] ba=acbcb with [4] acbcacbcb=c:

b a acbcacbcb

Critical pair: bc=acbcbcbcacbcb.

Flip LHS and RHS.

Referenced by [7].

[6] ca=acbcc

Overlap of [4] acbcacbcb=c with [3] ba=acbcb:

acbcacbc b ba

Critical pair: acbcacbcacbcb=ca.

Reduce LHS:

[4]acbc(acbcacbcb)
⇒ acbcc

Flip LHS and RHS.

Defines rule #3.

Referenced by [7], [8].

[7] ccbcccbcbcbcccbcb=bc

Simplify [5] acbcbcbcacbcb=bc.

Reduce LHS:

[6]acbcbcb(ca)cbcb
[3]⇒ acbcbc(ba)cbcccbcb
[6]⇒ acbcb(ca)cbcbcbcccbcb
[3]⇒ acbc(ba)cbcccbcbcbcccbcb
[4]⇒ (acbcacbcb)cbcccbcbcbcccbcb
⇒ ccbcccbcbcbcccbcb

Defines rule #1.

[8] aacbcccbcbcbcccbcb=c

Overlap of [4] acbcacbcb=c with [6] ca=acbcc:

acb cacbcb ca

Critical pair: acbacbcccbcb=c.

Reduce LHS:

[3]ac(ba)cbcccbcb
[6]⇒ a(ca)cbcbcbcccbcb
⇒ aacbcccbcbcbcccbcb

Defines rule #4.