Certificate for #4566 ⟨a, b | aaabbbaa=aab⟩

Back:⟨a, b | aaabbbaa=aab⟩

Completion settings:

[1] aaabbbaa=aab

Axiom: aaabbbaa=aab.

Referenced by [3].

[2] bbbaa=c

Axiom: bbbaa=c.

Defines rule #10.

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

[3] aab=aaac

Overlap of [1] aaabbbaa=aab with [2] bbbaa=c:

aaa bbbaa bbbaa

Critical pair: aaac=aab.

Flip LHS and RHS.

Defines rule #8.

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

[4] cb=cac

Overlap of [2] bbbaa=c with [3] aab=aaac:

bbb aa aab

Critical pair: bbbaaac=cb.

Reduce LHS:

[2](bbbaa)ac
⇒ cac

Flip LHS and RHS.

Defines rule #7.

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

[5] cab=caac

Overlap of [2] bbbaa=c with [3] aab=aaac:

bbba a aab

Critical pair: bbbaaaac=cab.

Reduce LHS:

[2](bbbaa)aac
⇒ caac

Flip LHS and RHS.

Defines rule #9.

Referenced by [8].

[6] aaacacacaa=aac

Overlap of [3] aab=aaac with [2] bbbaa=c:

aa b bbbaa

Critical pair: aac=aaacbbaa.

Reduce RHS:

[4]aaa(cb)baa
[4]⇒ aaaca(cb)aa
⇒ aaacacacaa

Flip LHS and RHS.

Defines rule #3.

Referenced by [9].

[7] cacacacaa=cc

Overlap of [4] cb=cac with [2] bbbaa=c:

c b bbbaa

Critical pair: cc=cacbbaa.

Reduce RHS:

[4]ca(cb)baa
[4]⇒ caca(cb)aa
⇒ cacacacaa

Flip LHS and RHS.

Defines rule #1.

Referenced by [10].

[8] caacacacaa=cac

Overlap of [5] cab=caac with [2] bbbaa=c:

ca b bbbaa

Critical pair: cac=caacbbaa.

Reduce RHS:

[4]caa(cb)baa
[4]⇒ caaca(cb)aa
⇒ caacacacaa

Flip LHS and RHS.

Defines rule #5.

Referenced by [9], [10], [11].

[9] aaccacacaa=aaacacacac

Overlap of [6] aaacacacaa=aac with [8] caacacacaa=cac:

aaacaca caa caacacacaa

Critical pair: aaacacacac=aaccacacaa.

Flip LHS and RHS.

Defines rule #4.

[10] cccacacaa=cacacacac

Overlap of [7] cacacacaa=cc with [8] caacacacaa=cac:

cacaca caa caacacacaa

Critical pair: cacacacac=cccacacaa.

Flip LHS and RHS.

Defines rule #2.

[11] caccacacaa=caacacacac

Overlap of [8] caacacacaa=cac with [8] caacacacaa=cac:

caacaca caa caacacacaa

Critical pair: caacacacac=caccacacaa.

Flip LHS and RHS.

Defines rule #6.