Certificate for #4599 ⟨a, b | aabaaaba=aba⟩

Back:⟨a, b | aabaaaba=aba⟩

Completion settings:

[1] aabaaaba=aba

Axiom: aabaaaba=aba.

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

[2] abaaaba=aabaaba

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

aaba aaba aabaaaba

Critical pair: aabaaba=abaaaba.

Flip LHS and RHS.

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

[3] abaaba=aababa

Overlap of [2] abaaaba=aabaaba with [1] aabaaaba=aba:

aba aaba aabaaaba

Critical pair: abaaba=aabaabaaaba.

Reduce RHS:

[1]aab(aabaaaba)
⇒ aababa

Defines rule #1.

Referenced by [4], [5].

[4] aaaababa=aba

Overlap of [1] aabaaaba=aba with [2] abaaaba=aabaaba:

a abaaaba abaaaba

Critical pair: aaabaaba=aba.

Reduce LHS:

[3]aa(abaaba)
⇒ aaaababa

Defines rule #3.

[5] abaaaba=aaababa

Simplify [2] abaaaba=aabaaba.

Reduce RHS:

[3]a(abaaba)
⇒ aaababa

Defines rule #2.