Certificate for #2058 ⟨a, b | abababba=ba⟩

Back:⟨a, b | abababba=ba⟩

Completion settings:

[1] abababba=ba

Axiom: abababba=ba.

Referenced by [3].

[2] abababb=c

Axiom: abababb=c.

Referenced by [3], [4].

[3] ba=ca

Overlap of [1] abababba=ba with [2] abababb=c:

abababba abababb

Critical pair: ca=ba.

Flip LHS and RHS.

Defines rule #1.

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

[4] acacabb=c

Overlap of [2] abababb=c with [3] ba=ca:

a bababb ba

Critical pair: acababb=c.

Reduce LHS:

[3]aca(ba)bb
⇒ acacabb

Defines rule #3.

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

[5] bc=cc

Overlap of [3] ba=ca with [4] acacabb=c:

b a acacabb

Critical pair: bc=cacacabb.

Reduce RHS:

[4]c(acacabb)
⇒ cc

Defines rule #2.

Referenced by [6], [7].

[6] acacacca=ca

Overlap of [4] acacabb=c with [3] ba=ca:

acacab b ba

Critical pair: acacabca=ca.

Reduce LHS:

[5]acaca(bc)a
⇒ acacacca

Defines rule #4.

[7] acacaccc=cc

Overlap of [4] acacabb=c with [5] bc=cc:

acacab b bc

Critical pair: acacabcc=cc.

Reduce LHS:

[5]acaca(bc)c
⇒ acacaccc

Defines rule #5.