Certificate for #4459 ⟨a, b | aaaabbaa=baa⟩

Back:⟨a, b | aaaabbaa=baa⟩

Completion settings:

[1] aaaabbaa=baa

Axiom: aaaabbaa=baa.

Referenced by [3].

[2] aaaabb=c

Axiom: aaaabb=c.

Defines rule #4.

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

[3] baa=caa

Overlap of [1] aaaabbaa=baa with [2] aaaabb=c:

aaaabbaa aaaabb

Critical pair: caa=baa.

Flip LHS and RHS.

Defines rule #2.

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

[4] aaaabcaa=caa

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

aaaab b baa

Critical pair: aaaabcaa=caa.

Referenced by [9].

[5] bc=cc

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

b aa aaaabb

Critical pair: bc=caaaabb.

Reduce RHS:

[2]c(aaaabb)
⇒ cc

Defines rule #1.

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

[6] bac=cac

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

ba a aaaabb

Critical pair: bac=caaaaabb.

Reduce RHS:

[2]ca(aaaabb)
⇒ cac

Defines rule #3.

Referenced by [8].

[7] aaaaccc=cc

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

aaaab b bc

Critical pair: aaaabcc=cc.

Reduce LHS:

[5]aaaa(bc)c
⇒ aaaaccc

Defines rule #5.

[8] aaaaccac=cac

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

aaaab b bac

Critical pair: aaaabcac=cac.

Reduce LHS:

[5]aaaa(bc)ac
⇒ aaaaccac

Defines rule #7.

[9] aaaaccaa=caa

Simplify [4] aaaabcaa=caa.

Reduce LHS:

[5]aaaa(bc)aa
⇒ aaaaccaa

Defines rule #6.