Certificate for #1936 ⟨a, b | aabaaaab=ab⟩

Back:⟨a, b | aabaaaab=ab⟩

Completion settings:

[1] aabaaaab=ab

Axiom: aabaaaab=ab.

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

[2] abaaaab=aabaaab

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

aabaa aab aabaaaab

Critical pair: aabaaab=abaaaab.

Flip LHS and RHS.

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

[3] abaaab=aabaab

Overlap of [2] abaaaab=aabaaab with [1] aabaaaab=ab:

abaa aab aabaaaab

Critical pair: abaaab=aabaaabaaaab.

Reduce RHS:

[1]aaba(aabaaaab)
⇒ aabaab

Referenced by [4], [5], [6], [7].

[4] abaab=aabab

Overlap of [3] abaaab=aabaab with [1] aabaaaab=ab:

aba aab aabaaaab

Critical pair: abaab=aabaabaaaab.

Reduce RHS:

[1]aab(aabaaaab)
⇒ aabab

Defines rule #1.

Referenced by [5], [6], [7].

[5] aaaaabab=ab

Overlap of [1] aabaaaab=ab with [2] abaaaab=aabaaab:

a abaaaab abaaaab

Critical pair: aaabaaab=ab.

Reduce LHS:

[3]aa(abaaab)
[4]⇒ aaa(abaab)
⇒ aaaaabab

Defines rule #4.

[6] abaaaab=aaaabab

Simplify [2] abaaaab=aabaaab.

Reduce RHS:

[3]a(abaaab)
[4]⇒ aa(abaab)
⇒ aaaabab

Defines rule #3.

[7] abaaab=aaabab

Simplify [3] abaaab=aabaab.

Reduce RHS:

[4]a(abaab)
⇒ aaabab

Defines rule #2.