Certificate for #1998 ⟨a, b | aabbabba=ba⟩

Back:⟨a, b | aabbabba=ba⟩

Completion settings:

[1] aabbabba=ba

Axiom: aabbabba=ba.

Referenced by [3].

[2] bba=c

Axiom: bba=c.

Referenced by [3], [4].

[3] ba=aacc

Overlap of [1] aabbabba=ba with [2] bba=c:

aa bbabba bba

Critical pair: aacbba=ba.

Reduce LHS:

[2]aac(bba)
⇒ aacc

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] aaccacc=c

Overlap of [2] bba=c with [3] ba=aacc:

b ba ba

Critical pair: baacc=c.

Reduce LHS:

[3](ba)acc
⇒ aaccacc

Defines rule #1.

Referenced by [5].

[5] bc=cacc

Overlap of [3] ba=aacc with [4] aaccacc=c:

b a aaccacc

Critical pair: bc=aaccaccacc.

Reduce RHS:

[4](aaccacc)acc
⇒ cacc

Defines rule #3.