Proof that pedersen-segment-scalar is not 0.
This is proved by first proving that
the loop function is outside the interval
between
The fact, mentioned above, that the loop function is outside a certain interval is also useful to prove other properties. Thus, we export a theorem asserting that.
Theorem:
(defthm pedersen-segment-scalar-loop-outside-interval (implies (and (posp j) (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (or (<= (pedersen-segment-scalar-loop j segment) (- (expt 2 (+ -4 (* 4 j))))) (<= (expt 2 (+ -4 (* 4 j))) (pedersen-segment-scalar-loop j segment)))))
Theorem:
(defthm pedersen-segment-scalar-not-zero (implies (and (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (not (equal (pedersen-segment-scalar segment) 0))) :rule-classes :type-prescription)