Certificate for #791 ⟨a, b | aabaaaba=a⟩

Back:⟨a, b | aabaaaba=a⟩

Completion settings:

[1] aabaaaba=a

Axiom: aabaaaba=a.

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

[2] aabaa=aaaba

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

aaba aaba aabaaaba

Critical pair: aabaa=aaaba.

Referenced by [3], [4].

[3] aaaababa=a

Overlap of [1] aabaaaba=a with [2] aabaa=aaaba:

aabaaaba aabaa

Critical pair: aaabaaba=a.

Reduce LHS:

[2]a(aabaa)ba
⇒ aaaababa

Defines rule #2.

Referenced by [4].

[4] aaababaa=a

Overlap of [2] aabaa=aaaba with [2] aabaa=aaaba:

aab aa aabaa

Critical pair: aabaaaba=aaababaa.

Reduce LHS:

[2](aabaa)aba
[2]⇒ a(aabaa)ba
[3]⇒ (aaaababa)
⇒ a

Flip LHS and RHS.

Referenced by [5].

[5] abaa=aaba

Overlap of [1] aabaaaba=a with [4] aaababaa=a:

aab aaaba aaababaa

Critical pair: aaba=abaa.

Flip LHS and RHS.

Defines rule #1.