Certificate for #801 ⟨a, b | aababaab=a

Completion settings:

[1] aababaab=a

Axiom: aababaab=a.

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

[2] aababa=aabaab

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

aabab aab aababaab

Critical pair: aababa=aabaab.

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

[3] aabaabab=a

Overlap of [1] aababaab=a with [2] aababa=aabaab:

aababaab aababa

Critical pair: aabaabab=a.

Referenced by [4].

[4] aaba=aaab

Overlap of [1] aababaab=a with [2] aababa=aabaab:

aabab aab aababa

Critical pair: aababaabaab=aaba.

Reduce LHS:

[2](aababa)abaab
[3](aabaabab)aab
aaab

Flip LHS and RHS.

Defines rule #1.

Referenced by [5], [6].

[5] aaabbaab=a

Overlap of [1] aababaab=a with [4] aaba=aaab:

aababaab aaba

Critical pair: aaabbaab=a.

Referenced by [7].

[6] aaabba=aaaabb

Overlap of [2] aababa=aabaab with [4] aaba=aaab:

aababa aaba

Critical pair: aaabba=aabaab.

Reduce RHS:

[4](aaba)ab
[4]a(aaba)b
aaaabb

Defines rule #2.

Referenced by [7].

[7] aaaaabbb=a

Simplify [5] aaabbaab=a.

Reduce LHS:

[6](aaabba)ab
[6]a(aaabba)b
aaaaabbb

Defines rule #3.