Certificate for #4227 ⟨a, b | abaaaaaab=ba⟩

Back:⟨a, b | abaaaaaab=ba⟩

Completion settings:

[1] abaaaaaab=ba

Axiom: abaaaaaab=ba.

Referenced by [3].

[2] aaaaaab=c

Axiom: aaaaaab=c.

Defines rule #4.

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

[3] ba=abc

Overlap of [1] abaaaaaab=ba with [2] aaaaaab=c:

ab aaaaaab aaaaaab

Critical pair: abc=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] ca=acc

Overlap of [2] aaaaaab=c with [3] ba=abc:

aaaaaa b ba

Critical pair: aaaaaaabc=ca.

Reduce LHS:

[2]a(aaaaaab)c
⇒ acc

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccb=bc

Overlap of [3] ba=abc with [2] aaaaaab=c:

b a aaaaaab

Critical pair: bc=abcaaaaab.

Reduce RHS:

[4]ab(ca)aaaab
[3]⇒ a(ba)ccaaaab
[4]⇒ aabcc(ca)aaab
[4]⇒ aabc(ca)ccaaab
[4]⇒ aab(ca)ccccaaab
[3]⇒ aa(ba)ccccccaaab
[4]⇒ aaabcccccc(ca)aab
[4]⇒ aaabccccc(ca)ccaab
[4]⇒ aaabcccc(ca)ccccaab
[4]⇒ aaabccc(ca)ccccccaab
[4]⇒ aaabcc(ca)ccccccccaab
[4]⇒ aaabc(ca)ccccccccccaab
[4]⇒ aaab(ca)ccccccccccccaab
[3]⇒ aaa(ba)ccccccccccccccaab
[4]⇒ aaaabcccccccccccccc(ca)ab
[4]⇒ aaaabccccccccccccc(ca)ccab
[4]⇒ aaaabcccccccccccc(ca)ccccab
[4]⇒ aaaabccccccccccc(ca)ccccccab
[4]⇒ aaaabcccccccccc(ca)ccccccccab
[4]⇒ aaaabccccccccc(ca)ccccccccccab
[4]⇒ aaaabcccccccc(ca)ccccccccccccab
[4]⇒ aaaabccccccc(ca)ccccccccccccccab
[4]⇒ aaaabcccccc(ca)ccccccccccccccccab
[4]⇒ aaaabccccc(ca)ccccccccccccccccccab
[4]⇒ aaaabcccc(ca)ccccccccccccccccccccab
[4]⇒ aaaabccc(ca)ccccccccccccccccccccccab
[4]⇒ aaaabcc(ca)ccccccccccccccccccccccccab
[4]⇒ aaaabc(ca)ccccccccccccccccccccccccccab
[4]⇒ aaaab(ca)ccccccccccccccccccccccccccccab
[3]⇒ aaaa(ba)ccccccccccccccccccccccccccccccab
[4]⇒ aaaaabcccccccccccccccccccccccccccccc(ca)b
[4]⇒ aaaaabccccccccccccccccccccccccccccc(ca)ccb
[4]⇒ aaaaabcccccccccccccccccccccccccccc(ca)ccccb
[4]⇒ aaaaabccccccccccccccccccccccccccc(ca)ccccccb
[4]⇒ aaaaabcccccccccccccccccccccccccc(ca)ccccccccb
[4]⇒ aaaaabccccccccccccccccccccccccc(ca)ccccccccccb
[4]⇒ aaaaabcccccccccccccccccccccccc(ca)ccccccccccccb
[4]⇒ aaaaabccccccccccccccccccccccc(ca)ccccccccccccccb
[4]⇒ aaaaabcccccccccccccccccccccc(ca)ccccccccccccccccb
[4]⇒ aaaaabccccccccccccccccccccc(ca)ccccccccccccccccccb
[4]⇒ aaaaabcccccccccccccccccccc(ca)ccccccccccccccccccccb
[4]⇒ aaaaabccccccccccccccccccc(ca)ccccccccccccccccccccccb
[4]⇒ aaaaabcccccccccccccccccc(ca)ccccccccccccccccccccccccb
[4]⇒ aaaaabccccccccccccccccc(ca)ccccccccccccccccccccccccccb
[4]⇒ aaaaabcccccccccccccccc(ca)ccccccccccccccccccccccccccccb
[4]⇒ aaaaabccccccccccccccc(ca)ccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcccccccccccccc(ca)ccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabccccccccccccc(ca)ccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcccccccccccc(ca)ccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabccccccccccc(ca)ccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcccccccccc(ca)ccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabccccccccc(ca)ccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcccccccc(ca)ccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabccccccc(ca)ccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcccccc(ca)ccccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabccccc(ca)ccccccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcccc(ca)ccccccccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabccc(ca)ccccccccccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabcc(ca)ccccccccccccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaabc(ca)ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccb
[4]⇒ aaaaab(ca)ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccb
[3]⇒ aaaaa(ba)ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccb
[2]⇒ (aaaaaab)cccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccb
⇒ ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccb

Flip LHS and RHS.

Defines rule #1.