Certificate for #1199 ⟨a, b | aabaa=aaba⟩

Back:⟨a, b | aabaa=aaba⟩

Completion settings:

[1] aabaa=aaba

Axiom: aabaa=aaba.

Referenced by [3].

[2] aaba=c

Axiom: aaba=c.

Defines rule #4.

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

[3] aabaa=c

Simplify [1] aabaa=aaba.

Reduce RHS:

[2](aaba)
⇒ c

Referenced by [4].

[4] ca=c

Overlap of [3] aabaa=c with [2] aaba=c:

aabaa aaba

Critical pair: ca=c.

Defines rule #1.

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

[5] aabc=cba

Overlap of [2] aaba=c with [2] aaba=c:

aab a aaba

Critical pair: aabc=caba.

Reduce RHS:

[4](ca)ba
⇒ cba

Referenced by [8].

[6] cba=cc

Overlap of [4] ca=c with [2] aaba=c:

c a aaba

Critical pair: cc=caba.

Reduce RHS:

[4](ca)ba
⇒ cba

Flip LHS and RHS.

Defines rule #2.

Referenced by [7], [8].

[7] cbc=ccc

Overlap of [6] cba=cc with [2] aaba=c:

cb a aaba

Critical pair: cbc=ccaba.

Reduce RHS:

[4]c(ca)ba
[6]⇒ c(cba)
⇒ ccc

Defines rule #3.

[8] aabc=cc

Simplify [5] aabc=cba.

Reduce RHS:

[6](cba)
⇒ cc

Defines rule #5.