Quelle trk_bands_2D.prf
Sprache: Lisp
(trk_bands_2Dnil 3460312877"" (skeep)"" (expand "trk_line_eps_irt" )"" (expand "tangent_line" )"" (lift-if)"" (split -1)"1" (flatten)"1" "trk_line" "trk_only_line(Qs(ss,eps),vo,vi,irt)" :hide? nil )"1" (expand "trk_only_line" )"1" (lift-if)"1" (split -1)"1" (flatten)"1" "rr" "root2b(sqv(Qs(ss, eps)), Qs(ss, eps) * vi, sqv(vi) - sqv(vo),irt)" )"1" (hide -1)"1" (replaces -1 :dir rl)"1" assert )"1" "1" rewrite "det_add_left" )"1" rewrite "det_scal_left" )"1" assert )"1" "1" "eps * det(vi, ss) - det(vi, ss) * eps = 0" )"1" "1" rewrite "det_asym" )"1" rewrite "det_s_Qs" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -1 :dir rl)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (typepred "nvo" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil )NOT const-decl "[bool -> bool]" booleans nil )"posreal" vectors_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"real" quadratic_2b "reals/" )"real" quadratic_2b "reals/" )nil reals nil )"real" reals nil )nil det_2D "vectors/" )"real" det_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )nil tangent_line nil )"nnreal" nil )"Sign" sign "reals/" )nil real_props nil )nil real_props nil )nil extra_tegies nil )nil extra_tegies nil )"real" reals nil )nil det_2D "vectors/" )"real" reals nil )nil det_2D "vectors/" )"real" reals nil )"Vect2" tangent_line nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"{k: real, nvo: Vect2 | AND k * vnz = nvo - vi}" nil )"posreal" trk_bands_2D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" definitions nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D_def "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Nz_vect2" trk_bands_2D nil )"Nz_vect2" tangent_line nil ))nil ))nil 3459317738"" (skeep)"" (expand "trk2v2" )"" (expand "trkgs2vect" )"" (rewrite "scal_scal_cont_rv" )"" (hide 2)"" (rewrite "pair_cont_rv" )"1" (rewrite "cos_cont_fun" ) nil nil )"2" (rewrite "sin_cont_fun" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"(trk_only?(vo2))" bands_util nil )nil vect2_cont_dot"vect_analysis/" )nil vectors_2D_def "vectors/" )nil booleans nil )"bool" cont_real_vect2 "vect_analysis/" )"real" sincos_def "trig_fnd/" )"real" sincos_def "trig_fnd/" )nil vectors_2D "vectors/" )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil continuous_functions"analysis/" )"bool" continuous_functions "analysis/" )nil vect_cont_2D "vect_analysis/" )nil sincos "trig_fnd/" )nil sincos "trig_fnd/" )"Nz_vect2" track nil ))nil )nil 3459317725 ("" (judgement-tcc) nil nil ) nil nil ))nil 3443464664"" (skeep)"" (expand "Vtrk" )"" (rewrite "sub_cont_rv" )"1" (hide 2) (("1" (rewrite "const_cont_rv" ) nil nil )) nil )"2" (hide 2)"2" "(LAMBDA (trk: real): trk2v2(vo)(trk)) = trk2v2(vo)" )"1" (assert ) nil nil )"2" (decompose-equality 1) nil nil ))nil ))nil ))nil ))nil ))nil )"Vect2" bands_util nil )"continuous_rv_fun" nil )"[T, T -> boolean]" equalities nil )nil vect_cont_2D "vect_analysis/" )"(trk_only?(vo2))" bands_util nil )"bool" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil cont_real_vect2"vect_analysis/" )"bool" cont_real_vect2 "vect_analysis/" )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vect_cont_2D "vect_analysis/" )"Nz_vect2" bands_util nil ))nil 3459203874"" (skeep)"" (expand "Omega_trk_spc" )"" (rewrite "sub_cont" )"1" (rewrite "const_cont" ) nil nil )"2" (rewrite "dot_cont_rr" )"1" "(LAMBDA(trk):trk2v2(vo)(trk))=trk2v2(vo)" )"1" (assert ) nil nil )"2" (decompose-equality 1) nil nil ))nil )"2" (rewrite "const_cont_rv" ) nil nil ))nil ))nil ))nil ))nil )"posreal" sq "reals/" )"real" reals nil )"real" trk_bands_2D nil )"Nz_vect2" bands_util nil )"bool" cont_real_vect2 "vect_analysis/" )nil vect2_cont_dot "vect_analysis/" )"odd_int" integers nil )"continuous_rv_fun" nil )"[T, T -> boolean]" equalities nil )nil vect_cont_2D "vect_analysis/" )nil continuous_lambda "analysis/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" trk_bands_2D nil )nil real_types nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )"(trk_only?(vo2))" bands_util nil )"bool" definitions nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )"real" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil continuous_functions"analysis/" )"bool" continuous_functions "analysis/" )nil booleans nil )nil continuous_lambda "analysis/" )"posreal" nil ))nil )nil 3459203808 ("" (judgement-tcc) nil nil ) nil nil ))nil 3467987873"" (skeep)"" (expand "trk_special_case?" )"" (typepred "trk2v2(vo)(trk)" )"" (expand "trk_only?" )"" (rewrite "norms_eq_sqv" )"" (replaces -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" trk_only nil )"Nz_vector" vectors_2D "vectors/" )"posreal" sq "reals/" )"posreal" nil )"posreal" vectors_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"continuous_rv_fun" nil )nil vectors_2D "vectors/" )"Nz_vect2" bands_util nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )"bool" definitions nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"(trk_only?(vo2))" bands_util nil ))nil ))"" 3504829738"" (skeep)"" (case "sqv(s)<sq(D)" )"1" (expand "trk_special_case?" )"1" (expand "Omega_trk_spc" )"1" (mult-by -2 "sq(t)" )"1" (rewrite "sq_div" )"1" (assert )"1" (real-props)"1" (flatten)"1" case "sq(t) * (vi * trk2v2(vo)(trk)) = t*(s*trk2v2(vo)(trk))" )"1" (replace -1)"1" (hide -1)"1" (both-sides "+" "sq(D)" -1)"1" (assert )"1" "sq_eq" )"1" "1" "1" "1" "1" rewrite "sq_times" )"1" "vectors_2D.cauchy_schwarz" )"1" "1" case "sqv(trk2v2(vo)(trk)) = sqv(vo)" )"1" replace -1)"1" "sq(t)" )"1" replace -3)"1" "sq(D)" )"1" expand "sq" )"1" assert )"1" "t * t" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "trk2v2" )"2" "norm_id" )"2" "norm(vo)" "trk" )"2" "sq_eq" )"2" "2" "2" "2" "1" rewrite "sq_norm" )"1" rewrite "sq_norm" )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -3 +)"2" (expand "sq" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"posreal" trk_bands_2D nil )nil real_types nil )"bool" reals nil )"nonneg_real" sq "reals/" )nil real_types nil )nil vectors_2D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil vectors_2D "vectors/" )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" sq "reals/" )"real" trk_bands_2D nil )nil sq "reals/" )nil real_props nil )nil real_props nil )nil real_props nil )"posreal" vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil sq "reals/" )"posreal" vectors_2D"vectors/" )"nnreal" vectors_2D "vectors/" )"Nz_vect2" track nil )nil vectors_2D "vectors/" )nil track nil )"(total_order?[real])" nil )nil real_props nil )nil extra_real_propsnil )nil vectors_2D "vectors/" )nil sq "reals/" )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"real" reals nil )"odd_int" integers nil )nil vectors_2D "vectors/" )"real" reals nil )"Nz_vect2" bands_util nil )"continuous_rv_fun" nil )"posreal" nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(total_order?[real])" nil )"Nz_vector" vectors_2D "vectors/" )"posreal" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" definitions nil )"(trk_only?(vo2))" bands_util nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil extra_real_props nil )"real" reals nil )"bool" trk_only nil )"({f | continuous?(f)})" nil ))nil 3476810585"" (skeep)"" (case "sqv(s)<sq(D)" )"1" (expand "trk_special_case?" )"1" (expand "Omega_trk_spc" )"1" (mult-by -2 "sq(t)" )"1" (rewrite "sq_div" )"1" (assert )"1" (real-props)"1" (flatten)"1" case "sq(t) * (vi * trk2v2(vo)(trk)) = t*(s*trk2v2(vo)(trk))" )"1" (replace -1)"1" (hide -1)"1" (both-sides "+" "sq(D)" -1)"1" (assert )"1" "sq_eq" )"1" "1" "1" "1" "1" rewrite "sq_times" )"1" "vectors_2D.cauchy_schwarz" )"1" "1" case "sqv(trk2v2(vo)(trk)) = sqv(vo)" )"1" replace -1)"1" "sq(t)" )"1" replace -3)"1" "sq(D)" )"1" expand "sq" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "trk2v2" )"2" "norm_id" )"2" "norm(vo)" "trk" )"2" "sq_eq" )"2" "2" "2" "2" "1" rewrite "sq_norm" )"1" rewrite "sq_norm" )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -3 +)"2" (expand "sq" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"bool" trk_only nil )"(trk_only?(vo2))" bands_util nil )"bool" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"Nz_vector" vectors_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"Nz_vect2" bands_util nil )nil vectors_2D "vectors/" )nil sq "reals/" )nil vectors_2D "vectors/" )nil track nil )nil vectors_2D "vectors/" )"Nz_vect2" track nil )"nnreal" vectors_2D "vectors/" )"posreal" vectors_2D"vectors/" )nil sq "reals/" )"posreal" vectors_2D "vectors/" )nil sq "reals/" )"posreal" sq "reals/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"nonneg_real" sq "reals/" ))nil ))nil 3476809011"" (skeep)"" (lemma "Omega_trk_spc_separated" )"" (inst - "s" "t" "trk" "vi" "vo" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil trk_bands_2D nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(total_order?[real])" nil )"({f | continuous?(f)})" nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D_def "vectors/" )nil reals nil ))nil ))nil 3467987851"" (skeep)"" (lemma "Omega_trk_spc_separated" )"" (inst - "s" "t" "trk" "vi" "vo" )"" (assert )"" (lemma "trk_spc_line_solution" )"" (inst - "s" "t" "vi" "trk2v2(vo)(trk)" )"" (expand "Vtrk" )"" (ground)"1" (lemma "trk_special_case_invariant" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (lemma "trk_spc_dot" )"2" (expand "Omega_trk_spc" )"2" "trk2v2(vo)(trk)" "s" "t" "vi" "vo" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trk_bands_2D nil )"({f | continuous?(f)})" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"(total_order?[real])" nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"bool" definitions nil )"(trk_only?(vo2))" bands_util nil )"Nz_vect2" bands_util nil )"continuous_rv_fun" nil )nil trk_bands_2D nil )"real" trk_bands_2D nil )"posreal" nil )"real" reals nil )nil trk_only nil )"Vect2" bands_util nil )"posreal" trk_bands_2D nil )nil trk_only nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D_def "vectors/" )nil reals nil ))nil )nil 3459191518"" (lemma "trk_spc_line_solution" )"" (skeep)"" (expand "Vtrk" )"" (inst - "sp" "T" "vi" "trk2v2(vo)(trk)" )"" (ground)"1" (postpone) nil nil )"2" (expand "Omega_trk_spc" )"2" (lemma "trk_spc_dot" )"2" (inst - "trk2v2(vo)(trk)" "sp" "T" "vi" "vo" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" definitions nil )nil sign "reals/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"posreal" sq "reals/" ))nil 3476631150"" (skeep)"" (name-replace "v" "Vtrk(vo,vi)(trk)" :hide? nil )"" (case "sqv(s+T*v)=sq(D)" )"1" (expand "trk_special_case?" )"1" (flatten)"1" (split)"1" (flatten)"1" (expand "conflict_2D?" )"1" (skolem -2 "tt" )"1" (typepred "tt" )"1" (lemma "horizontal_entry_le" )"1" (inst -1 "s" "tt" "T" "v" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (case-replace "v=zero" )"1" (assert ) nil nil )"2" (lemma "not_horizontal_entry_lt" )"2" (inst -1 "v" "s" "T" )"1" (skoletin -1)"1" (assert )"1" (flatten)"1" (expand "conflict_2D?" )"1" "max(t1,B)" )"1" expand "max" +)"1" "1" "1" "strictly_convex_btw_pt_lt" )"1" "horiz_dist_strictly_convex_scaf" )"1" "s" "v" )"1" assert )"1" "t1" "T" "0" "LAMBDA (trt: real): horiz_dist_scaf(s)(trt, v)" "B" )"1" assert )"1" expand "horiz_dist_scaf" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "max" +)"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "Vtrk" )"2" (lemma "trk_spc_on_D" )"2" (inst?)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )nil vectors_2D_def "vectors/" )nil booleans nil )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vect2" bands_util nil )nil trk_only nil )"(trk_only?(vo2))" bands_util nil )"bool" definitions nil )"Nz_vect2" bands_util nil )"continuous_rv_fun" nil )"bool" trk_only nil )"bool" cd2d nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil Lookahead nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"continuous_rv_fun" nil )"Nz_vector" vectors_2D "vectors/" )"posreal" vectors_2D "vectors/" )"posreal" nil )nil horizontal nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vect2" trk_bands_2D nil )"(strict_total_order?[real])" real_props nil )nil nil )"real" horizontal_dist_convexity nil )nil convex_functions"reals/" )"{p: real | p >= 0 AND p >= horizontal_tca(s, v)}" trk_bands_2Dnil )"Vect2" trk_bands_2D nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"bool" reals nil )"real" vectors_2D "vectors/" )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[bool, bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" definitions nil )"[bool, bool -> bool]" booleans nil )nil horizontal nil )"posreal" sq "reals/" )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil )"nonneg_real" sq "reals/" )"posreal" trk_bands_2D nil ))nil ))nil 3476631820"" (skeep)"" (name-replace "v" "Vtrk(vo,vi)(trk)" :hide? nil )"" (lemma "on_D_conflict" )"" (inst?)"" (split -1)"1" (replace -1)"1" (hide-all-but 1) (("1" (ground) nil nil )) nil ))nil )"2" (expand "Vtrk" )"2" (lemma "trk_spc_on_D" )"2" (inst?)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )nil vectors_2D_def "vectors/" )nil booleans nil )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vect2" bands_util nil )"(strict_total_order?[real])" real_props nil )"continuous_rv_fun" nil )"Nz_vect2" bands_util nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"bool" definitions nil )"(trk_only?(vo2))" bands_util nil )nil trk_only nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil cd2d nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trk_bands_2D nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil ))nil ))nil 3476636132"" (skeep)"" (lemma "trk_special_case_conflict_T" )"" (inst?)"" (assert )"" (split 1)"1" (flatten)"1" (assert )"1" (hide -2)"1" (expand "Omega_trk_spc" )"1" (expand "Vtrk" )"1" (expand "trk_special_case?" )"1" (flatten)"1" (hide 1)"1" (replace -4 :dir rl)"1" "1" "w" "trk2v2(vo)(trk)" )"1" replace -1)"1" case "sqv(vo) = sqv(w)" )"1" "1" replace -4)"1" "1" replace -1)"1" "1" "T" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk2v2(vo)(trk)" )"2" expand "trk_only?" )"2" "vectors_2D.sq_norm" )"2" "trk2v2(vo)(trk)" )"2" "vo" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -2)"2" (expand "trk_special_case?" )"2" (flatten)"2" (expand "Omega_trk_spc" )"2" (replace -2)"2" (replace -3 :dir rl)"2" (name "w" "trk2v2(vo)(trk)" )"2" replace -1)"2" case "sqv(vo) = sqv(w)" )"1" replace -1)"1" expand "Vtrk" )"1" replace -2)"1" "1" "T" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "trk2v2(vo)(trk)" )"2" expand "trk_only?" )"2" "vectors_2D.sq_norm" )"2" "trk2v2(vo)(trk)" )"2" "vo" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trk_bands_2D nil )"continuous_rv_fun" nil )"({f | continuous?(f)})" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )"Vect2" bands_util nil )"Nz_vect2" bands_util nil )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" definitions nil )"(trk_only?(vo2))" bands_util nil )"posreal" vectors_2D "vectors/" )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"real" reals nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"real" reals nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"nnreal" nil )"Nz_vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"continuous_rv_fun" nil )"posreal" vectors_2D"vectors/" )nil vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" trk_only nil )"real" trk_bands_2D nil )"posreal" sq "reals/" )"(total_order?[real])" nil )"real" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D_def "vectors/" )nil reals nil )"odd_int" integers nil ))nil ))nil 3476636249"" (skeep)"" (lemma "trk_special_case_conflict_B" )"" (inst?)"" (assert )"" (hide -2)"" (split 1)"1" (flatten)"1" (assert )"1" (hide -2)"1" (expand "Omega_trk_spc" )"1" (expand "Vtrk" )"1" (expand "trk_special_case?" )"1" (flatten)"1" (hide 1)"1" replace -4 :dir rl)"1" "1" "w" "trk2v2(vo)(trk)" )"1" replace -1)"1" case "sqv(vo) = sqv(w)" )"1" "1" replace -4)"1" "1" replace -1)"1" "1" "B" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "trk2v2(vo)(trk)" )"2" expand "trk_only?" )"2" "vectors_2D.sq_norm" )"2" "trk2v2(vo)(trk)" )"2" "vo" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -2)"2" (expand "trk_special_case?" )"2" (flatten)"2" (expand "Omega_trk_spc" )"2" (replace -2)"2" (replace -3 :dir rl)"2" "w" "trk2v2(vo)(trk)" )"2" replace -1)"2" case "sqv(vo) = sqv(w)" )"1" replace -1)"1" expand "Vtrk" )"1" replace -2)"1" "1" "B" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "trk2v2(vo)(trk)" )"2" expand "trk_only?" )"2" "vectors_2D.sq_norm" )"2" "trk2v2(vo)(trk)" )"2" "vo" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trk_bands_2D nil )"continuous_rv_fun" nil )"({f | continuous?(f)})" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"posreal" sq "reals/" )"real" trk_bands_2D nil )"bool" trk_only nil )NOT const-decl "[bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"posreal" vectors_2D"vectors/" )"continuous_rv_fun" nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" reals nil )"real" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"nnreal" trk_bands_2D nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )"posreal" vectors_2D "vectors/" )"(trk_only?(vo2))" bands_util nil )"bool" definitions nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"Nz_vect2" bands_util nil )"real" reals nil )"Vect2" bands_util nil )nil extra_real_propsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D_def "vectors/" )nil reals nil ))nil ))nil 3444144010"" (skeep)"" (rewrite "comp_vr_rv_cont" )"" (lemma "omega_v2_continuous" )"" (hide 2)"" (inst?)"" (expand "continuous_vr?" )"" (expand "continuous?" )"" (expand "continuous?" )"" (expand "continuous_at?" )"" (expand "continuous_vr?" )"" (skeep)"" (inst - "x0" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" "1" "delta!1" )"1" "1" "x!1" )"1" expand "member" )"1" expand "ball" )"1" expand "real_dist" )"1" assert )"1" "dist_norm" )"1" "1" case "norm(x0-x!1) = norm(x!1-x0)" )"1" expand "abs" )"1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"continuous_rv_fun" nil )nil vect2_cont_comp "vect_analysis/" )nil vectors_2D_def "vectors/" )nil booleans nil )"bool" cont_real_vect2 "vect_analysis/" )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vect2" bands_util nil )"bool" cont_vect2_real "vect_analysis/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trk_bands_2D nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil )"real" omega_v2 nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" continuity_ms_def "analysis/" )"real" reals nil )"bool" cont_vect2_real "vect_analysis/" )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"Vect2" trk_bands_2D nil )"Vect2" trk_bands_2D nil )"set[T]" metric_spaces "analysis/" )"(strict_total_order?[real])" real_props nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"real" reals nil )"real" reals nil )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil distance_2D "vectors/" )"nnreal" real_metric_space "analysis/" )"bool" sets nil )"bool" continuity_ms_def "analysis/" )"bool" continuity_ms_def "analysis/" )nil omega_v2 nil ))nil )nil 3444143969 ("" (subtype-tcc) nil nil ) nil nil ))nil 3443205728"" (skeep)"" (expand "Omega_trk" )"" (expand "o" )"" (expand "Vtrk" )"" (lemma "omega_v2_critical_points" )"" (inst?)"" (assert )"" (expand "trk_critical?" )"" (flatten)"" (split -1)"1" (flatten)"1" (skeep -2)"1" (assert )"1" (lemma "trk_line_complete" )"1" "1" assert )"1" (inst 1 "eps" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "trk_only_circle_complete" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil )"3" (flatten)"3" (assert )"3" (lemma "trk_only_circle_complete" )"3" "1" "trk2v2(vo)(trk)" "s" "B" "vi" "vo" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"({f | continuous?(f)})" trk_bands_2D nil )"Vect2" bands_util nil )"(trk_only?(vo2))" bands_util nil )"bool" definitions nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"bool" trk_bands_2D nil )nil trk_line nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"(total_order?[real])" nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"odd_int" integers nil )nil trk_only nil )"Nz_vect2" bands_util nil )"continuous_rv_fun" nil )"(strict_total_order?[real])" real_props nil )nil omega_v2 nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trk_bands_2D nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil )"[T -> real]" vect2_cont_comp "vect_analysis/" ))nil ))nil 3460979611"" (skeep)"" (lemma "trk_line_eps_irt_tangent_line" )"" (inst?)"" (assert )"" (expand "tangent_line?" )"" (skeep -1)"" (case-replace "nnk=0" )"1" (assert ) (("1" (rewrite "sub_eq_zero" ) nil nil ))nil )"2" case "det(nvo-vi,ss) = det(nnk * tangent_line(ss, eps),ss)" )"1" (hide -2)"1" (rewrite "det_sub_left" )"1" (rewrite "det_scal_left" )"1" (mult-by -1 "eps" )"1" (assert )"1" case "nnk*(det(tangent_line(ss, eps), ss) * eps) > 0" )"1" (assert ) nil nil )"2" "2" "2" expand "tangent_line" )"2" rewrite "det_asym" )"2" "det_s_Qs_lt_0" )"2" "eps" "ss" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" trk_bands_2D nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trk_line nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"Nz_vect2" tangent_line nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" det_2D "vectors/" )nil det_2D "vectors/" )"real" reals nil )nil extra_real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"Vect2" tangent_line nil )nil det_2D "vectors/" )"Nz_vect2" trk_bands_2D nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil tangent_line nil )nil det_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" tangent_line nil )nil horizontal nil )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil 3460995654"" (skeep)"" (typepred "vo" )"" (typepred "ss" )"" (case "ss /= zero" )"1" (lemma "norm_eq_0" )"1" (inst-cp - "vo" )"1" (inst - "ss" )"1" (flatten)"1" (replace 1)"1" (replace 3) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"(total_order?[real])" nil )"posreal" sq "reals/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"nnreal" nil )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"posreal" trk_bands_2D nil )nil horizontal nil )"posreal" vectors_2D"vectors/" )"posreal" nil )"real" reals nil ))nil ))nil 3460995654"" (skosimp*)"" (expand "trk_line_eps_irt?" ) (("" (assert ) nil nil )) nil ))nil )"bool" trk_line nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"real" reals nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"posreal" nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3460995654"" (skosimp*)"" (expand "trk_line_eps_irt?" ) (("" (assert ) nil nil )) nil ))nil )"bool" trk_line nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"real" reals nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"posreal" nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3460995873"" (skeep)"" (beta)"" (flatten)"" (lemma "trk_line_sort_eps" )"" (inst-cp -1 "1" "irt1" "nvo1" "ss" "vi" "vo" )"" (assert )"" (inst -1 "-1" "irt2" "nvo2" "ss" "vi" "vo" )"" (assert )"" (expand "trk_line_eps_irt?" )"" (flatten)"" "trk_line_eps_irt(ss, vo, vi, 1, irt1)" )"" (assert )"" "trk_line_eps_irt(ss, vo, vi, -1, irt2)" )"" (assert )"" "" expand "trk_only?" )"" "ordered_eps_1" )"" "nvo1" "ss" "vi" )"" assert )"" "" "ordered_eps_neg_1" )"" "nvo2" "ss" "vi" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"real" reals nil )nil trk_bands_2D nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )nil track nil )nil track nil )"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil )"bool" definitions nil )nil horizontal nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" trk_line nil )nil horizontal nil )"posreal" trk_bands_2D nil )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" vectors_2D"vectors/" )"posreal" nil )"real" reals nil ))nil 3461083409"" (skosimp*)"" (expand "trk_line_eps_irt?" ) (("" (flatten) nil nil )) nil ))nil )"bool" trk_line nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"posreal" nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3461083409"" (skosimp*)"" (expand "trk_line_eps_irt?" ) (("" (flatten) nil nil )) nil ))nil )"bool" trk_line nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"posreal" nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3461083490"" (skeep)"" (beta)"" (flatten)"" (lemma "trk_line_sort_eps" )"" (inst-cp -1 "1" "-1" "nvo1" "ss" "vi" "vo" )"" (assert )"" (inst -1 "1" "1" "nvo2" "ss" "vi" "vo" )"" (assert )"" (lemma "trk_line_eps_irt_dot" )"" (inst -1 "1" "nvo1" "nvo2" "ss" "vi" "vo" )"" (assert )"" (mult-cases -5)"" (expand "trk_line_eps_irt?" )"" (flatten)"" "trk_line_eps_irt(ss, vo, vi, 1, -1)" )"" assert )"" "trk_line_eps_irt(ss, vo, vi, 1, 1)" )"" assert )"" expand "trk_only?" )"" "" " ordered_eps_1_dot_gt_0" )"" "nvo1" "ss" "vi" )"" "" assert )"" "" " ordered_eps_1_dot_lt_0" )"" "nvo2" "ss" "vi" )"" replace -4)"" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"real" reals nil )nil trk_bands_2D nil )"nzreal" real_typesnil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"real" vectors_2D "vectors/" )"nnreal" nil )nil track nil )nil track nil )"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil )"bool" definitions nil )nil horizontal nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" trk_line nil )nil trk_line nil )nil horizontal nil )"posreal" trk_bands_2D nil )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )"posreal" vectors_2D"vectors/" )"posreal" nil )"real" reals nil ))nil ))nil 3461087210"" (skosimp*)"" (expand "trk_line_eps_irt?" ) (("" (flatten) nil nil )) nil ))nil )"bool" trk_line nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"posreal" nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3461087210"" (skosimp*)"" (expand "trk_line_eps_irt?" ) (("" (flatten) nil nil )) nil ))nil )"bool" trk_line nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"posreal" nil )"posreal" vectors_2D"vectors/" ))nil ))nil 3461087322"" (skeep)"" (beta)"" (flatten)"" (lemma "trk_line_sort_eps" )"" (inst-cp -1 "1" "1" "nvo2" "ss" "vi" "vo" )"" (inst -1 "1" "-1" "nvo1" "ss" "vi" "vo" )"" (assert )"" (expand "trk_line_eps_irt?" )"" (flatten)"" "trk_line_eps_irt(ss, vo, vi, 1, -1)" )"" "trk_line_eps_irt(ss, vo, vi, 1, 1)" )"" (replaces (-7 -8) :dir rl)"" (assert )"" (expand "trk_only?" )"" "xx1" "to2pi(track(nvo1) - " nil )"" "xx2" "to2pi(track(nvo2) - " nil )"" case "xx2-xx1 > -pi AND xx2-xx1 < pi" )"1" "1" case "to2pi(xx1-xx2) = to2pi(track(nvo1)-track(nvo2))" )"1" "trkgs2vect_id" )"1" "nvo1" )"1" "nvo2" )"1" replace -1 5 :dir rl)"1" replace "1" expand "trkgs2vect" )"1" rewrite "det_scal_left" )"1" rewrite "det_scal_right" )"1" "norm(nvo1) * ") "1" "1" expand "det" "1" rewrite "sin_minus" "1" "sin_id_to2pi" )"1" "1" "1" rewrite "sin_id_to2pi" )"1" "1" "xx1 < xx2 IFF xx1 - xx2 < 0" )"1" "1" "1" "1" "yy" "xx1-xx2" )"1" "1" "1" "1" "sin_ge_0" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "sin_lt_0" )"2" "yy+2*pi" )"2" assert )"2" "sin_period" )"2" "yy" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "vectors_2D.norm_eq_0" )"2" "nvo1" )"2" "nvo2" )"2" assert )"2" "1" "1" "1" nil nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "to2pi_to2pi" )"2" "track(nvo1) - asin(det(vi, ss) / (norm(vo) * norm(ss))) - " "-to2pi(track(nvo2) - asin(det(vi, ss) / (norm(vo) * norm(ss))) ") "2" assert )"2" "2" "to2pi_to2pi_sub" )"2" "track(nvo2) - asin(det(vi, ss) / (norm(vo) * norm(ss))) " "track(nvo1) - asin(det(vi, ss) / (norm(vo) * norm(ss))) ") "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "ordered_eps_1_dot_le_0" )"1" "nvo1" "ss" "vi" )"1" "nvo2" "ss" "vi" )"1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ordered_eps_1_dot_ge_0" )"2" "nvo1" "ss" "vi" )"2" "nvo2" "ss" "vi" )"2" assert )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )"real" reals nil )"real" reals nil )nil trk_bands_2D nil )"odd_int" integers nil )"bool" trk_line nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil horizontal nil )"bool" definitions nil )"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil )nil real_props nil )"real" vectors_2D "vectors/" )"nnreal" nil )nil track nil )nil track nil )"real" reals nil )nil to2pi "trig_fnd/" )nil to2pi "trig_fnd/" )nil track nil )"Vector" vectors_2D "vectors/" )"real" sincos_def "trig_fnd/" )"real" sincos_def "trig_fnd/" )nil det_2D "vectors/" )"trig_range" sincos_def"trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )"[bool, bool -> bool]" booleans nil )nil to2pi "trig_fnd/" )nil real_props nil )nil trig_basic "trig_fnd/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )nil integers nil )nil trig_ineq "trig_fnd/" )nil trig_ineq "trig_fnd/" )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_types nil )nil real_types nil )nil real_props nil )"nzreal" nil )nil extra_tegies nil )nil extra_tegies nil )nil trig_basic "trig_fnd/" )nil vectors_2D "vectors/" )nil real_props nil )nil det_2D "vectors/" )"Nz_vect2" track nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" atan "trig_fnd/" )nil atan2 "trig_fnd/" )"nnreal_lt_2pi" to2pi "trig_fnd/" )"[numfield, numfield -> numfield]" number_fields nil )"nnreal_lt_2pi" track nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil asin "trig_fnd/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil asin "trig_fnd/" )"real_abs_le_pi2" asin "trig_fnd/" )"real" det_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nzreal" real_typesnil )nil horizontal nil )"posreal" trk_bands_2D nil )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"boolean" notequal nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" vectors_2D"vectors/" )"posreal" nil )"real" reals nil ))nil 3460208623"" (skeep)"" (expand "trk_line_eps_irt?" )"" (expand "trk_line_eps_irt" )"" (lift-if)"" (assert )"" (split -1)"1" (flatten)"1" "trko" "trk_only_line(tangent_line(ss, eps), vo, vi, irt)" nil )"1" (expand "trk_only_line" )"1" (lift-if)"1" (split -1)"1" (flatten)"1" (decompose-equality -2)"1" (replace -1)"1" "1" "kk" "trko`1" )"1" expand "tangent_line" )"1" expand "root2b" )"1" case "discr2b(sqv(Qs(ss, eps)), Qs(ss, eps) * vi, sqv(vi) - sqv(vo)) > 0" )"1" "dd" "discr2b(sqv(Qs(ss, eps)), Qs(ss, eps) * vi, sqv(vi) - sqv(vo))" )"1" "1" rewrite "sqv_Qs" )"1" rewrite "det_perpR" "1" "1" rewrite "det_add_right" )"1" rewrite "det_scal_right" )"1" expand "Qs" "1" rewrite "det_sub_right" )"1" rewrite "det_Q_s" )"1" rewrite "Q_eq_Qs_perp" )"1" rewrite "det_scal_left" )"1" rewrite "det_asym" )"1" rewrite "dot_perpR" "1" "sD2" "sqv(ss)-sq(D)" )"1" "1" assert )"1" "epsirt" "pm*(eps*irt)" )"1" "1" "1" expand "epsirt" )"1" rewrite "sq" "1" rewrite "dot_comm" )"1" "(sqrt(sD2) > 0 AND sD2 > 0)" )"1" "1" "QQ" "Qs(ss,eps)*vi" )"1" "(-((((QQ * D) * eps) * pm) * sD2) - ") "1" "1" "-sqrt(dd) * sqrt(sD2) * sqrt(sD2) * D * eps * irt * pm > 0 IFF (sqrt(sD2)*sqrt(sD2)*D*sqrt(dd))*(pm*(eps*irt)) < 0" )"1" "1" rewrite "sq" "1" case "(sD2 * D * sqrt(dd)) > 0" )"1" "1" "abc" "(sD2 * D * sqrt(dd))" )"1" nil nil ))nil ))nil )"2" "2" "2" "2" expand "sD2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "sD2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "discr2b" )"2" rewrite "sqv_Qs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (decompose-equality -1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" trk_line nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil vectors_2D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" definitions nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trk_bands_2D nil )"{k: real, nvo: Vect2 | AND k * vnz = nvo - vi}" nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"Nz_vect2" tangent_line nil )nil horizontal nil )"posreal" nil )"posreal" nil )"real" reals nil )"real" reals nil )nil tangent_line nil )nil det_2D "vectors/" )nil det_2D "vectors/" )nil det_2D "vectors/" )nil tangent_line nil )"nzreal" nil )"Sign" sign "reals/" )"Nz_vector" vectors_2D "vectors/" )nil det_2D "vectors/" )"real" reals nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"Sign" trk_bands_2D nil )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" trk_bands_2D nil )nil real_props nil )nil real_props nil )nil sqrt "reals/" )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )nil det_2D "vectors/" )"nnreal" nil )nil det_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"Vect2" perpendicular_2D "vectors/" )"nzreal" nil )nil tangent_line nil )nil det_2D "vectors/" )nil det_2D "vectors/" )"Vect2" tangent_line nil )"Vect2" tangent_line nil )nil reals nil )"real" quadratic_2b "reals/" )"real" quadratic_2b "reals/" )"real" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"Nz_vect2" trk_bands_2D nil )"real" reals nil )"real" reals nil )"posreal" vectors_2D "vectors/" )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"posreal" sq "reals/" )"posreal" nil )"(total_order?[real])" nil )"Nz_vect2" perpendicular_2D"vectors/" )"(strict_total_order?[real])" real_props nil )"Sign" sign "reals/" )"(divides(n))" divides nil )"(divides(m))" divides nil )"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil ))nil 3443226487"" (skeep)"" (rewrite "cd2d" :dir rl)"" (expand "trk_green?" )"" (split)"1" (flatten)"1" (skolem 2 "trk1" )"1" (case "trk_special_case?(s,vo,vi,T)" )"1" (lemma "trk_special_case_conflict_T" )"1" (inst-cp -1 "s" "trko" "vi" "vo" )"1" (inst -1 "s" "trk1" "vi" "vo" )"1" (assert )"1" (assert )"1" (hide (-3 2))"1" (lemma "IntermediateValue" )"1" "band" "Omega_trk_spc(vo,vi,T)" )"1" assert )"1" "1" "trko" "trk1" )"1" expand "Vtrk" )"1" "trk_spc_horizontal_dir" )"1" "Entry" "trk2v2(vo)(trko)" "s" "T" "vi" "vo" )"1" "Entry" "trk2v2(vo)(trk1)" "s" "T" "vi" "vo" )"1" assert )"1" "1" "1" expand "Omega_trk_spc" )"1" assert )nil nil ))nil )"2" expand "Omega_trk_spc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x" )"2" "2" "Omega_trk_spc_critical" )"2" "s" "T" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" "2" "x" )"2" expand "trk_critical?" )"2" "trk_line_complete" )"2" "2" "2" "Omega_trk_spc_separated" )"2" "s" "T" "x" "vi" "vo" )"2" assert )"2" assert )"2" expand "Vtrk" )"2" "eps" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "B>0 AND trk_special_case?(s,vo,vi,B)" )"1" (flatten)"1" (lemma "trk_special_case_conflict_B" )"1" (inst-cp -1 "s" "trko" "vi" "vo" )"1" (inst -1 "s" "trk1" "vi" "vo" )"1" (assert )"1" (lemma "IntermediateValue" )"1" "band" "Omega_trk_spc(vo,vi,B)" )"1" assert )"1" "1" "trko" "trk1" )"1" expand "Vtrk" )"1" "trk_spc_horizontal_dir" )"1" "Exit" "trk2v2(vo)(trko)" "s" "B" "vi" "vo" )"1" "Exit" "trk2v2(vo)(trk1)" "s" "B" "vi" "vo" )"1" assert )"1" "1" expand "Omega_trk_spc" )"1" assert )nil nil ))nil )"2" expand "Omega_trk_spc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x" )"2" "2" "Omega_trk_spc_critical" )"2" "s" "B" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" "2" "x" )"2" expand "trk_critical?" )"2" "trk_line_complete" )"2" "2" "2" assert )"2" "Omega_trk_spc_separated" )"2" "s" "B" "x" "vi" "vo" )"2" assert )"2" assert )"2" expand "Vtrk" )"2" "eps" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "omega_v2_conflict" :dir rl)"2" (rewrite "omega_v2_conflict" :dir rl)"2" (lemma "IntermediateValue" )"2" (inst -1 "band" "Omega_trk(s,vo,vi)" )"2" (assert )"2" (split -1)"1" "trko" "trk1" )"1" expand "Omega_trk" )"1" expand "o" )"1" (mult-cases -1) nil nil ))nil ))nil ))nil )"2" "x" )"2" "Omega_trk_critical" )"2" "s" "x" "vi" "vo" )"2" assert )"2" "1" expand "trk_band?" )"1" (inst -3 "x" ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (inst? -1) nil nil )) nil ))nil ))nil ))nil ))nil )nil cd2d nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vect2" bands_util nil )set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil connected_set "reals/" )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" atan "trig_fnd/" )nil connected_set "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trk_bands_2D nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil )"continuous_rv_fun" nil )nil trk_bands_2D nil )"nzreal" nil )"({f | continuous?(f)})" trk_bands_2D nil )"bool" continuous_functions "analysis/" )"real" omega_v2 nil )"[T -> real]" vect2_cont_comp "vect_analysis/" )nil trk_bands_2D nil )"(strict_total_order?[real])" real_props nil )nil omega_v2 nil )nil trk_bands_2D nil )"real" reals nil )"(total_order?[real])" nil )nil interm_value_thm "analysis/" )"({f | continuous?(f)})" nil )nil trk_bands_2D nil )"bool" trk_bands_2D nil )nil trk_bands_2D nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )nil trk_line nil )"bool" trk_bands_2D nil )nil trk_only nil )"posreal" nil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"Nz_vect2" bands_util nil )"continuous_rv_fun" nil )"posreal" sq "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" definitions nil )"(trk_only?(vo2))" bands_util nil )"real" trk_bands_2D nil )"odd_int" integers nil )"bool" trk_only nil )"bool" trk_bands_2D nil ))nil )nil 3443196394"" (skeep)"" (lemma "trk_green_two_parallel" )"" (inst?)"" (assert )"" (expand "trk_green?" )"" (skolem 2 "cc" )"" (flatten)"" (case "cc < c" )"1" (lemma "interm_value2" )"1" (inst -1 "cc" "c" "0" )"1" (assert )"1" "LAMBDA (x:closed_interval(cc,c)): omega(ss,vo,vi)(x)" )"1" (assert )"1" (split -1)"1" "1" "Omega_trk_critical" )"1" "c_1" "ss" "vi" "vo" )"1" "1" expand "trk_band?" )"1" "c_1" )"1" (assert ) nil nil ))nil ))nil )"2" expand "omega" -3)"2" (propax) nil nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "omega_continuous" )"2" "2" "cont_intv" )"2" "cc" "c" "omega(ss,vo,vi)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "c < cc" )"1" (lemma "interm_value4" )"1" (inst -1 "c" "cc" "0" )"1" (assert )"1" "LAMBDA (x:closed_interval(c,cc)): omega(ss,vo,vi)(x)" )"1" (assert )"1" "1" "1" "Omega_trk_critical" )"1" "c_1" "ss" "vi" "vo" )"1" "1" expand "trk_band?" )"1" "c_1" )"1" (assert ) nil nil ))nil ))nil )"2" expand "omega" -3)"2" (propax) nil nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "omega_continuous" )"2" "2" "cont_intv" )"2" "c" "cc" "omega(ss,vo,vi)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interm_value_thm "analysis/" )nil interm_value_thm "analysis/" )nil interm_value_thm "analysis/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil horizontal nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil 3476539631"" (skeep)"" (rewrite "cd2d" :dir rl)"" (expand "trk_red?" )"" (split)"1" (flatten)"1" (skolem 1 "trk1" )"1" (case "trk_special_case?(s,vo,vi,T)" )"1" (lemma "trk_special_case_conflict_T" )"1" (inst-cp -1 "s" "trko" "vi" "vo" )"1" (inst -1 "s" "trk1" "vi" "vo" )"1" (assert )"1" (assert )"1" (hide (-3 2))"1" (lemma "IntermediateValue" )"1" "band" "Omega_trk_spc(vo,vi,T)" )"1" assert )"1" "1" "trko" "trk1" )"1" expand "Vtrk" )"1" "trk_spc_horizontal_dir" )"1" "Entry" "trk2v2(vo)(trk1)" "s" "T" "vi" "vo" )"1" "Entry" "trk2v2(vo)(trko)" "s" "T" "vi" "vo" )"1" assert )"1" "1" "1" expand "Omega_trk_spc" )"1" assert )nil nil ))nil )"2" expand "Omega_trk_spc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x" )"2" "2" "Omega_trk_spc_critical" )"2" "s" "T" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" "2" "x" )"2" expand "trk_critical?" )"2" "2" "trk_line_complete" )"2" "2" assert )"2" "Omega_trk_spc_separated" )"2" "s" "T" "x" "vi" "vo" )"2" assert )"2" assert )"2" expand "Vtrk" )"2" "eps" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "B>0 AND trk_special_case?(s,vo,vi,B)" )"1" (flatten)"1" (lemma "trk_special_case_conflict_B" )"1" (inst-cp -1 "s" "trko" "vi" "vo" )"1" (inst -1 "s" "trk1" "vi" "vo" )"1" (assert )"1" (lemma "IntermediateValue" )"1" "band" "Omega_trk_spc(vo,vi,B)" )"1" assert )"1" "1" "trko" "trk1" )"1" expand "Vtrk" )"1" "trk_spc_horizontal_dir" )"1" "Exit" "trk2v2(vo)(trk1)" "s" "B" "vi" "vo" )"1" "Exit" "trk2v2(vo)(trko)" "s" "B" "vi" "vo" )"1" assert )"1" "1" expand "Omega_trk_spc" )"1" assert )nil nil ))nil )"2" expand "Omega_trk_spc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x" )"2" "2" "Omega_trk_spc_critical" )"2" "s" "B" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" "2" "x" )"2" expand "trk_critical?" )"2" "2" "trk_line_complete" )"2" "2" assert )"2" "Omega_trk_spc_separated" )"2" "s" "B" "x" "vi" "vo" )"2" assert )"2" assert )"2" expand "Vtrk" )"2" "eps" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "omega_v2_conflict" :dir rl)"2" (rewrite "omega_v2_conflict" :dir rl)"2" (lemma "IntermediateValue" )"2" (inst -1 "band" "Omega_trk(s,vo,vi)" )"2" (assert )"2" (split -1)"1" "trko" "trk1" )"1" expand "Omega_trk" )"1" expand "o" )"1" (mult-cases -1) nil nil ))nil ))nil ))nil )"2" "x" )"2" "Omega_trk_critical" )"2" "s" "x" "vi" "vo" )"2" assert )"2" "1" expand "trk_band?" )"1" (inst -3 "x" ) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil cd2d nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vect2" bands_util nil )set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil connected_set "reals/" )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" atan "trig_fnd/" )nil connected_set "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trk_bands_2D nil )nil real_types nil )"nnreal" trk_bands_2D nil )"{AB: posreal | AB > B}" trk_bands_2D nil )"continuous_rv_fun" nil )nil trk_bands_2D nil )"nzreal" nil )"({f | continuous?(f)})" trk_bands_2D nil )"bool" continuous_functions "analysis/" )"real" omega_v2 nil )"[T -> real]" vect2_cont_comp "vect_analysis/" )nil trk_bands_2D nil )"(strict_total_order?[real])" real_props nil )nil omega_v2 nil )nil trk_bands_2D nil )"real" reals nil )"(total_order?[real])" nil )nil interm_value_thm "analysis/" )"({f | continuous?(f)})" nil )nil trk_bands_2D nil )"bool" trk_bands_2D nil )nil trk_line nil )"continuous_vr_fun" vect_cont_2D"vect_analysis/" )nil trk_bands_2D nil )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"bool" trk_bands_2D nil )nil trk_only nil )"posreal" nil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"Nz_vect2" bands_util nil )"continuous_rv_fun" nil )"posreal" sq "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" definitions nil )"(trk_only?(vo2))" bands_util nil )"real" trk_bands_2D nil )"odd_int" integers nil )"bool" trk_only nil )"bool" trk_bands_2D nil ))nil )nil 3467650840"" (skeep)"" (rewrite "cd2d" :dir rl)"" (expand "trk_red?" )"" (split)"1" (flatten)"1" (skolem 1 "trk1" )"1" (case "trk_special_case?(sp,vo,vi,T)" )"1" (lemma "trk_special_case_conflict" )"1" (inst-cp -1 "sp" "trko" "vi" "vo" )"1" (inst -1 "sp" "trk1" "vi" "vo" )"1" (assert )"1" (hide (-3 2))"1" (lemma "IntermediateValue" )"1" "band" "Omega_trk_spc(vo,vi,T)" )"1" assert )"1" "1" "trko" "trk1" )"1" expand "Vtrk" )"1" "trk_spc_horizontal_dir" )"1" "Entry" "trk2v2(vo)(trk1)" "sp" "T" "vi" "vo" )"1" "Entry" "trk2v2(vo)(trko)" "sp" "T" "vi" "vo" )"1" assert )"1" "1" "1" expand "Omega_trk_spc" )"1" assert )nil nil ))nil )"2" expand "Omega_trk_spc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x" )"2" "2" "Omega_trk_spc_critical" )"2" "sp" "T" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" "2" "x" )"2" expand "trk_critical?" )"2" "2" "trk_line_complete" )"2" expand "Vtrk" )"2" "2" assert )"2" "eps" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "omega_vv_conflict" :dir rl)"2" (rewrite "omega_vv_conflict" :dir rl)"2" (lemma "IntermediateValue" )"2" (inst -1 "band" "Omega_trk(sp,vo,vi)" )"2" (assert )"2" (split -1)"1" (inst -1 "trko" "trk1" )"1" expand "Omega_trk" )"1" expand "o" )"1" (mult-cases -1) nil nil ))nil ))nil ))nil )"2" (skolem 1 "x" )"2" "Omega_trk_critical" )"2" "sp" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" (inst -3 "x" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil cd2d nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil connected_set "reals/" )"posreal" atan "trig_fnd/" )nil connected_set "reals/" )"[T -> real]" vect2_cont_comp "vect_analysis/" )"bool" definitions nil )nil sign "reals/" )"posreal" sq "reals/" )nil trk_only nil )nil trk_line nil )nil interm_value_thm "analysis/" )"bool" trk_only nil ))nil )nil 3443269825"" (skeep)"" (rewrite "cd2d" :dir rl)"" (expand "trk_red?" )"" (split)"1" (flatten)"1" (skolem 1 "trk1" )"1" (case "trk_special_case?(sp,vo,vi,T)" )"1" (lemma "trk_special_case_conflict" )"1" (inst-cp -1 "sp" "trko" "vi" "vo" )"1" (inst -1 "sp" "trk1" "vi" "vo" )"1" (assert )"1" (hide (-3 2))"1" (lemma "IntermediateValue" )"1" "band" "Omega_trk_spc(vo,vi)" )"1" assert )"1" "1" "trko" "trk1" )"1" expand "Vtrk" )"1" "trk_spc_horizontal_dir" )"1" "Entry" "trk2v2(vo)(trk1)" "sp" "T" "vi" "vo" )"1" "Entry" "trk2v2(vo)(trko)" "sp" "T" "vi" "vo" )"1" assert )"1" "1" "1" expand "Omega_trk_spc" )"1" assert )nil nil ))nil )"2" expand "Omega_trk_spc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x" )"2" "2" "Omega_trk_spc_critical" )"2" "sp" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" "x" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "omega_vv_conflict" :dir rl)"2" (rewrite "omega_vv_conflict" :dir rl)"2" (lemma "IntermediateValue" )"2" (inst -1 "band" "Omega_trk(sp,vo,vi)" )"2" (assert )"2" (split -1)"1" (inst -1 "trko" "trk1" )"1" expand "Omega_trk" )"1" expand "o" )"1" (mult-cases -1) nil nil ))nil ))nil ))nil )"2" (skolem 1 "x" )"2" "Omega_trk_critical" )"2" "sp" "x" "vi" "vo" )"2" assert )"2" expand "trk_band?" )"2" (inst -3 "x" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil cd2d nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil connected_set "reals/" )"posreal" atan "trig_fnd/" )nil connected_set "reals/" )nil sign "reals/" )"posreal" sq "reals/" )nil trk_only nil )nil interm_value_thm "analysis/" )"bool" trk_only nil ))nil )nil 3443210630"" (skeep)"" (case "NOT two_parallel?(ss,vo,vi)" )"1" (expand "trk_red?" )"1" (skolem 2 "cc" )"1" (flatten)"1" (case "cc < c" )"1" (lemma "interm_value4" )"1" (inst -1 "cc" "c" "0" )"1" (assert )"1" "LAMBDA (x:closed_interval(cc,c)): Omega_trk(ss,vo,vi)(x)" )"1" (assert )"1" (split -1)"1" (skeep -1 :preds? t)"1" (lemma "Omega_trk_critical" )"1" "c_1" "ss" "vi" "vo" )"1" "1" expand "trk_band?" )"1" "c_1" )"1" assert )"1" "ab" )"1" "cc" "c" "c_1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Omega_trk" -3)"2" (propax) nil nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "Omega_trk_continuous" )"2" (inst? -1)"2" "cont_intv" )"2" "cc" "c" "Omega_trk(ss,vo,vi)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "c < cc" )"1" (lemma "interm_value2" )"1" (inst -1 "c" "cc" "0" )"1" (assert )"1" "LAMBDA (x:closed_interval(c,cc)): Omega_trk(ss,vo,vi)(x)" )"1" (assert )"1" (split -1)"1" (skeep -1 :preds? t)"1" "Omega_trk_critical" )"1" "c_1" "ss" "vi" "vo" )"1" "1" expand "trk_band?" )"1" "c_1" )"1" assert )"1" "ab" )"1" "c" "cc" "c_1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Omega_trk" -3)"2" (propax) nil nil ))nil )"3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "Omega_trk_continuous" )"2" "2" "cont_intv" )"2" "c" "cc" "Omega_trk(ss,vo,vi)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "trk_green_two_parallel" )"2" (inst?)"2" (inst? -1)"2" (assert )"2" (expand "trk_green?" )"2" (inst -1 "c" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interm_value_thm "analysis/" )nil interm_value_thm "analysis/" )nil interm_value_thm "analysis/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nonneg_real" sq "reals/" )nil horizontal nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" ))nil )))
Messung V0.5 C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.349 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-04-08
