Certificate for #1050 ⟨a, b | aaabba=aab⟩

Back:⟨a, b | aaabba=aab⟩

Completion settings:

[1] aaabba=aab

Axiom: aaabba=aab.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #4.

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

[3] aaabba=c

Simplify [1] aaabba=aab.

Reduce RHS:

[2](aab)
⇒ c

Referenced by [4].

[4] acba=c

Overlap of [3] aaabba=c with [2] aab=c:

a aabba aab

Critical pair: acba=c.

Defines rule #3.

Referenced by [5], [6].

[5] acbc=cab

Overlap of [4] acba=c with [2] aab=c:

acb a aab

Critical pair: acbc=cab.

Referenced by [6], [7].

[6] cab=ccba

Overlap of [4] acba=c with [4] acba=c:

acb a acba

Critical pair: acbc=ccba.

Reduce LHS:

[5](acbc)
⇒ cab

Defines rule #1.

Referenced by [7].

[7] acbc=ccba

Simplify [5] acbc=cab.

Reduce RHS:

[6](cab)
⇒ ccba

Defines rule #2.