Certificate for #2232 ⟨a, b | aababaa=aab⟩

Back:⟨a, b | aababaa=aab⟩

Completion settings:

[1] aababaa=aab

Axiom: aababaa=aab.

Referenced by [3].

[2] babaa=c

Axiom: babaa=c.

Defines rule #4.

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

[3] aab=aac

Overlap of [1] aababaa=aab with [2] babaa=c:

aa babaa babaa

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] cb=cc

Overlap of [2] babaa=c with [3] aab=aac:

bab aa aab

Critical pair: babaac=cb.

Reduce LHS:

[2](babaa)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

Referenced by [7].

[5] cab=cac

Overlap of [2] babaa=c with [3] aab=aac:

baba a aab

Critical pair: babaaac=cab.

Reduce LHS:

[2](babaa)ac
⇒ cac

Flip LHS and RHS.

Defines rule #3.

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

[6] aacacaa=aac

Overlap of [3] aab=aac with [2] babaa=c:

aa b babaa

Critical pair: aac=aacabaa.

Reduce RHS:

[5]aa(cab)aa
⇒ aacacaa

Flip LHS and RHS.

Defines rule #6.

[7] ccacaa=cc

Overlap of [4] cb=cc with [2] babaa=c:

c b babaa

Critical pair: cc=ccabaa.

Reduce RHS:

[5]c(cab)aa
⇒ ccacaa

Flip LHS and RHS.

Defines rule #5.

[8] cacacaa=cac

Overlap of [5] cab=cac with [2] babaa=c:

ca b babaa

Critical pair: cac=cacabaa.

Reduce RHS:

[5]ca(cab)aa
⇒ cacacaa

Flip LHS and RHS.

Defines rule #7.