Certificate for #926 ⟨a, b | aabaaab=ab⟩

Back:⟨a, b | aabaaab=ab⟩

Completion settings:

[1] aabaaab=ab

Axiom: aabaaab=ab.

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

[2] abaaab=aabaab

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

aaba aab aabaaab

Critical pair: aabaab=abaaab.

Flip LHS and RHS.

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

[3] abaab=aabab

Overlap of [2] abaaab=aabaab with [1] aabaaab=ab:

aba aab aabaaab

Critical pair: abaab=aabaabaaab.

Reduce RHS:

[1]aab(aabaaab)
⇒ aabab

Defines rule #1.

Referenced by [4], [5].

[4] aaaabab=ab

Overlap of [1] aabaaab=ab with [2] abaaab=aabaab:

a abaaab abaaab

Critical pair: aaabaab=ab.

Reduce LHS:

[3]aa(abaab)
⇒ aaaabab

Defines rule #3.

[5] abaaab=aaabab

Simplify [2] abaaab=aabaab.

Reduce RHS:

[3]a(abaab)
⇒ aaabab

Defines rule #2.