|
(trk_bands_2D
(trk_band 0
(trk_band-1 nil 3460312877
("" (skeep)
(("" (expand "trk_line_eps_irt")
(("" (expand "tangent_line")
(("" (lift-if)
(("" (split -1)
(("1" (flatten)
(("1"
(name-replace "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"
(name-replace "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"
(replaces -2)
(("1"
(rewrite "det_add_left")
(("1"
(rewrite "det_scal_left")
(("1"
(assert)
(("1"
(move-terms 1 l 1)
(("1"
(case-replace
"eps * det(vi, ss) - det(vi, ss) * eps = 0")
(("1"
(hide -1)
(("1"
(rewrite "det_asym")
(("1"
(rewrite "det_s_Qs")
(("1"
(real-props
:simple?
t)
(("1"
(grind-reals)
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)
((trk_line_eps_irt const-decl
"{nvo: Vect2 | nvo /= zero => trk_only?(vo)(nvo)}" trk_line nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(root2b const-decl "real" quadratic_2b "reals/")
(discr2b const-decl "real" quadratic_2b "reals/")
(nzreal nonempty-type-eq-decl nil reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(det_scal_left formula-decl nil det_2D "vectors/")
(det const-decl "real" det_2D "vectors/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(det_s_Qs formula-decl nil tangent_line nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sign_neg_clos application-judgement "Sign" sign "reals/")
(neg_times_ge formula-decl nil real_props nil)
(pos_times_ge formula-decl nil real_props nil)
(neg_mult formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(minus_real_is_real application-judgement "real" reals nil)
(det_asym formula-decl nil det_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(det_add_left formula-decl nil det_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(Qs const-decl "Vect2" tangent_line nil)
(Ss_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(trk_only_line const-decl "{k: real, nvo: Vect2 |
nvo /= zero => trk_only?(vo)(nvo) AND k * vnz = nvo - vi}"
trk_only nil)
(D formal-const-decl "posreal" trk_bands_2D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Qs_nzv application-judgement "Nz_vect2" trk_bands_2D nil)
(tangent_line const-decl "Nz_vect2" tangent_line nil))
nil))
(trk2v2_continuous 0
(trk2v2_continuous-2 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)
((trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(scal_scal_cont_rv formula-decl nil vect2_cont_dot
"vect_analysis/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(bool nonempty-type-eq-decl nil booleans nil)
(continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
(sin const-decl "real" sincos_def "trig_fnd/")
(cos const-decl "real" sincos_def "trig_fnd/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(continuous_fun nonempty-type-eq-decl nil continuous_functions
"analysis/")
(continuous? const-decl "bool" continuous_functions "analysis/")
(pair_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
(cos_cont_fun formula-decl nil sincos "trig_fnd/")
(sin_cont_fun formula-decl nil sincos "trig_fnd/")
(trkgs2vect const-decl "Nz_vect2" track nil))
nil)
(trk2v2_continuous-1 nil 3459317725 ("" (judgement-tcc) nil nil) nil
nil))
(Vtrk_continuous 0
(Vtrk_continuous-1 nil 3443464664
("" (skeep)
(("" (expand "Vtrk")
(("" (rewrite "sub_cont_rv")
(("1" (hide 2) (("1" (rewrite "const_cont_rv") nil nil)) nil)
("2" (hide 2)
(("2"
(case-replace
"(LAMBDA (trk: real): trk2v2(vo)(trk)) = trk2v2(vo)")
(("1" (assert) nil nil)
("2" (decompose-equality 1) nil nil))
nil))
nil))
nil))
nil))
nil)
((Vtrk const-decl "Vect2" bands_util nil)
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(const_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(trk_only? const-decl "bool" definitions nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2
"vect_analysis/")
(continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sub_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil))
shostak))
(Omega_trk_spc 0
(Omega_trk_spc-2 nil 3459203874
("" (skeep)
(("" (expand "Omega_trk_spc")
(("" (rewrite "sub_cont")
(("1" (rewrite "const_cont") nil nil)
("2" (rewrite "dot_cont_rr")
(("1"
(case-replace "(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)
((sq_nz_pos application-judgement "posreal" sq "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(Omega_trk_spc const-decl "real" trk_bands_2D nil)
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
(dot_cont_rr formula-decl nil vect2_cont_dot "vect_analysis/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(const_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
(const_cont formula-decl nil continuous_lambda "analysis/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(D formal-const-decl "posreal" trk_bands_2D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(trk_only? const-decl "bool" definitions nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(* const-decl "real" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(continuous_fun nonempty-type-eq-decl nil continuous_functions
"analysis/")
(continuous? const-decl "bool" continuous_functions "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(sub_cont formula-decl nil continuous_lambda "analysis/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil)
(Omega_trk_spc-1 nil 3459203808 ("" (judgement-tcc) nil nil) nil
nil))
(trk_special_case_invariant 0
(trk_special_case_invariant-1 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)
((trk_special_case? const-decl "bool" trk_only nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(norms_eq_sqv formula-decl nil vectors_2D "vectors/")
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(trk_only? const-decl "bool" definitions nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil))
nil))
(Omega_trk_spc_separated 0
(Omega_trk_spc_separated-2 "" 3504829738
("" (skeep)
(("" (case "sqv(s))
(("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"
(lemma "sq_eq")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(split -1)
(("1"
(rewrite "sq_times")
(("1"
(lemma
"vectors_2D.cauchy_schwarz")
(("1"
(inst?)
(("1"
(case
"sqv(trk2v2(vo)(trk)) = sqv(vo)")
(("1"
(replace -1)
(("1"
(mult-by
-2
"sq(t)")
(("1"
(replace -3)
(("1"
(mult-by
-5
"sq(D)")
(("1"
(expand "sq")
(("1"
(assert)
(("1"
(mult-by
-7
"t * t")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "trk2v2")
(("2"
(lemma "norm_id")
(("2"
(inst
-
"norm(vo)"
"trk")
(("2"
(lemma "sq_eq")
(("2"
(inst?)
(("2"
(flatten)
(("2"
(hide -1)
(("2"
(split
-1)
(("1"
(rewrite
"sq_norm")
(("1"
(rewrite
"sq_norm")
nil
nil))
nil)
("2"
(propax)
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)
((D formal-const-decl "posreal" trk_bands_2D nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(sq const-decl "nonneg_real" sq "reals/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(Omega_trk_spc const-decl "real" trk_bands_2D nil)
(sq_div formula-decl nil sq "reals/")
(div_cancel4 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(div_cancel1 formula-decl nil real_props nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq_times formula-decl nil sq "reals/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(norm const-decl "nnreal" vectors_2D "vectors/")
(trkgs2vect const-decl "Nz_vect2" track nil)
(sq_norm formula-decl nil vectors_2D "vectors/")
(norm_id formula-decl nil track nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(cauchy_schwarz formula-decl nil vectors_2D "vectors/")
(sq_eq formula-decl nil sq "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(real_times_real_is_real application-judgement "real" reals nil)
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(trk_only? const-decl "bool" definitions nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(trk_special_case? const-decl "bool" trk_only nil)
(Omega_trk_spc application-judgement "({f | continuous?(f)})"
trk_bands_2D nil))
shostak)
(Omega_trk_spc_separated-1 nil 3476810585
("" (skeep)
(("" (case "sqv(s))
(("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"
(lemma "sq_eq")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(hide -1)
(("1"
(split -1)
(("1"
(rewrite "sq_times")
(("1"
(lemma
"vectors_2D.cauchy_schwarz")
(("1"
(inst?)
(("1"
(case
"sqv(trk2v2(vo)(trk)) = sqv(vo)")
(("1"
(replace -1)
(("1"
(mult-by
-2
"sq(t)")
(("1"
(replace -3)
(("1"
(mult-by
-5
"sq(D)")
(("1"
(expand "sq")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "trk2v2")
(("2"
(lemma "norm_id")
(("2"
(inst
-
"norm(vo)"
"trk")
(("2"
(lemma "sq_eq")
(("2"
(inst?)
(("2"
(flatten)
(("2"
(hide -1)
(("2"
(split
-1)
(("1"
(rewrite
"sq_norm")
(("1"
(rewrite
"sq_norm")
nil
nil))
nil)
("2"
(propax)
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)
((trk_special_case? const-decl "bool" trk_only nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(trk_only? const-decl "bool" definitions nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(* const-decl "real" vectors_2D "vectors/")
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(dot_scal_left formula-decl nil vectors_2D "vectors/")
(sq_eq formula-decl nil sq "reals/")
(cauchy_schwarz formula-decl nil vectors_2D "vectors/")
(norm_id formula-decl nil track nil)
(sq_norm formula-decl nil vectors_2D "vectors/")
(trkgs2vect const-decl "Nz_vect2" track nil)
(norm const-decl "nnreal" vectors_2D "vectors/")
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(sq_times formula-decl nil sq "reals/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(sq_div formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(sq const-decl "nonneg_real" sq "reals/"))
nil))
(Omega_trk_spc_critical_TCC1 0
(Omega_trk_spc_critical_TCC1-1 nil 3476809011
("" (skeep)
(("" (lemma "Omega_trk_spc_separated")
(("" (inst - "s" "t" "trk" "vi" "vo") (("" (assert) nil nil))
nil))
nil))
nil)
((Omega_trk_spc_separated formula-decl nil trk_bands_2D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Omega_trk_spc application-judgement "({f | continuous?(f)})"
trk_bands_2D nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil))
(Omega_trk_spc_critical 0
(Omega_trk_spc_critical-2 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"
(inst - "trk2v2(vo)(trk)" "s" "t" "vi" "vo")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Omega_trk_spc_separated formula-decl nil trk_bands_2D nil)
(Omega_trk_spc application-judgement "({f | continuous?(f)})"
trk_bands_2D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(sq const-decl "nonneg_real" sq "reals/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(trk_only? const-decl "bool" definitions nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(trk_special_case_invariant formula-decl nil trk_bands_2D nil)
(Omega_trk_spc const-decl "real" trk_bands_2D nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(trk_spc_dot formula-decl nil trk_only nil)
(Vtrk const-decl "Vect2" bands_util nil)
(D formal-const-decl "posreal" trk_bands_2D nil)
(trk_spc_line_solution formula-decl nil trk_only nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil))
nil)
(Omega_trk_spc_critical-1 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)
((trk_only? const-decl "bool" definitions nil)
(Sign type-eq-decl nil sign "reals/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(Sp_vect2 type-eq-decl nil horizontal nil)
(sq const-decl "nonneg_real" sq "reals/")
(sqv const-decl "nnreal" vectors_2D "vectors/")
(Vector type-eq-decl nil vectors_2D "vectors/")
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(sq_nz_pos application-judgement "posreal" sq "reals/"))
shostak))
(trk_special_case_conflict_T 0
(trk_special_case_conflict_T-1 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"
(inst 2 "max(t1,B)")
(("1"
(expand "max" +)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(lemma
"strictly_convex_btw_pt_lt")
(("1"
(lemma
"horiz_dist_strictly_convex_scaf")
(("1"
(inst - "s" "v")
(("1"
(assert)
(("1"
(inst
-
"t1"
"T"
"0"
"LAMBDA (trt: real): horiz_dist_scaf(s)(trt, v)"
"B")
(("1"
(assert)
(("1"
(expand
"horiz_dist_scaf")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "max" +)
(("2"
(lift-if)
(("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)
((real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(Vtrk const-decl "Vect2" bands_util nil)
(trk_spc_on_D formula-decl nil trk_only nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(trk_only? const-decl "bool" definitions nil)
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(trk_special_case? const-decl "bool" trk_only nil)
(conflict_2D? const-decl "bool" cd2d nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(Lookahead type-eq-decl nil Lookahead nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(Vtrk_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(horizontal_entry_le formula-decl nil horizontal nil)
(dot_zero_right formula-decl nil vectors_2D "vectors/")
(add_zero_right formula-decl nil vectors_2D "vectors/")
(scal_zero formula-decl nil vectors_2D "vectors/")
(v skolem-const-decl "Vect2" trk_bands_2D nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(horiz_dist_strictly_convex_scaf formula-decl nil
horizontal_dist_convexity nil)
(horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil)
(strictly_convex_btw_pt_lt formula-decl nil convex_functions
"reals/")
(t1 skolem-const-decl
"{p: real | p >= 0 AND p >= horizontal_tca(s, v)}" trk_bands_2D
nil)
(s skolem-const-decl "Vect2" trk_bands_2D nil)
(nonneg_real_max application-judgement
"{z: nonneg_real | z >= x AND z >= y}" real_defs nil)
(< const-decl "bool" reals nil)
(* const-decl "real" vectors_2D "vectors/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(horizontal_tca const-decl "real" definitions nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(not_horizontal_entry_lt formula-decl nil horizontal nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" trk_bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" trk_bands_2D nil)
(sq const-decl "nonneg_real" sq "reals/")
(D formal-const-decl "posreal" trk_bands_2D nil))
nil))
(trk_special_case_conflict_B 0
(trk_special_case_conflict_B-1 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)
((real nonempty-type-from-decl nil reals nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(zero const-decl "Vector" vectors_2D "vectors/")
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(Vtrk const-decl "Vect2" bands_util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(trk_only? const-decl "bool" definitions nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(trk_spc_on_D formula-decl nil trk_only nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(on_D_conflict formula-decl nil cd2d nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(D formal-const-decl "posreal" trk_bands_2D nil)
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" trk_bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" trk_bands_2D nil))
nil))
(Omega_trk_spc_conflict_T 0
(Omega_trk_spc_conflict_T-1 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"
(hide -4)
(("1"
(name "w" "trk2v2(vo)(trk)")
(("1"
(replace -1)
(("1"
(case "sqv(vo) = sqv(w)")
(("1"
(hide -2)
(("1"
(replace -4)
(("1"
(hide -4)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(mult-by -1 "T")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "trk2v2(vo)(trk)")
(("2"
(expand "trk_only?")
(("2"
(lemma
"vectors_2D.sq_norm")
(("2"
(inst-cp
-1
"trk2v2(vo)(trk)")
(("2"
(inst -1 "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"
(hide -)
(("1"
(mult-by 1 "T")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "trk2v2(vo)(trk)")
(("2"
(expand "trk_only?")
(("2"
(lemma "vectors_2D.sq_norm")
(("2"
(inst-cp
-1
"trk2v2(vo)(trk)")
(("2"
(inst -1 "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)
((trk_special_case_conflict_T formula-decl nil trk_bands_2D nil)
(Vtrk_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(Omega_trk_spc application-judgement "({f | continuous?(f)})"
trk_bands_2D nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(< const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(Vtrk const-decl "Vect2" bands_util nil)
(trk2v2_Nzv application-judgement "Nz_vect2" bands_util nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(trk_only? const-decl "bool" definitions nil)
(trk2v2 const-decl "(trk_only?(vo2))" bands_util nil)
(nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sqv const-decl "nnreal" vectors_2D "vectors/")
(real_minus_real_is_real application-judgement "real" reals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" trk_bands_2D nil)
(T formal-const-decl "{AB: posreal | AB > B}" trk_bands_2D nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "real" vectors_2D "vectors/")
(real_plus_real_is_real application-judgement "real" reals nil)
(sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
"vect_analysis/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
(+ const-decl "Vector" vectors_2D "vectors/")
(- const-decl "Vector" vectors_2D "vectors/")
(* const-decl "Vector" vectors_2D "vectors/")
(trk2v2_continuous application-judgement "continuous_rv_fun"
trk_bands_2D nil)
(nz_norm_gt_0 application-judgement "posreal" vectors_2D
"vectors/")
(sq_norm formula-decl nil vectors_2D "vectors/")
(NOT const-decl "[bool -> bool]" booleans nil)
(trk_special_case? const-decl "bool" trk_only nil)
(Omega_trk_spc const-decl "real" trk_bands_2D nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
(zero const-decl "Vector" vectors_2D "vectors/")
(/= const-decl "boolean" notequal nil)
(Vector type-eq-decl nil vectors_2D "vectors/")
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(Vect2 type-eq-decl nil vectors_2D_def "vectors/")
(real nonempty-type-from-decl nil reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(Omega_trk_spc_conflict_B 0
(Omega_trk_spc_conflict_B-1 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"
(hide -4)
(("1"
(name "w" "trk2v2(vo)(trk)")
(("1"
(replace -1)
(("1"
(case "sqv(vo) = sqv(w)")
(("1"
(hide -2)
(("1"
(replace -4)
(("1"
(hide -4)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(mult-by -1 "B")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "trk2v2(vo)(trk)")
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.54Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
