Certificate for #4569 ⟨a, b | aaabbbaa=baa⟩

Back:⟨a, b | aaabbbaa=baa⟩

Completion settings:

[1] aaabbbaa=baa

Axiom: aaabbbaa=baa.

Referenced by [3].

[2] aaabbb=c

Axiom: aaabbb=c.

Defines rule #4.

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

[3] baa=caa

Overlap of [1] aaabbbaa=baa with [2] aaabbb=c:

aaabbbaa aaabbb

Critical pair: caa=baa.

Flip LHS and RHS.

Defines rule #2.

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

[4] aaabbcaa=caa

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

aaabb b baa

Critical pair: aaabbcaa=caa.

Referenced by [9].

[5] bc=cc

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

b aa aaabbb

Critical pair: bc=caaabbb.

Reduce RHS:

[2]c(aaabbb)
⇒ cc

Defines rule #1.

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

[6] bac=cac

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

ba a aaabbb

Critical pair: bac=caaaabbb.

Reduce RHS:

[2]ca(aaabbb)
⇒ cac

Defines rule #3.

Referenced by [8].

[7] aaacccc=cc

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

aaabb b bc

Critical pair: aaabbcc=cc.

Reduce LHS:

[5]aaab(bc)c
[5]⇒ aaa(bc)cc
⇒ aaacccc

Defines rule #5.

[8] aaacccac=cac

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

aaabb b bac

Critical pair: aaabbcac=cac.

Reduce LHS:

[5]aaab(bc)ac
[5]⇒ aaa(bc)cac
⇒ aaacccac

Defines rule #7.

[9] aaacccaa=caa

Simplify [4] aaabbcaa=caa.

Reduce LHS:

[5]aaab(bc)aa
[5]⇒ aaa(bc)caa
⇒ aaacccaa

Defines rule #6.