Certificate for #1082 ⟨a, b | aabbaa=aab⟩

Back:⟨a, b | aabbaa=aab⟩

Completion settings:

[1] aabbaa=aab

Axiom: aabbaa=aab.

Referenced by [3].

[2] bbaa=c

Axiom: bbaa=c.

Defines rule #4.

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

[3] aab=aac

Overlap of [1] aabbaa=aab with [2] bbaa=c:

aa bbaa bbaa

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] cb=cc

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

bb aa aab

Critical pair: bbaac=cb.

Reduce LHS:

[2](bbaa)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

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

[5] cab=cac

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

bba a aab

Critical pair: bbaaac=cab.

Reduce LHS:

[2](bbaa)ac
⇒ cac

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[6] aaccaa=aac

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

aa b bbaa

Critical pair: aac=aacbaa.

Reduce RHS:

[4]aa(cb)aa
⇒ aaccaa

Flip LHS and RHS.

Defines rule #6.

[7] cccaa=cc

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

c b bbaa

Critical pair: cc=ccbaa.

Reduce RHS:

[4]c(cb)aa
⇒ cccaa

Flip LHS and RHS.

Defines rule #5.

[8] caccaa=cac

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

ca b bbaa

Critical pair: cac=cacbaa.

Reduce RHS:

[4]ca(cb)aa
⇒ caccaa

Flip LHS and RHS.

Defines rule #7.