[Termtools] Scoring for complexity

Dear all,

scoring for complexity categories was discussed among SC and changed as follows. - Providing upper bound n^u will be given score 1 + 0.5^u. - Providing lower bound n^l will be given score 1 - 0.5^l.

Intuitively, as the upper bound goes up, the score goes down towards 1 (terminating), and as the lower bound goes up, the score goes up towards 1 (nonterminating).

The maximum score is 2, and is achieved by proving tight bounds (u = l). The only exception is NON_POLY lower bound, which is given score 1, hypothetically reserving 1 for a termination proof.

Best, Akihisa