Certificate for #1844 ⟨a, b | aaaaabba=ba⟩

Back:⟨a, b | aaaaabba=ba⟩

Completion settings:

[1] aaaaabba=ba

Axiom: aaaaabba=ba.

Referenced by [3].

[2] aaaaabb=c

Axiom: aaaaabb=c.

Defines rule #3.

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

[3] ba=ca

Overlap of [1] aaaaabba=ba with [2] aaaaabb=c:

aaaaabba aaaaabb

Critical pair: ca=ba.

Flip LHS and RHS.

Defines rule #1.

Referenced by [4], [5].

[4] aaaaabca=ca

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

aaaaab b ba

Critical pair: aaaaabca=ca.

Referenced by [7].

[5] bc=cc

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

b a aaaaabb

Critical pair: bc=caaaaabb.

Reduce RHS:

[2]c(aaaaabb)
⇒ cc

Defines rule #2.

Referenced by [6], [7].

[6] aaaaaccc=cc

Overlap of [2] aaaaabb=c with [5] bc=cc:

aaaaab b bc

Critical pair: aaaaabcc=cc.

Reduce LHS:

[5]aaaaa(bc)c
⇒ aaaaaccc

Defines rule #5.

[7] aaaaacca=ca

Simplify [4] aaaaabca=ca.

Reduce LHS:

[5]aaaaa(bc)a
⇒ aaaaacca

Defines rule #4.