Lines Matching defs:x0
421 F x0 (choose_x)
1025 val x0 = genvar int_ty
1026 val Fx0 = mk_comb(F, x0)
1030 (MP (SPECL [F, delta_tm, x0] top_and_lessers)
1035 (MP (SPECL [F, delta_tm, x0] bot_and_greaters)
1038 (* this looks like: .. |- !c. 0 < c ==> F (x0 - c * d) *)
1054 specialise can_get_small with [y, x0, d] and MP with zero_lt_delta
1055 (little_c_ex) |- ?c. 0 < c /\ x0 - c * d < y
1058 MP (SPECL [y, x0, delta_tm] can_become_extreme) zero_lt_delta
1061 (choose_u) . |- 0 < u /\ x0 - u * d < y
1065 (x0_less_ud) . |- x0 - u * d < y
1077 (Fx0_less_ud) . |- F (x0 - u * d)
1080 (* SPEC choose_lemma with x0 - u * d and MP with x0_less_ud to get
1081 (Fneginf_x0_less_ud) . |- F (x0 - u * d) = neginf (x0 - u * d)
1088 (neginf_x0_less_ud) . |- neginf (x0 - u * d)
1094 so specialise this with x0 - u * d and delta_tm, and then MP with
1096 (exists_small_k) |- ?k. 0 < x0 - u * d - k * d /\
1097 x0 - u * d - k * d <= d
1103 (choose_k) |- 0 < x0 - u * d - k * d /\ x0 - u*d - k*d <= d
1123 (* choose on x0 to get an existential assumption *)
1124 val res4 = CHOOSE (x0, ASSUME (mk_exists(Bvar, Fx))) res3