Certificate for #2270 ⟨a, b | aabbbaa=aab⟩

Back:⟨a, b | aabbbaa=aab⟩

Completion settings:

[1] aabbbaa=aab

Axiom: aabbbaa=aab.

Referenced by [3].

[2] bbbaa=c

Axiom: bbbaa=c.

Defines rule #4.

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

[3] aab=aac

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

aa bbbaa bbbaa

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] cb=cc

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

bbb aa aab

Critical pair: bbbaac=cb.

Reduce LHS:

[2](bbbaa)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

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

[5] cab=cac

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

bbba a aab

Critical pair: bbbaaac=cab.

Reduce LHS:

[2](bbbaa)ac
⇒ cac

Flip LHS and RHS.

Defines rule #3.

Referenced by [8].

[6] aacccaa=aac

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

aa b bbbaa

Critical pair: aac=aacbbaa.

Reduce RHS:

[4]aa(cb)baa
[4]⇒ aac(cb)aa
⇒ aacccaa

Flip LHS and RHS.

Defines rule #6.

[7] ccccaa=cc

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

c b bbbaa

Critical pair: cc=ccbbaa.

Reduce RHS:

[4]c(cb)baa
[4]⇒ cc(cb)aa
⇒ ccccaa

Flip LHS and RHS.

Defines rule #5.

[8] cacccaa=cac

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

ca b bbbaa

Critical pair: cac=cacbbaa.

Reduce RHS:

[4]ca(cb)baa
[4]⇒ cac(cb)aa
⇒ cacccaa

Flip LHS and RHS.

Defines rule #7.