Certificate for #2021 ⟨a, b | abaaaaab=ba⟩

Back:⟨a, b | abaaaaab=ba⟩

Completion settings:

[1] abaaaaab=ba

Axiom: abaaaaab=ba.

Referenced by [3].

[2] aaaaab=c

Axiom: aaaaab=c.

Defines rule #4.

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

[3] ba=abc

Overlap of [1] abaaaaab=ba with [2] aaaaab=c:

ab aaaaab aaaaab

Critical pair: abc=ba.

Flip LHS and RHS.

Defines rule #2.

Referenced by [4], [5].

[4] ca=acc

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

aaaaa b ba

Critical pair: aaaaaabc=ca.

Reduce LHS:

[2]a(aaaaab)c
⇒ acc

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] ccccccccccccccccccccccccccccccccb=bc

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

b a aaaaab

Critical pair: bc=abcaaaab.

Reduce RHS:

[4]ab(ca)aaab
[3]⇒ a(ba)ccaaab
[4]⇒ aabcc(ca)aab
[4]⇒ aabc(ca)ccaab
[4]⇒ aab(ca)ccccaab
[3]⇒ aa(ba)ccccccaab
[4]⇒ aaabcccccc(ca)ab
[4]⇒ aaabccccc(ca)ccab
[4]⇒ aaabcccc(ca)ccccab
[4]⇒ aaabccc(ca)ccccccab
[4]⇒ aaabcc(ca)ccccccccab
[4]⇒ aaabc(ca)ccccccccccab
[4]⇒ aaab(ca)ccccccccccccab
[3]⇒ aaa(ba)ccccccccccccccab
[4]⇒ aaaabcccccccccccccc(ca)b
[4]⇒ aaaabccccccccccccc(ca)ccb
[4]⇒ aaaabcccccccccccc(ca)ccccb
[4]⇒ aaaabccccccccccc(ca)ccccccb
[4]⇒ aaaabcccccccccc(ca)ccccccccb
[4]⇒ aaaabccccccccc(ca)ccccccccccb
[4]⇒ aaaabcccccccc(ca)ccccccccccccb
[4]⇒ aaaabccccccc(ca)ccccccccccccccb
[4]⇒ aaaabcccccc(ca)ccccccccccccccccb
[4]⇒ aaaabccccc(ca)ccccccccccccccccccb
[4]⇒ aaaabcccc(ca)ccccccccccccccccccccb
[4]⇒ aaaabccc(ca)ccccccccccccccccccccccb
[4]⇒ aaaabcc(ca)ccccccccccccccccccccccccb
[4]⇒ aaaabc(ca)ccccccccccccccccccccccccccb
[4]⇒ aaaab(ca)ccccccccccccccccccccccccccccb
[3]⇒ aaaa(ba)ccccccccccccccccccccccccccccccb
[2]⇒ (aaaaab)cccccccccccccccccccccccccccccccb
⇒ ccccccccccccccccccccccccccccccccb

Flip LHS and RHS.

Defines rule #1.