Certificate for #3613 ⟨a, b | aababbbaab=a⟩

Back:⟨a, b | aababbbaab=a⟩

Completion settings:

[1] aababbbaab=a

Axiom: aababbbaab=a.

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

[2] aababbba=aabbbaab

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

aababbb aab aababbbaab

Critical pair: aababbba=aabbbaab.

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

[3] aabbbaabab=a

Overlap of [1] aababbbaab=a with [2] aababbba=aabbbaab:

aababbbaab aababbba

Critical pair: aabbbaabab=a.

Referenced by [4], [5].

[4] aabbba=abbaab

Overlap of [1] aababbbaab=a with [2] aababbba=aabbbaab:

aababbb aab aababbba

Critical pair: aababbbaabbbaab=aabbba.

Reduce LHS:

[2](aababbba)abbbaab
[3]⇒ (aabbbaabab)bbaab
⇒ abbaab

Flip LHS and RHS.

Defines rule #1.

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

[5] abbaababab=a

Simplify [3] aabbbaabab=a.

Reduce LHS:

[4](aabbba)abab
⇒ abbaababab

Defines rule #5.

Referenced by [6], [7].

[6] abaababab=abbaababa

Overlap of [1] aababbbaab=a with [5] abbaababab=a:

aababbba ab abbaababab

Critical pair: aababbbaa=abaababab.

Reduce LHS:

[2](aababbba)a
[4]⇒ (aabbba)aba
⇒ abbaababa

Flip LHS and RHS.

Defines rule #4.

Referenced by [7].

[7] aaababab=abaababa

Overlap of [1] aababbbaab=a with [6] abaababab=abbaababa:

aababbba ab abaababab

Critical pair: aababbbaabbaababa=aaababab.

Reduce LHS:

[2](aababbba)abbaababa
[4]⇒ (aabbba)ababbaababa
[5]⇒ (abbaababab)baababa
⇒ abaababa

Flip LHS and RHS.

Defines rule #3.

[8] aababbba=abbaabab

Simplify [2] aababbba=aabbbaab.

Reduce RHS:

[4](aabbba)ab
⇒ abbaabab

Defines rule #2.