Certificate for #1903 ⟨a, b | aaababba=ba⟩

Back:⟨a, b | aaababba=ba⟩

Completion settings:

[1] aaababba=ba

Axiom: aaababba=ba.

Referenced by [3].

[2] aaababb=c

Axiom: aaababb=c.

Referenced by [3], [4].

[3] ba=ca

Overlap of [1] aaababba=ba with [2] aaababb=c:

aaababba aaababb

Critical pair: ca=ba.

Flip LHS and RHS.

Defines rule #1.

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

[4] aaacabb=c

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

aaa babb ba

Critical pair: aaacabb=c.

Defines rule #3.

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

[5] bc=cc

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

b a aaacabb

Critical pair: bc=caaacabb.

Reduce RHS:

[4]c(aaacabb)
⇒ cc

Defines rule #2.

Referenced by [6], [7].

[6] aaacacca=ca

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

aaacab b ba

Critical pair: aaacabca=ca.

Reduce LHS:

[5]aaaca(bc)a
⇒ aaacacca

Defines rule #4.

[7] aaacaccc=cc

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

aaacab b bc

Critical pair: aaacabcc=cc.

Reduce LHS:

[5]aaaca(bc)c
⇒ aaacaccc

Defines rule #5.