Certificate for #4659 ⟨a, b | aababbaa=baa⟩

Back:⟨a, b | aababbaa=baa⟩

Completion settings:

[1] aababbaa=baa

Axiom: aababbaa=baa.

Referenced by [3].

[2] aababb=c

Axiom: aababb=c.

Defines rule #4.

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

[3] baa=caa

Overlap of [1] aababbaa=baa with [2] aababb=c:

aababbaa aababb

Critical pair: caa=baa.

Flip LHS and RHS.

Defines rule #2.

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

[4] aababcaa=caa

Overlap of [2] aababb=c with [3] baa=caa:

aabab b baa

Critical pair: aababcaa=caa.

Referenced by [9].

[5] bc=cc

Overlap of [3] baa=caa with [2] aababb=c:

b aa aababb

Critical pair: bc=caababb.

Reduce RHS:

[2]c(aababb)
⇒ cc

Defines rule #1.

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

[6] bac=cac

Overlap of [3] baa=caa with [2] aababb=c:

ba a aababb

Critical pair: bac=caaababb.

Reduce RHS:

[2]ca(aababb)
⇒ cac

Defines rule #3.

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

[7] aacaccc=cc

Overlap of [2] aababb=c with [5] bc=cc:

aabab b bc

Critical pair: aababcc=cc.

Reduce LHS:

[5]aaba(bc)c
[6]⇒ aa(bac)cc
⇒ aacaccc

Defines rule #5.

[8] aacaccac=cac

Overlap of [2] aababb=c with [6] bac=cac:

aabab b bac

Critical pair: aababcac=cac.

Reduce LHS:

[5]aaba(bc)ac
[6]⇒ aa(bac)cac
⇒ aacaccac

Defines rule #7.

[9] aacaccaa=caa

Simplify [4] aababcaa=caa.

Reduce LHS:

[5]aaba(bc)aa
[6]⇒ aa(bac)caa
⇒ aacaccaa

Defines rule #6.