Certificate for #4191 ⟨a, b | aabbbaaab=ab⟩

Back:⟨a, b | aabbbaaab=ab⟩

Completion settings:

[1] aabbbaaab=ab

Axiom: aabbbaaab=ab.

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

[2] abbbaaab=aabbbaab

Overlap of [1] aabbbaaab=ab with [1] aabbbaaab=ab:

aabbba aab aabbbaaab

Critical pair: aabbbaab=abbbaaab.

Flip LHS and RHS.

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

[3] abbbaab=aabbbab

Overlap of [2] abbbaaab=aabbbaab with [1] aabbbaaab=ab:

abbba aab aabbbaaab

Critical pair: abbbaab=aabbbaabbbaaab.

Reduce RHS:

[1]aabbb(aabbbaaab)
⇒ aabbbab

Defines rule #1.

Referenced by [4], [5].

[4] aaaabbbab=ab

Overlap of [1] aabbbaaab=ab with [2] abbbaaab=aabbbaab:

a abbbaaab abbbaaab

Critical pair: aaabbbaab=ab.

Reduce LHS:

[3]aa(abbbaab)
⇒ aaaabbbab

Defines rule #3.

[5] abbbaaab=aaabbbab

Simplify [2] abbbaaab=aabbbaab.

Reduce RHS:

[3]a(abbbaab)
⇒ aaabbbab

Defines rule #2.