Certificate for #4656 ⟨a, b | aababbaa=aab⟩

Back:⟨a, b | aababbaa=aab⟩

Completion settings:

[1] aababbaa=aab

Axiom: aababbaa=aab.

Referenced by [3].

[2] babbaa=c

Axiom: babbaa=c.

Defines rule #4.

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

[3] aab=aac

Overlap of [1] aababbaa=aab with [2] babbaa=c:

aa babbaa babbaa

Critical pair: aac=aab.

Flip LHS and RHS.

Defines rule #2.

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

[4] cb=cc

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

babb aa aab

Critical pair: babbaac=cb.

Reduce LHS:

[2](babbaa)c
⇒ cc

Flip LHS and RHS.

Defines rule #1.

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

[5] cab=cac

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

babba a aab

Critical pair: babbaaac=cab.

Reduce LHS:

[2](babbaa)ac
⇒ cac

Flip LHS and RHS.

Defines rule #3.

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

[6] aacaccaa=aac

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

aa b babbaa

Critical pair: aac=aacabbaa.

Reduce RHS:

[5]aa(cab)baa
[4]⇒ aaca(cb)aa
⇒ aacaccaa

Flip LHS and RHS.

Defines rule #6.

[7] ccaccaa=cc

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

c b babbaa

Critical pair: cc=ccabbaa.

Reduce RHS:

[5]c(cab)baa
[4]⇒ cca(cb)aa
⇒ ccaccaa

Flip LHS and RHS.

Defines rule #5.

[8] cacaccaa=cac

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

ca b babbaa

Critical pair: cac=cacabbaa.

Reduce RHS:

[5]ca(cab)baa
[4]⇒ caca(cb)aa
⇒ cacaccaa

Flip LHS and RHS.

Defines rule #7.