Certificate for #1699 ⟨a, b | aababbaab=a⟩

Back:⟨a, b | aababbaab=a⟩

Completion settings:

[1] aababbaab=a

Axiom: aababbaab=a.

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

[2] aababba=aabbaab

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

aababb aab aababbaab

Critical pair: aababba=aabbaab.

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

[3] aabbaabab=a

Overlap of [1] aababbaab=a with [2] aababba=aabbaab:

aababbaab aababba

Critical pair: aabbaabab=a.

Referenced by [4], [5].

[4] aabba=abaab

Overlap of [1] aababbaab=a with [2] aababba=aabbaab:

aababb aab aababba

Critical pair: aababbaabbaab=aabba.

Reduce LHS:

[2](aababba)abbaab
[3]⇒ (aabbaabab)baab
⇒ abaab

Flip LHS and RHS.

Defines rule #1.

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

[5] abaababab=a

Simplify [3] aabbaabab=a.

Reduce LHS:

[4](aabba)abab
⇒ abaababab

Defines rule #4.

Referenced by [6].

[6] aaababab=abaababa

Overlap of [1] aababbaab=a with [5] abaababab=a:

aababba ab abaababab

Critical pair: aababbaa=aaababab.

Reduce LHS:

[2](aababba)a
[4]⇒ (aabba)aba
⇒ abaababa

Flip LHS and RHS.

Defines rule #3.

[7] aababba=abaabab

Simplify [2] aababba=aabbaab.

Reduce RHS:

[4](aabba)ab
⇒ abaabab

Defines rule #2.