Certificate for #1982 ⟨a, b | aabbaaab=ab⟩

Back:⟨a, b | aabbaaab=ab⟩

Completion settings:

[1] aabbaaab=ab

Axiom: aabbaaab=ab.

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

[2] abbaaab=aabbaab

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

aabba aab aabbaaab

Critical pair: aabbaab=abbaaab.

Flip LHS and RHS.

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

[3] abbaab=aabbab

Overlap of [2] abbaaab=aabbaab with [1] aabbaaab=ab:

abba aab aabbaaab

Critical pair: abbaab=aabbaabbaaab.

Reduce RHS:

[1]aabb(aabbaaab)
⇒ aabbab

Defines rule #1.

Referenced by [4], [5].

[4] aaaabbab=ab

Overlap of [1] aabbaaab=ab with [2] abbaaab=aabbaab:

a abbaaab abbaaab

Critical pair: aaabbaab=ab.

Reduce LHS:

[3]aa(abbaab)
⇒ aaaabbab

Defines rule #3.

[5] abbaaab=aaabbab

Simplify [2] abbaaab=aabbaab.

Reduce RHS:

[3]a(abbaab)
⇒ aaabbab

Defines rule #2.