Certificate for #5304 ⟨a, b | abaaaba=baab⟩

Back:⟨a, b | abaaaba=baab⟩

Completion settings:

[1] abaaaba=baab

Axiom: abaaaba=baab.

Referenced by [3].

[2] aaab=c

Axiom: aaab=c.

Defines rule #3.

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

[3] baab=abca

Overlap of [1] abaaaba=baab with [2] aaab=c:

ab aaaba aaab

Critical pair: abca=baab.

Flip LHS and RHS.

Defines rule #6.

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

[4] acca=caab

Overlap of [2] aaab=c with [3] baab=abca:

aaa b baab

Critical pair: aaaabca=caab.

Reduce LHS:

[2]a(aaab)ca
⇒ acca

Defines rule #2.

Referenced by [6], [7].

[5] bcca=abcc

Overlap of [3] baab=abca with [3] baab=abca:

baa b baab

Critical pair: baaabca=abcaaab.

Reduce LHS:

[2]b(aaab)ca
⇒ bcca

Reduce RHS:

[2]abc(aaab)
⇒ abcc

Defines rule #5.

Referenced by [7].

[6] accc=ccca

Overlap of [4] acca=caab with [2] aaab=c:

acc a aaab

Critical pair: accc=caabaab.

Reduce RHS:

[3]caa(baab)
[2]⇒ c(aaab)ca
⇒ ccca

Defines rule #1.

[7] bccc=cccb

Overlap of [3] baab=abca with [5] bcca=abcc:

baa b bcca

Critical pair: baaabcc=abcacca.

Reduce LHS:

[2]b(aaab)cc
⇒ bccc

Reduce RHS:

[4]abc(acca)
[5]⇒ a(bcca)ab
[5]⇒ aa(bcca)b
[2]⇒ (aaab)ccb
⇒ cccb

Defines rule #4.