Lines Matching defs:delta
212 the above forms, call it delta *)
221 val delta = if null all_deltas then Arbint.one else lcml all_deltas
222 val delta_tm = term_of_int delta
231 c int_divides (x +/- y * delta + e) to
233 given that c is a divisor of delta. We first reduce
334 assumption: ?c. (0 < c /\ c <= delta) /\ neginf(c)
335 lemma2: !x y. neginf(x - y * delta) = neginf(x)
340 y, c and delta
342 0 < delta ==> ?e. 0 < e /\ c - e * delta < y
343 discharge 0 < delta to get
344 ?e. 0 < e /\ c - e * delta < y
346 c - e * delta < y (2)
348 neginf(c - e * delta) = neginf(c) (3)
350 F(c - e * delta) = neginf(c - e * delta) (4)
352 F(c - e * delta) = neginf(c) (5)
354 F(c - e * delta) (6)
425 !x. F x ==> F (x - delta)
430 |- !b j. MEM b [b1; b2; .. bn] /\ 0 < j /\ j <= delta ==>
436 expand out F(x - delta) (i.e. do a BETA_CONV) and traverse this
438 a F(x) theorem and a F(x - delta) term and produces a theorem