Certificate for #4614 ⟨a, b | aabaabaa=aab⟩

Back:⟨a, b | aabaabaa=aab⟩

Completion settings:

[1] aabaabaa=aab

Axiom: aabaabaa=aab.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #3.

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

[3] aabaabaa=c

Simplify [1] aabaabaa=aab.

Reduce RHS:

[2](aab)
⇒ c

Referenced by [4].

[4] ccaa=c

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

aabaabaa aab

Critical pair: caabaa=c.

Reduce LHS:

[2]c(aab)aa
⇒ ccaa

Defines rule #1.

Referenced by [5], [6].

[5] cb=ccc

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

cc aa aab

Critical pair: ccc=cb.

Flip LHS and RHS.

Defines rule #2.

[6] cab=ccac

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

cca a aab

Critical pair: ccac=cab.

Flip LHS and RHS.

Defines rule #4.