Certificate for #4732 ⟨a, b | aabbbbaa=aab⟩

Back:⟨a, b | aabbbbaa=aab⟩

Completion settings:

[1] aabbbbaa=aab

Axiom: aabbbbaa=aab.

Referenced by [3].

[2] bbbbaa=c

Axiom: bbbbaa=c.

Defines rule #4.

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

[3] aab=aac

Overlap of [1] aabbbbaa=aab with [2] bbbbaa=c:

aa bbbbaa bbbbaa

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] cb=cc

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

bbbb aa aab

Critical pair: bbbbaac=cb.

Reduce LHS:

[2](bbbbaa)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

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

[5] cab=cac

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

bbbba a aab

Critical pair: bbbbaaac=cab.

Reduce LHS:

[2](bbbbaa)ac
⇒ cac

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[6] aaccccaa=aac

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

aa b bbbbaa

Critical pair: aac=aacbbbaa.

Reduce RHS:

[4]aa(cb)bbaa
[4]⇒ aac(cb)baa
[4]⇒ aacc(cb)aa
⇒ aaccccaa

Flip LHS and RHS.

Defines rule #6.

[7] cccccaa=cc

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

c b bbbbaa

Critical pair: cc=ccbbbaa.

Reduce RHS:

[4]c(cb)bbaa
[4]⇒ cc(cb)baa
[4]⇒ ccc(cb)aa
⇒ cccccaa

Flip LHS and RHS.

Defines rule #5.

[8] caccccaa=cac

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

ca b bbbbaa

Critical pair: cac=cacbbbaa.

Reduce RHS:

[4]ca(cb)bbaa
[4]⇒ cac(cb)baa
[4]⇒ cacc(cb)aa
⇒ caccccaa

Flip LHS and RHS.

Defines rule #7.