Certificate for #739 ⟨a, b | aaaaabaa=a

Completion settings:

[1] aaaaabaa=a

Axiom: aaaaabaa=a.

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

[2] aaaabaa=aaaaaba

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

aaaaab aa aaaaabaa

Critical pair: aaaaaba=aaaabaa.

Flip LHS and RHS.

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

[3] aaabaa=aaaaba

Overlap of [1] aaaaabaa=a with [2] aaaabaa=aaaaaba:

aaaaab aa aaaabaa

Critical pair: aaaaabaaaaaba=aaabaa.

Reduce LHS:

[1](aaaaabaa)aaaba
aaaaba

Flip LHS and RHS.

Referenced by [5].

[4] aabaa=aaaba

Overlap of [2] aaaabaa=aaaaaba with [2] aaaabaa=aaaaaba:

aaaab aa aaaabaa

Critical pair: aaaabaaaaaba=aaaaabaaabaa.

Reduce LHS:

[2](aaaabaa)aaaba
[1](aaaaabaa)aaba
aaaba

Reduce RHS:

[1](aaaaabaa)abaa
aabaa

Flip LHS and RHS.

Referenced by [5].

[5] abaa=aaba

Overlap of [4] aabaa=aaaba with [1] aaaaabaa=a:

aab aa aaaaabaa

Critical pair: aaba=aaabaaaabaa.

Reduce RHS:

[3](aaabaa)aabaa
[2](aaaabaa)abaa
[1](aaaaabaa)baa
abaa

Flip LHS and RHS.

Defines rule #1.

[6] aaaaaaba=a

Overlap of [1] aaaaabaa=a with [2] aaaabaa=aaaaaba:

a aaaabaa aaaabaa

Critical pair: aaaaaaba=a.

Defines rule #2.