Certificate for #841 ⟨a, b | abaababa=a⟩

Back:⟨a, b | abaababa=a⟩

Completion settings:

[1] abaababa=a

Axiom: abaababa=a.

Referenced by [2], [3].

[2] abaaba=aababa

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

abaab aba abaababa

Critical pair: abaaba=aababa.

Referenced by [3], [4].

[3] aabababa=a

Overlap of [1] abaababa=a with [2] abaaba=aababa:

abaababa abaaba

Critical pair: aabababa=a.

Defines rule #2.

Referenced by [4], [5].

[4] abaaababa=aa

Overlap of [2] abaaba=aababa with [2] abaaba=aababa:

aba aba abaaba

Critical pair: abaaababa=aababaaba.

Reduce RHS:

[2]aab(abaaba)
[2]⇒ a(abaaba)ba
[3]⇒ a(aabababa)
⇒ aa

Referenced by [5].

[5] abaa=aaba

Overlap of [4] abaaababa=aa with [3] aabababa=a:

aba aababa aabababa

Critical pair: abaa=aaba.

Defines rule #1.