Certificate for #3557 ⟨a, b | aabaabaaab=a⟩

Back:⟨a, b | aabaabaaab=a⟩

Completion settings:

[1] aabaabaaab=a

Axiom: aabaabaaab=a.

Referenced by [3].

[2] aab=c

Axiom: aab=c.

Defines rule #2.

Referenced by [3].

[3] ccac=a

Overlap of [1] aabaabaaab=a with [2] aab=c:

aabaabaaab aab

Critical pair: caabaaab=a.

Reduce LHS:

[2]c(aab)aaab
[2]⇒ cca(aab)
⇒ ccac

Defines rule #1.

Referenced by [4], [5].

[4] acac=ccaa

Overlap of [3] ccac=a with [3] ccac=a:

cca c ccac

Critical pair: ccaa=acac.

Flip LHS and RHS.

Defines rule #4.

Referenced by [5].

[5] aac=ccccaa

Overlap of [3] ccac=a with [4] acac=ccaa:

cc ac acac

Critical pair: ccccaa=aac.

Flip LHS and RHS.

Defines rule #3.