Certificate for #4511 ⟨a, b | aaababaa=baa⟩

Back:⟨a, b | aaababaa=baa⟩

Completion settings:

[1] aaababaa=baa

Axiom: aaababaa=baa.

Referenced by [3].

[2] aaabab=c

Axiom: aaabab=c.

Defines rule #4.

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

[3] baa=caa

Overlap of [1] aaababaa=baa with [2] aaabab=c:

aaababaa aaabab

Critical pair: caa=baa.

Flip LHS and RHS.

Defines rule #2.

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

[4] aaabacaa=caa

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

aaaba b baa

Critical pair: aaabacaa=caa.

Referenced by [9].

[5] bc=cc

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

b aa aaabab

Critical pair: bc=caaabab.

Reduce RHS:

[2]c(aaabab)
⇒ cc

Defines rule #1.

Referenced by [7].

[6] bac=cac

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

ba a aaabab

Critical pair: bac=caaaabab.

Reduce RHS:

[2]ca(aaabab)
⇒ cac

Defines rule #3.

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

[7] aaacacc=cc

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

aaaba b bc

Critical pair: aaabacc=cc.

Reduce LHS:

[6]aaa(bac)c
⇒ aaacacc

Defines rule #5.

[8] aaacacac=cac

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

aaaba b bac

Critical pair: aaabacac=cac.

Reduce LHS:

[6]aaa(bac)ac
⇒ aaacacac

Defines rule #7.

[9] aaacacaa=caa

Simplify [4] aaabacaa=caa.

Reduce LHS:

[6]aaa(bac)aa
⇒ aaacacaa

Defines rule #6.