Certificate for #3736 ⟨a, b | abaabababa=a⟩

Back:⟨a, b | abaabababa=a⟩

Completion settings:

[1] abaabababa=a

Axiom: abaabababa=a.

Referenced by [2], [3].

[2] abaababa=aabababa

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

abaabab aba abaabababa

Critical pair: abaababa=aabababa.

Referenced by [3], [4].

[3] aababababa=a

Overlap of [1] abaabababa=a with [2] abaababa=aabababa:

abaabababa abaababa

Critical pair: aababababa=a.

Defines rule #2.

Referenced by [4].

[4] abaa=aaba

Overlap of [2] abaababa=aabababa with [2] abaababa=aabababa:

abaab aba abaababa

Critical pair: abaabaabababa=aabababaababa.

Reduce LHS:

[2]aba(abaababa)ba
[3]⇒ aba(aababababa)
⇒ abaa

Reduce RHS:

[2]aabab(abaababa)
[2]⇒ aab(abaababa)ba
[2]⇒ a(abaababa)baba
[3]⇒ a(aababababa)ba
⇒ aaba

Defines rule #1.