Certificate for #821 ⟨a, b | aabbbaab=a⟩

Back:⟨a, b | aabbbaab=a⟩

Completion settings:

[1] aabbbaab=a

Axiom: aabbbaab=a.

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

[2] aabbba=abbaab

Overlap of [1] aabbbaab=a with [1] aabbbaab=a:

aabbb aab aabbbaab

Critical pair: aabbba=abbaab.

Defines rule #1.

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

[3] abbaabab=a

Overlap of [1] aabbbaab=a with [2] aabbba=abbaab:

aabbbaab aabbba

Critical pair: abbaabab=a.

Defines rule #4.

Referenced by [4], [5].

[4] abaabab=abbaaba

Overlap of [1] aabbbaab=a with [3] abbaabab=a:

aabbba ab abbaabab

Critical pair: aabbbaa=abaabab.

Reduce LHS:

[2](aabbba)a
⇒ abbaaba

Flip LHS and RHS.

Defines rule #3.

Referenced by [5].

[5] aaabab=abaaba

Overlap of [1] aabbbaab=a with [4] abaabab=abbaaba:

aabbba ab abaabab

Critical pair: aabbbaabbaaba=aaabab.

Reduce LHS:

[2](aabbba)abbaaba
[3]⇒ (abbaabab)baaba
⇒ abaaba

Flip LHS and RHS.

Defines rule #2.