Certificate for #3429 ⟨a, b | aaabaaaaba=a⟩

Back:⟨a, b | aaabaaaaba=a⟩

Completion settings:

[1] aaabaaaaba=a

Axiom: aaabaaaaba=a.

Referenced by [2], [3].

[2] aaabaa=aaaaba

Overlap of [1] aaabaaaaba=a with [1] aaabaaaaba=a:

aaaba aaaba aaabaaaaba

Critical pair: aaabaa=aaaaba.

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

[3] aaaaaababa=a

Overlap of [1] aaabaaaaba=a with [2] aaabaa=aaaaba:

aaabaaaaba aaabaa

Critical pair: aaaabaaaba=a.

Reduce LHS:

[2]a(aaabaa)aba
[2]⇒ aa(aaabaa)ba
⇒ aaaaaababa

Defines rule #2.

Referenced by [4], [5].

[4] aaaaababaa=a

Overlap of [2] aaabaa=aaaaba with [2] aaabaa=aaaaba:

aaab aa aaabaa

Critical pair: aaabaaaaba=aaaabaabaa.

Reduce LHS:

[2](aaabaa)aaba
[2]⇒ a(aaabaa)aba
[2]⇒ aa(aaabaa)ba
[3]⇒ (aaaaaababa)
⇒ a

Reduce RHS:

[2]a(aaabaa)baa
⇒ aaaaababaa

Flip LHS and RHS.

Referenced by [5], [6].

[5] aabaa=aaaba

Overlap of [2] aaabaa=aaaaba with [4] aaaaababaa=a:

aaab aa aaaaababaa

Critical pair: aaaba=aaaabaaaababaa.

Reduce RHS:

[2]a(aaabaa)aababaa
[2]⇒ aa(aaabaa)ababaa
[2]⇒ aaa(aaabaa)babaa
[3]⇒ a(aaaaaababa)baa
⇒ aabaa

Flip LHS and RHS.

Referenced by [6].

[6] abaa=aaba

Overlap of [4] aaaaababaa=a with [5] aabaa=aaaba:

aaaaabab aa aabaa

Critical pair: aaaaababaaaba=abaa.

Reduce LHS:

[4](aaaaababaa)aba
⇒ aaba

Flip LHS and RHS.

Defines rule #1.