Certificate for #2187 ⟨a, b | aaabbaa=baa⟩

Back:⟨a, b | aaabbaa=baa⟩

Completion settings:

[1] aaabbaa=baa

Axiom: aaabbaa=baa.

Referenced by [3].

[2] aaabb=c

Axiom: aaabb=c.

Defines rule #4.

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

[3] baa=caa

Overlap of [1] aaabbaa=baa with [2] aaabb=c:

aaabbaa aaabb

Critical pair: caa=baa.

Flip LHS and RHS.

Defines rule #2.

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

[4] aaabcaa=caa

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

aaab b baa

Critical pair: aaabcaa=caa.

Referenced by [9].

[5] bc=cc

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

b aa aaabb

Critical pair: bc=caaabb.

Reduce RHS:

[2]c(aaabb)
⇒ cc

Defines rule #1.

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

[6] bac=cac

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

ba a aaabb

Critical pair: bac=caaaabb.

Reduce RHS:

[2]ca(aaabb)
⇒ cac

Defines rule #3.

Referenced by [8].

[7] aaaccc=cc

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

aaab b bc

Critical pair: aaabcc=cc.

Reduce LHS:

[5]aaa(bc)c
⇒ aaaccc

Defines rule #5.

[8] aaaccac=cac

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

aaab b bac

Critical pair: aaabcac=cac.

Reduce LHS:

[5]aaa(bc)ac
⇒ aaaccac

Defines rule #7.

[9] aaaccaa=caa

Simplify [4] aaabcaa=caa.

Reduce LHS:

[5]aaa(bc)aa
⇒ aaaccaa

Defines rule #6.