| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 490 kB |
|
Quellcode-Bibliothek tca_3D.prfSprache: Lisp |
|||||||||||||||
|
(tca_3D (IMP_metric_space_real_fun_TCC1 0 (IMP_metric_space_real_fun_TCC1-1 nil 3563728619 ("" (lemma "real_metric_space") (("" (inst?) nil nil)) nil) ((fullset const-decl "set" sets nil) (set type-eq-decl nil sets 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) (real_metric_space formula-decl nil real_metric_space "analysis/")) nil)) (cyl_norm_sq_diff_cont 0 (cyl_norm_sq_diff_cont-1 nil 3487000249 ("" (skeep) (("" (lemma "diff_continuous[real,real_dist]") (("" (inst - "fullset[real]" "(LAMBDA (t:real): sqv(vect2(s) + t * vect2(v)) / sq(D))" "(LAMBDA (t:real): sq(s`z + t * v`z) / sq(H))") (("" (expand "-" -) (("" (assert) (("" (hide 2) (("" (lemma "vectors_2D.sqv_add") (("" (name "hf1" "(LAMBDA (t:real): sqv(vect2(s))/sq(D))") (("" (name "hf2" "(LAMBDA (t:real): t*(2*vect2(s)*vect2(v)/sq(D)))") (("" (name "hf3" "(LAMBDA (t:real): t*(sqv(vect2(v))/sq(D)))") (("" (name "hf4" "(LAMBDA (t:real): t)") (("" (case "NOT (LAMBDA (t: real): sqv(vect2(s) + t * vect2(v)) / sq(D)) = hf1 + hf2 + hf3*hf4") (("1" (hide 2) (("1" (hide -5) (("1" (decompose-equality +) (("1" (hide -) (("1" (expand "hf1" +) (("1" (expand "hf2" +) (("1" (expand "hf3" +) (("1" (expand "hf4" +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (name "vf1" "(LAMBDA (t:real): sq(s`z)/sq(H))") (("2" (name "vf2" "(LAMBDA (t:real): t*(2*s`z*v`z/sq(H)))") (("2" (name "vf3" "(LAMBDA (t:real): t*(sq(v`z)/sq(H)))") (("2" (name "vf4" "(LAMBDA (t:real): t)") (("2" (case "NOT (LAMBDA (t: real): sq(s`z + t * v`z) / sq(H)) = vf1 + vf2 + vf3*vf4") (("1" (hide 2) (("1" (decompose-equality +) (("1" (hide -) (("1" (expand "vf1" +) (("1" (expand "vf2" +) (("1" (expand "vf3" +) (("1" (expand "vf4" +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (split +) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst - "fullset[real]" "hf1 + hf2" "hf3*hf4") (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (expand "continuous?") (("1" (skosimp*) (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst + "1") (("1" (skosimp*) (("1" (expand "member" +) (("1" (expand "ball" +) (("1" (expand "real_dist") (("1" (expand "hf1" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "hf2") (("2" (name "cc" "2*vect2(s)*vect2(v)/sq(D)") (("2" (replace -1) (("2" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split +) (("1" (expand "hf3") (("1" (name "cc" "sqv(vect2(v))/sq(D)") (("1" (replace -1) (("1" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "hf4") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sum_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (expand "vf1") (("1" (grind :exclude ("fullset" "sq")) nil nil)) nil) ("2" (expand "vf2") (("2" (name "cc" "(2 * (s`z * v`z) / sq(H))") (("2" (replace -1) (("2" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split) (("1" (expand "vf3") (("1" (name "cc" "sq(v`z)/sq(H)") (("1" (replace -1) (("1" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "vf4") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1") (("2" (skosimp*) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_dist const-decl "nnreal" real_metric_space "analysis/") (nnreal type-eq-decl nil real_types nil) (>= 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) (diff_continuous formula-decl nil metric_space_real_fun "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (hf2 skolem-const-decl "[real -> real]" tca_3D nil) (hf4 skolem-const-decl "[real -> real]" tca_3D nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (hf3 skolem-const-decl "[real -> real]" tca_3D nil) (hf1 skolem-const-decl "[real -> nnreal]" tca_3D nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (vf1 skolem-const-decl "[real -> nnreal]" tca_3D nil) (vf3 skolem-const-decl "[real -> real]" tca_3D nil) (vf4 skolem-const-decl "[real -> real]" tca_3D nil) (vf2 skolem-const-decl "[real -> real]" tca_3D nil) (cc skolem-const-decl "real" tca_3D nil) (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (cc skolem-const-decl "nnreal" tca_3D nil) (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (sum_continuous formula-decl nil metric_space_real_fun "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (cc skolem-const-decl "real" tca_3D nil) (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (abs_mult formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (abs_nat formula-decl nil abs_lems "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (member const-decl "bool" sets nil) (abs_0 formula-decl nil abs_lems "reals/") (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ball const-decl "set[T]" metric_spaces "analysis/") (cc skolem-const-decl "nnreal" tca_3D nil) (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (prod_continuous formula-decl nil metric_space_real_fun "analysis/") (* const-decl "real" vectors_2D "vectors/") (sqv_add formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (H formal-const-decl "posreal" tca_3D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (D formal-const-decl "posreal" tca_3D 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) (* const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (cyl_norm_sq_IVT1 0 (cyl_norm_sq_IVT1-1 nil 3487063566 ("" (skeep) (("" (name "ff" "LAMBDA (tr:real): (sqv(vect2(s) + tr*vect2(v))/sq(D) - sq(s`z+tr*v`z)/sq(H))") (("" (lemma "cyl_norm_sq_diff_cont") (("" (inst - "s" "v") (("" (replace -2) (("" (case "ff(t1) >= 0") (("1" (case "ff(t2) <= 0") (("1" (hide -5) (("1" (case "EXISTS (t: real): ((t1 <= t AND t <= t2) OR (t2 <= t AND t <= t1)) AND ff(t) = 0") (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "ff" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide 2) (("2" (hide -4) (("2" (lemma "real_fun_continuity_equiv") (("2" (inst - "ff") (("2" (assert) (("2" (ground) (("1" (case "t1 <= t2") (("1" (assert) (("1" (lemma "intermediate_value4[t1,t2]") (("1" (inst - "ff" "0") (("1" (expand "restrict") (("1" (split -) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "continuous?" (-3 +)) (("2" (skosimp*) (("2" (inst - "x0!1") (("2" (expand "continuous?" (-3 +)) (("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "intermediate_value2[t2,t1]") (("1" (inst - "ff" "0") (("1" (assert) (("1" (split -) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) (("1" (expand "restrict") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "continuous?" (-2 +)) (("2" (skosimp*) (("2" (inst - "x0!1") (("2" (expand "continuous?" (-2 +)) (("2" (expand "restrict") (("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "restrict") (("3" (propax) nil nil)) nil) ("4" (expand "restrict") (("4" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "continuous?" -) (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst - "x0!1") (("1" (expand "continuous?" 1) (("1" (expand "continuous_at?" -) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (assert) (("1" (split -4) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "abs" (-1 1)) (("2" (lift-if) (("2" (ground) 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) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide -3) (("2" (expand "ff") (("2" (hide -) (("2" (expand "cyl_norm_sq" +) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (expand "max") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "ff") (("2" (expand "cyl_norm_sq") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((H formal-const-decl "posreal" tca_3D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (D formal-const-decl "posreal" tca_3D 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) (* const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields 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) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (vz_scal formula-decl nil vectors_3D "vectors/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (vz_distr_add formula-decl nil vectors_3D "vectors/") (vect2_add formula-decl nil vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (intermediate_value2 formula-decl nil continuity_interval "analysis/") (t1 skolem-const-decl "real" tca_3D nil) (t2 skolem-const-decl "real" tca_3D nil) (restrict const-decl "R" restrict nil) (J nonempty-type-eq-decl nil continuity_interval "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (continuous? const-decl "bool" continuous_functions "analysis/") (intermediate_value4 formula-decl nil continuity_interval "analysis/") (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (x0!1 skolem-const-decl "real" tca_3D nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "real" tca_3D nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (member const-decl "bool" sets nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (real_fun_continuity_equiv formula-decl nil real_fun_continuity_equiv "analysis/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals 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) (ff skolem-const-decl "[real -> real]" tca_3D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (cyl_norm_sq_diff_cont formula-decl nil tca_3D nil)) shostak)) (cyl_norm_sq_IVT2 0 (cyl_norm_sq_IVT2-2 nil 3487065298 ("" (skeep) (("" (name "ff" "LAMBDA (tr:real): (sqv(vect2(s) + tr*vect2(v))/sq(D) - sq(s`z+tr*v`z)/sq(H))") (("" (lemma "cyl_norm_sq_diff_cont") (("" (inst - "s" "v") (("" (replace -2) (("" (case "ff(t1) <= 0") (("1" (case "ff(t2) >= 0") (("1" (hide -5) (("1" (case "EXISTS (t: real): ((t1 <= t AND t <= t2) OR (t2 <= t AND t <= t1)) AND ff(t) = 0") (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (expand "ff" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide 2) (("2" (hide -4) (("2" (lemma "real_fun_continuity_equiv") (("2" (inst - "ff") (("2" (assert) (("2" (ground) (("1" (case "t2 <= t1") (("1" (assert) (("1" (lemma "intermediate_value4[t2,t1]") (("1" (inst - "ff" "0") (("1" (expand "restrict") (("1" (split -) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "continuous?" (-3 +)) (("2" (skosimp*) (("2" (inst - "x0!1") (("2" (expand "continuous?" (-3 +)) (("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "intermediate_value2[t1,t2]") (("1" (inst - "ff" "0") (("1" (assert) (("1" (expand "restrict") (("1" (split -) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (expand "continuous?" (-2 +)) (("2" (skosimp*) (("2" (inst - "x0!1") (("2" (expand "continuous?" (-2 +)) (("2" (skosimp*) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst + "delta!1") (("2" (skosimp*) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "continuous?" -) (("2" (expand "continuous?" 1) (("2" (skosimp*) (("2" (inst - "x0!1") (("1" (expand "continuous?" 1) (("1" (expand "continuous_at?" -) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (assert) (("1" (split -4) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "abs" (-1 1)) (("2" (lift-if) (("2" (ground) 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) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (hide -) (("2" (expand "ff") (("2" (expand "cyl_norm_sq" +) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (expand "max") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "ff") (("2" (expand "cyl_norm_sq") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((H formal-const-decl "posreal" tca_3D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (D formal-const-decl "posreal" tca_3D 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) (* const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields 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) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (<= const-decl "bool" reals nil) (* const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (vect2_add formula-decl nil vect_3D_2D "vectors/") (vz_distr_add formula-decl nil vectors_3D "vectors/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (vz_scal formula-decl nil vectors_3D "vectors/") (vect2_scal formula-decl nil vect_3D_2D "vectors/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (intermediate_value2 formula-decl nil continuity_interval "analysis/") (t2 skolem-const-decl "real" tca_3D nil) (t1 skolem-const-decl "real" tca_3D nil) (restrict const-decl "R" restrict nil) (J nonempty-type-eq-decl nil continuity_interval "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (continuous? const-decl "bool" continuous_functions "analysis/") (intermediate_value4 formula-decl nil continuity_interval "analysis/") (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (x0!1 skolem-const-decl "real" tca_3D nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (ball const-decl "set[T]" metric_spaces "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "real" tca_3D nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (member const-decl "bool" sets nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (real_fun_continuity_equiv formula-decl nil real_fun_continuity_equiv "analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (ff skolem-const-decl "[real -> real]" tca_3D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cyl_norm_sq_diff_cont formula-decl nil tca_3D nil)) nil) (cyl_norm_sq_IVT2-1 nil 3487065280 ("" (postpone) nil nil) nil shostak)) (cyl_norm_sq_fun_convex 0 (cyl_norm_sq_fun_convex-1 nil 3487677670 ("" (skeep) (("" (expand "cyl_norm_sq_fun") (("" (expand "cyl_norm_sq") (("" (lemma "max_of_convex") (("" (inst - "LAMBDA (t:real): sqv(vect2(s + t * v)) / sq(D)" "LAMBDA (t:real): sq((s + t * v)`z) / sq(H)") (("" (assert) (("" (hide 2) (("" (lemma "quad_convex") (("" (split) (("1" (name "ac" "sqv(vect2(v))/sq(D)") (("1" (name "bc" "2*vect2(s)*vect2(v)/sq(D)") (("1" (name "cc" "sqv(vect2(s))/sq(D)") (("1" (case "NOT quadratic(ac,bc,cc) = (LAMBDA (t: real): sqv(vect2(s + t * v)) / sq(D))") (("1" (hide 2) (("1" (hide -4) (("1" (decompose-equality) (("1" (expand "ac" +) (("1" (expand "bc" +) (("1" (expand "cc" +) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (inst - "ac" "bc" "cc") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "ad" "sq(v`z)/sq(H)") (("2" (name "bd" "2*s`z*v`z/sq(H)") (("2" (name "cd" "sq(s`z)/sq(H)") (("2" (case "NOT quadratic(ad,bd,cd) = (LAMBDA (t: real): sq((s + t * v)`z) / sq(H))") (("1" (hide-all-but 1) (("1" (decompose-equality) (("1" (expand "ad") (("1" (expand "bd") (("1" (expand "cd") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (inst - "ad" "bd" "cd") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (max_of_convex formula-decl nil convex_functions "reals/") (quad_convex formula-decl nil convex_functions "reals/") (ad skolem-const-decl "nnreal" tca_3D nil) (cd skolem-const-decl "nnreal" tca_3D nil) (bd skolem-const-decl "real" tca_3D nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_times_real_is_real application-judgement "real" reals nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (bc skolem-const-decl "real" tca_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cc skolem-const-decl "nnreal" tca_3D nil) (ac skolem-const-decl "nnreal" tca_3D nil) (quadratic const-decl "real" quadratic "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (H formal-const-decl "posreal" tca_3D nil) (D formal-const-decl "posreal" tca_3D 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) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (cyl_norm_sq const-decl "nnreal" tca_3D nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) shostak)) (cyl_norm_sq_fun_cont 0 (cyl_norm_sq_fun_cont-1 nil 3487069832 ("" (skeep) (("" (expand "cyl_norm_sq_fun") (("" (expand "cyl_norm_sq") (("" (lemma "max_fun_continuous[real,real_dist]") (("" (name "fD" "LAMBDA (t): sqv(vect2(s + t * v)) / sq(D)") (("" (name "fH" "LAMBDA (t): sq((s + t * v)`z) / sq(H)") (("" (inst - "fullset[real]" "fD" "fH") (("" (expand "max_fun") (("" (replace -1 -3 :dir rl) (("" (replace -2 -3 :dir rl) (("" (assert) (("" (hide 2) (("" (name "vf1" "(LAMBDA (t:real): sq(s`z)/sq(H))") (("" (name "vf2" "(LAMBDA (t:real): t*(2*s`z*v`z/sq(H)))") (("" (name "vf3" "(LAMBDA (t:real): t*(sq(v`z)/sq(H)))") (("" (name "vf4" "(LAMBDA (t:real): t)") (("" (case "NOT (LAMBDA (t: real): sq((s + t * v)`z) / sq(H)) = vf1 + vf2 + vf3*vf4") (("1" (hide 2) (("1" (decompose-equality +) (("1" (hide -) (("1" (expand "vf1" +) (("1" (expand "vf2" +) (("1" (expand "vf3" +) (("1" (expand "vf4" +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (hide -1) (("2" (name "hf1" "(LAMBDA (t:real): sqv(vect2(s))/sq(D))") (("2" (name "hf2" "(LAMBDA (t:real): t*(2*vect2(s)*vect2(v)/sq(D)))") (("2" (name "hf3" "(LAMBDA (t:real): t*(sqv(vect2(v))/sq(D)))") (("2" (name "hf4" "(LAMBDA (t:real): t)") (("2" (case "NOT (LAMBDA (t: real): sqv(vect2(s + t * v)) / sq(D)) = hf1 + hf2 + hf3*hf4") (("1" (hide 2) (("1" (decompose-equality +) (("1" (hide -) (("1" (expand "hf1" +) (("1" (expand "hf2" +) (("1" (expand "hf3" +) (("1" (expand "hf4" +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (split +) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split +) (("1" (expand "continuous?") (("1" (skosimp*) (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst + "1") (("1" (skosimp*) (("1" (expand "member" +) (("1" (expand "ball" +) (("1" (expand "real_dist") (("1" (expand "hf1" +) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "hf2") (("2" (name "cc" "2*vect2(s)*vect2(v)/sq(D)") (("2" (replace -1) (("2" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split +) (("1" (expand "hf3") (("1" (name "cc" "sqv(vect2(v))/sq(D)") (("1" (replace -1) (("1" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "hf4") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sum_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split) (("1" (lemma "sum_continuous[real,real_dist]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (expand "vf1") (("1" (grind :exclude ("fullset" "sq")) nil nil)) nil) ("2" (expand "vf2") (("2" (name "cc" "(2 * (s`z * v`z) / sq(H))") (("2" (replace -1) (("2" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prod_continuous[real,real_dist]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (split) (("1" (expand "vf3") (("1" (name "cc" "sq(v`z)/sq(H)") (("1" (replace -1) (("1" (case "cc = 0") (("1" (replace -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1/abs(cc)") (("1" (hide -) (("1" (skosimp*) (("1" (expand "member") (("1" (expand "ball") (("1" (expand "real_dist") (("1" (lemma "abs_mult") (("1" (inst - "cc" "x!1-y!1") (("1" (assert) (("1" (replace -1) (("1" (cross-mult -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "epsilon!1/abs(cc) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "vf4") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (expand "continuous_at?") (("2" (skosimp*) (("2" (inst + "epsilon!1") (("2" (skosimp*) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (nnreal type-eq-decl nil real_types nil) (>= 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) (max_fun_continuous formula-decl nil continuity_of_max_min "analysis/") (H formal-const-decl "posreal" tca_3D nil) (max_fun const-decl "real" continuity_of_max_min "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (hf1 skolem-const-decl "[real -> nnreal]" tca_3D nil) (hf3 skolem-const-decl "[real -> real]" tca_3D nil) (hf4 skolem-const-decl "[real -> real]" tca_3D nil) (hf2 skolem-const-decl "[real -> real]" tca_3D nil) (prod_continuous formula-decl nil metric_space_real_fun "analysis/") (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (cc skolem-const-decl "nnreal" tca_3D nil) (ball const-decl "set[T]" metric_spaces "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (abs_0 formula-decl nil abs_lems "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (member const-decl "bool" sets nil) (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abs_nat formula-decl nil abs_lems "reals/") (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_mult formula-decl nil real_props nil) (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (cc skolem-const-decl "real" tca_3D nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sum_continuous formula-decl nil metric_space_real_fun "analysis/") (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (cc skolem-const-decl "nnreal" tca_3D nil) (epsilon!1 skolem-const-decl "posreal" tca_3D nil) (cc skolem-const-decl "real" tca_3D nil) (* const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (vf2 skolem-const-decl "[real -> real]" tca_3D nil) (vf4 skolem-const-decl "[real -> real]" tca_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (vf3 skolem-const-decl "[real -> real]" tca_3D nil) (vf1 skolem-const-decl "[real -> nnreal]" tca_3D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (Vector type-eq-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" tca_3D nil) (cyl_norm_sq const-decl "nnreal" tca_3D nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) shostak)) (cyl_norm_min_exists 0 (cyl_norm_min_exists-1 nil 3487070618 ("" (skeep) (("" (lemma "closed_intervals_compact") (("" (inst - "B1" "B2") (("1" (lemma "cont_on_compact_min") (("1" (inst - "closed_intv(B1,B2)" "cyl_norm_sq_fun(s,v)") (("1" (assert) (("1" (case "continuous?(cyl_norm_sq_fun(s, v), LAMBDA (x: real): B1 <= x AND x <= B2)") (("1" (assert) (("1" (split -) (("1" (expand "empty?") (("1" (inst - "B1") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "s!1") (("2" (assert) (("2" (skosimp*) (("2" (inst - "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (hide -1) (("2" (hide 2) (("2" (lemma "cyl_norm_sq_fun_cont") (("2" (inst?) (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst - "x!1") (("1" (expand "continuous_at?") (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + "delta!1") (("1" (skosimp*) (("1" (inst - "y!1") (("1" (assert) nil nil) ("2" (expand "fullset") (("2" (propax) nil 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) ("2" (inst + "B1") (("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "B1") (("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((closed_intervals_compact formula-decl nil real_metric_space "analysis/") (cont_on_compact_min formula-decl nil real_fun_on_compact_sets "analysis/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_dist const-decl "nnreal" real_metric_space "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (y!1 skolem-const-decl "(LAMBDA (x: real): B1 <= x AND x <= B2)" tca_3D nil) (x!1 skolem-const-decl "(LAMBDA (x: real): B1 <= x AND x <= B2)" tca_3D nil) (fullset const-decl "set" sets nil) (cyl_norm_sq_fun_cont formula-decl nil tca_3D nil) (r!1 skolem-const-decl "real" tca_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (continuous? const-decl "bool" continuity_ms_def "analysis/") (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (<= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (B1 skolem-const-decl "real" tca_3D nil) (B2 skolem-const-decl "real" tca_3D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (cyl_norm_min_exists_inf 0 (cyl_norm_min_exists_inf-1 nil 3487071184 ("" (case "FORALL (aa,bb,cc,ZZ:real): aa > 0 IMPLIES (EXISTS (BBB: nnreal): FORALL (xx:real): xx>= (("1" (label "quadlem" -1) (("1" (hide "quadlem") (("1" (skeep) (("1" (case "EXISTS (Bz:nnreal): FORALL (nnt:nnreal): nnt >= Bz IMPLIES cyl_norm_sq_fun(s,v)(nnt (("1" (skeep -1) (("1" (lemma "cyl_norm_min_exists") (("1" (inst - "0" "Bz" "s" "v") (("1" (assert) (("1" (skosimp*) (("1" (inst + "t!1") (("1" (skosimp*) (("1" (case "nnt!1 <= Bz") (("1" (inst - "nnt!1") (("1" (assert) nil nil)) nil) ("2" (inst -4 "nnt!1") (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "vect2(v) /= zero IMPLIES EXISTS (BD:nnreal): FORALL (nnt:nnreal): nnt >= BD IMPLIES sqv (("1" (case "v`z /= 0 IMPLIES EXISTS (BH:nnreal): FORALL (nnt:nnreal): nnt >= BH IMPLIES sq((s+nnt*v (("1" (case "vect2(v) /= zero OR v`z /= 0") (("1" (split -) (("1" (assert) (("1" (skeep -3) (("1" (inst + "BD") (("1" (skosimp*) (("1" (inst - "nnt!1") (("1" (assert) (("1" (hide -1) (("1" (expand "cyl_norm_sq_fun" + 1) (("1" (expand "cyl_norm_sq") (("1" (expand "max") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -3) (("2" (skeep -2) (("2" (inst + "BH") (("2" (skosimp*) (("2" (inst - "nnt!1") (("2" (assert) (("2" (expand "cyl_norm_sq_fun" + 1) (("2" (expand "cyl_norm_sq") (("2" (expand "max") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (case "v = zero") (("1" (replace -1) (("1" (hide 1) (("1" (hide -) (("1" (inst + "1") (("1" (skosimp*) (("1" (expand "cyl_norm_sq_fun") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (flatten) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (flatten) (("2" (case "sq(v`z) /= 0") (("1" (flatten) (("1" (reveal "quadlem") (("1" (inst - "sq(v`z)" "2*s`z*v`z" "sq(s`z)" "cyl_norm_sq_fun(s,v)(0)*sq(H)") (("1" (assert) (("1" (skeep -1) (("1" (inst + "BBB") (("1" (skosimp*) (("1" (inst - "nnt!1") (("1" (assert) (("1" (cross-mult 3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (flatten) (("2" (reveal "quadlem") (("2" (inst - "sqv(vect2(v))" "2*vect2(s)*vect2(v)" "sqv(vect2(s))" "cyl_norm_sq_fun(s,v)(0)*sq(D)") (("2" (case "sqv(vect2(v)) > 0") (("1" (assert) (("1" (skeep -2) (("1" (inst + "BBB") (("1" (skosimp*) (("1" (inst - "nnt!1") (("1" (assert) (("1" (hide -1) (("1" (cross-mult 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "vectors_2D.sqv_eq_0") (("2" (inst - "vect2(v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (name "BB" "max(max((1-bb)/aa,0),ZZ-cc)") (("1" (name "yy" "max((1-bb)/aa,0)") (("1" (replace -1) (("1" (typepred "max(yy,ZZ-cc)") (("1" (name "rr" "max(yy,ZZ-cc)") (("1" (replace -1) (("1" (inst + "BB") (("1" (replace -5 + :dir rl) (("1" (skeep) (("1" (expand "quadratic") (("1" (case "xx*(aa*xx+bb) >= ZZ-cc") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (case "aa*xx+bb >= 1") (("1" (mult-by -1 "xx") (("1" (assert) nil nil)) nil) ("2" (typepred "yy") (("2" (case "aa*xx >= aa*yy") (("1" (cross-mult -2) (("1" (assert) nil nil)) nil) ("2" (mult-by -9 "aa") (("2" (mult-by -5 "aa") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (bb skolem-const-decl "real" tca_3D nil) (aa skolem-const-decl "real" tca_3D nil) (ZZ skolem-const-decl "real" tca_3D nil) (cc skolem-const-decl "real" tca_3D nil) (BB skolem-const-decl "{p: real | p >= max((1 - bb) / aa, 0) AND p >= ZZ - cc}" tca_3D nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (xx skolem-const-decl "real" tca_3D nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_ge2 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (H formal-const-decl "posreal" tca_3D nil) (scal_zero formula-decl nil vectors_3D "vectors/") (add_zero_right formula-decl nil vectors_3D "vectors/") (zero const-decl "Vector" vectors_3D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sq_eq_0 formula-decl nil sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "real" vectors_2D "vectors/") (div_mult_pos_ge1 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" tca_3D nil) (<= const-decl "bool" reals nil) (t!1 skolem-const-decl "real" tca_3D 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) (cyl_norm_min_exists formula-decl nil tca_3D nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (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) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (quadratic const-decl "real" quadratic "reals/")) shostak)) (conflict_at_cyl_norm_sq 0 (conflict_at_cyl_norm_sq-1 nil 3486897240 ("" (skeep) (("" (expand "cyl_norm_sq") (("" (expand "max") (("" (lift-if) (("" (ground) (("1" (cross-mult 1) (("1" (lemma "sq_lt") (("1" (inst?) (("1" (assert) (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult -1) (("2" (lemma "sq_lt") (("2" (inst?) (("2" (assert) (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "vect2_add") (("3" (rewrite "vect2_scal") (("3" (mult-by -2 "sq(D)") (("3" (assert) (("3" (mult-by -1 "sq(D)") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "vect2_add") (("4" (cross-mult 1) (("4" (rewrite "vect2_scal") (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (case "sq((s+t*v)`z) < sq(H)") (("1" (lemma "sq_lt") (("1" (inst - "abs(s`z + t*v`z)" "H") (("1" (assert) (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "sq((s+t*v)`z)/sq(H) < 1") (("1" (cross-mult -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("6" (cross-mult -1) (("6" (rewrite "vect2_add") (("6" (rewrite "vect2_scal") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (< const-decl "bool" reals nil) (vect2_add formula-decl nil vect_3D_2D "vectors/") (both_sides_times_pos_lt1 formula-decl nil real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (D formal-const-decl "posreal" tca_3D nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (div_mult_pos_lt1 formula-decl nil real_props nil) (* const-decl "Vector" vectors_3D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (H formal-const-decl "posreal" tca_3D nil) (sq const-decl "nonneg_real" sq "reals/") (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 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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (vz_distr_add formula-decl nil vectors_3D "vectors/") (vz_scal formula-decl nil vectors_3D "vectors/") (sq_abs formula-decl nil sq "reals/") (sq_lt formula-decl nil sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (minimum_info_TCC1 0 (minimum_info_TCC1-1 nil 3486904731 ("" (subtype-tcc) nil nil) nil nil)) (minimum_info_TCC2 0 (minimum_info_TCC2-1 nil 3486904731 ("" (subtype-tcc) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (horizontal_min_info_TCC1 0 (horizontal_min_info_TCC1-1 nil 3486904731 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (info const-decl "Min_Info" tca_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (horizontal_min_info_TCC2 0 (horizontal_min_info_TCC2-1 nil 3486904731 ("" (subtype-tcc) nil nil) ((vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (horizontal_min_info_TCC3 0 (horizontal_min_info_TCC3-1 nil 3486979459 ("" (skeep) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (horizontal_min_info_TCC4 0 (horizontal_min_info_TCC4-1 nil 3486979459 ("" (skeep) (("" (assert) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (horiz_vert_min_info_TCC1 0 (horiz_vert_min_info_TCC1-3 nil 3563291424 ("" (skeep) (("" (split -) (("1" (assert) (("1" (typepred "horizontal_min_info(s,v)") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "horizontal_min_info(s,v)") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_min_info const-decl "{MI: Min_Info | MI`min_dist <= info(s, v, 0)`min_dist AND (vect2(v) /= zero AND horizontal_tca(vect2(s), vect2(v)) >= 0 IMPLIES MI`min_dist <= info(s, v, horizontal_tca(vect2(s), vect2(v)))`min_dist)}" tca_3D nil) (horizontal_tca const-decl "real" definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (info const-decl "Min_Info" tca_3D nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Min_Info type-eq-decl nil tca_3D nil) (nnreal type-eq-decl nil real_types nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (<= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil) (horiz_vert_min_info_TCC1-2 nil 3563291372 ("" (skeep) (("" (assert) (("" (split +) (("1" (name "MII" "minimum_info(horizontal_min_info(s, v), info(s, v, -s`z / v`z))") (("1" (replace -1) (("1" (typepred "MII") (("1" (hide -1) (("1" (typepred "horizontal_min_info(s,v)") (("1" (assert) nil))))))))))) ("2" (flatten) (("2" (name "MII" "minimum_info(horizontal_min_info(s, v), info(s, v, -s`z / v`z))") (("2" (replace -1) (("2" (typepred "MII") (("2" (hide -1) (("2" (typepred "horizontal_min_info(s,v)") (("2" (assert) nil))))))))))))) ("3" (name "MII" "minimum_info(horizontal_min_info(s, v), info(s, v, -s`z / v`z))") (("3" (replace -1) (("3" (typepred "MII") (("3" (propax) nil)))))))))))) nil) nil nil) (horiz_vert_min_info_TCC1-1 nil 3486904731 ("" (skeep) (("" (assert) (("" (split -) (("1" (assert) (("1" (flatten) (("1" (typepred "horizontal_min_info(s,v)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (typepred "horizontal_min_info(s,v)") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case "s`z = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "s`z/v`z = 0") (("1" (cross-mult -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_tca const-decl "real" definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/")) nil)) (horiz_vert_min_info_TCC2 0 (horiz_vert_min_info_TCC2-1 nil 3486904731 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (horiz_vert_min_info_TCC3 0 (horiz_vert_min_info_TCC3-1 nil 3486979459 ("" (subtype-tcc) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (horiz_vert_min_info_TCC4 0 (horiz_vert_min_info_TCC4-1 nil 3486979459 ("" (skeep) (("" (assert) (("" (split +) (("1" (name "MII" "minimum_info(horizontal_min_info(s, v), info(s, v, -s`z / v`z))") (("1" (replace -1) (("1" (typepred "MII") (("1" (hide -1) (("1" (typepred "horizontal_min_info(s,v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (name "MII" "minimum_info(horizontal_min_info(s, v), info(s, v, -s`z / v`z))") (("2" (replace -1) (("2" (typepred "MII") (("2" (hide -1) (("2" (typepred "horizontal_min_info(s,v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (name "MII" "minimum_info(horizontal_min_info(s, v), info(s, v, -s`z / v`z))") (("3" (replace -1) (("3" (typepred "MII") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields 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) (horizontal_min_info const-decl "{MI: Min_Info | MI`min_dist <= info(s, v, 0)`min_dist AND (vect2(v) /= zero AND horizontal_tca(vect2(s), vect2(v)) >= 0 IMPLIES MI`min_dist <= info(s, v, horizontal_tca(vect2(s), vect2(v)))`min_dist)}" tca_3D nil) (horizontal_tca const-decl "real" definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (info const-decl "Min_Info" tca_3D nil) (>= const-decl "bool" reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (minimum_info const-decl "{MI: Min_Info | (MI = MI1 OR MI = MI2) AND MI`min_dist <= MI1`min_dist AND MI`min_dist <= MI2`min_dist}" tca_3D nil) (<= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Min_Info type-eq-decl nil tca_3D nil) (nnreal type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_time_TCC1 0 (cyl_intersect_time_TCC1-1 nil 3486904731 ("" (subtype-tcc) nil 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_time_TCC2 0 (cyl_intersect_time_TCC2-1 nil 3486904731 ("" (subtype-tcc) nil 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_time_TCC3 0 (cyl_intersect_time_TCC3-1 nil 3486904731 ("" (subtype-tcc) nil 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_time_lt 0 (cyl_intersect_time_lt-1 nil 3486980115 ("" (skeep) (("" (expand "cyl_intersect_time") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (assert) (("" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (split 2) (("1" (propax) nil nil) ("2" (flatten) (("2" (split 2) (("1" (propax) nil nil) ("2" (flatten) (("2" (rewrite "root2b_root") (("2" (rewrite "root2b_root") (("2" (name "aa" "sqv(vect2(v)) / sq(D) - sq(v`z) / sq(H)") (("2" (replace -1) (("2" (name "bb" "vect2(s) * vect2(v) / sq(D) - s`z * v`z / sq(H)") (("2" (replace -1) (("2" (copy -1) (("2" (mult-by -1 "2") (("2" (assert) (("2" (replace -1) (("2" (name "cc" "sqv(vect2(s)) / sq(D) - sq(s`z) / sq(H)") (("2" (replace -1) (("2" (rewrite "discr2b_discr") (("2" (hide -) (("2" (expand "root") (("2" (case "aa > 0") (("1" (copy -1) (("1" (mult-by -1 "2") (("1" (assert) (("1" (cross-mult 2) (("1" (expand "sign") (("1" (case "sqrt(discr(aa,2*bb,cc)) >= 0") (("1" (mult-by -1 "aa") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sign") (("2" (assert) (("2" (case "2*aa < 0") (("1" (cross-mult 3) (("1" (case "sqrt(discr(aa,2*bb,cc)) >= 0") (("1" (mult-by -1 "-aa") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cyl_intersect_time const-decl "real" tca_3D nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (nonzero_real nonempty-type-eq-decl nil reals nil) (discr const-decl "real" quadratic "reals/") (times_div2 formula-decl nil real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (div_mult_neg_le1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (root const-decl "real" quadratic "reals/") (discr2b_discr formula-decl nil quadratic_2b "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sign const-decl "Sign" sign "reals/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (H formal-const-decl "posreal" tca_3D nil) (D formal-const-decl "posreal" tca_3D 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 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (root2b_root formula-decl nil quadratic_2b "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil)) shostak)) (cyl_intersect_time_id 0 (cyl_intersect_time_id-1 nil 3486904731 ("" (deftactic squim (&optional (fnum 1)) (then (isolate fnum l 1) (assert fnum))) (("" (skeep) (("" (label "exlem" -1) (("" (hide "exlem") (("" (name "a" "sqv(vect2(v))/sq(D) - sq(v`z)/sq(H)") (("" (name "b" "vect2(s)*vect2(v)/sq(D) - s`z*v`z/sq(H)") (("" (name "c" "sqv(vect2(s))/sq(D) - sq(s`z)/sq(H)") (("" (case "NOT quadratic(a,2*b,c)(t) = 0") (("1" (hide 2) (("1" (expand "a" +) (("1" (expand "b" +) (("1" (expand "c" +) (("1" (hide -1) (("1" (hide -1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "cyl_intersect_time") (("2" (replace -2) (("2" (replace -3) (("2" (case "(2 * (vect2(s) * vect2(v) / sq(D)) - 2 * (s`z * v`z / sq(H))) = 2*b") (("1" (replace -1) (("1" (replace -5) (("1" (lemma "quad2b_eq_0") (("1" (inst - "a" "b" "c" "t") (("1" (assert) (("1" (flatten) (("1" (skosimp*) (("1" (inst + "sign(a)*eps!1") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (expand "quadratic") (("1" (replace -6) (("1" (reveal "exlem") (("1" (skosimp*) (("1" (mult-by -7 "t1!1") (("1" (mult-by -8 "sq(t1!1)") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (replace -1) (("2" (expand "quadratic") (("2" (cross-mult 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "sign(a)*sign(a) = 1") (("1" (assert) nil nil) ("2" (typepred "sign(a)") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (inst + "1") (("2" (lift-if) (("2" (ground) (("1" (replace -1) (("1" (expand "quadratic") (("1" (replace -4) (("1" (assert) (("1" (reveal "exlem") (("1" (skosimp*) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_add") (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (rewrite "vect2_scal") (("1" (rewrite "vect2_scal") (("1" (rewrite "sqv_add") (("1" (rewrite "sq_plus") (("1" (rewrite "sqv_scal") (("1" (rewrite "sq_times") (("1" (assert) (("1" (rewrite "div_distributes" :dir rl) (("1" (rewrite "div_distributes" :dir rl) (("1" (rewrite "div_distributes" :dir rl) (("1" (rewrite "div_distributes" :dir rl) (("1" (assert) (("1" (squim -5) (("1" (squim -6) (("1" (squim -7) (("1" (replace -5) (("1" (replace -6) (("1" (assert) (("1" (replace -7) (("1" (field) 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)) nil) ("2" (expand "quadratic") (("2" (cross-mult 2) (("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)) nil)) nil)) nil)) nil) ((* const-decl "real" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (quadratic const-decl "real" quadratic "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (a skolem-const-decl "real" tca_3D nil) (c skolem-const-decl "real" tca_3D nil) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (b skolem-const-decl "real" tca_3D nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (sign_mult_clos application-judgement "Sign" sign "reals/") (sign const-decl "Sign" sign "reals/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel4 formula-decl nil real_props nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (discr2b const-decl "real" quadratic_2b "reals/") (sqrt_0 formula-decl nil sqrt "reals/") (root2b const-decl "real" quadratic_2b "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (vz_scal formula-decl nil vectors_3D "vectors/") (sq_plus formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_distributes formula-decl nil real_props nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (both_sides_times1 formula-decl nil real_props nil) (cross_mult formula-decl nil real_props nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (sqv_scal formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_add formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (vect2_scal formula-decl nil vect_3D_2D "vectors/") (vz_distr_add formula-decl nil vectors_3D "vectors/") (vect2_add formula-decl nil vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (cyl_intersect_time const-decl "real" tca_3D nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real_pred const-decl "[number_field -> boolean]" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" tca_3D nil) (H formal-const-decl "posreal" tca_3D nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (cyl_intersect_min_info_TCC1 0 (cyl_intersect_min_info_TCC1-1 nil 3486908162 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (/= const-decl "boolean" notequal 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_min_info_TCC2 0 (cyl_intersect_min_info_TCC2-1 nil 3486908162 ("" (skeep) (("" (skeep) (("" (lemma "cyl_intersect_time_lt") (("" (inst - "s" "v") (("" (replace -2 :dir rl) (("" (replace -4 :dir rl) (("" (skeep) (("" (typepred "eps") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" 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) (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) (/= const-decl "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cyl_intersect_time_lt formula-decl nil tca_3D nil)) nil)) (cyl_intersect_min_info_TCC3 0 (cyl_intersect_min_info_TCC3-1 nil 3486908162 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (real nonempty-type-from-decl nil reals 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_min_info_TCC4 0 (cyl_intersect_min_info_TCC4-1 nil 3486979459 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (real nonempty-type-from-decl nil reals nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (info const-decl "Min_Info" tca_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) nil)) (cyl_intersect_min_info_TCC5 0 (cyl_intersect_min_info_TCC5-1 nil 3486979459 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (real nonempty-type-from-decl nil reals 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_min_info_TCC6 0 (cyl_intersect_min_info_TCC6-1 nil 3486979459 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (real nonempty-type-from-decl nil reals 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (cyl_intersect_min_info_TCC7 0 (cyl_intersect_min_info_TCC7-1 nil 3486979459 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (real nonempty-type-from-decl nil reals nil) (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (info const-decl "Min_Info" tca_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) nil)) (tca_3D_id_TCC1 0 (tca_3D_id_TCC1-1 nil 3486976541 ("" (skeep) (("" (lemma "vectors_2D.sqv_eq_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((sqv_eq_0 formula-decl nil vectors_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (tca_3D_id_TCC2 0 (tca_3D_id_TCC2-1 nil 3486976541 ("" (skeep) (("" (lemma "sq_eq_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((sq_eq_0 formula-decl nil sq "reals/") (Vect3 type-eq-decl nil vectors_3D_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)) nil)) (tca_3D_id 0 (tca_3D_id-1 nil 3486976541 ("" (skeep) (("" (lemma "tca_3D") (("" (decompose-equality -1) (("" (inst - "(s,v)") (("" (typepred "minimum_info(horiz_vert_min_info(s, v), cyl_intersect_min_info(s, v))") (("" (hide -1) (("" (name "MIB" "minimum_info(horiz_vert_min_info(s, v), cyl_intersect_min_info(s, v))") (("" (replace -1) (("" (name "hvmi" "horiz_vert_min_info(s, v)") (("" (replace -1) (("" (name "cimi" "cyl_intersect_min_info(s, v)") (("" (replace -1) (("" (case "MIB`min_dist = cyl_norm_sq(s + tca_3D(s, v) * v)") (("1" (replace -1) (("1" (hide -1) (("1" (case "nnt = 0") (("1" (hide -8) (("1" (replace -1) (("1" (assert) (("1" (typepred "hvmi") (("1" (expand "info" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "nntnz" 1) (("2" (assert) (("2" (hide 1) (("2" (split -) (("1" (flatten) (("1" (typepred "hvmi") (("1" (assert) (("1" (expand "horizontal_tca") (("1" (assert) (("1" (replace -4 :dir rl) (("1" (expand "info" -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "hvmi") (("2" (assert) (("2" (case "nnt = -s`z/v`z") (("1" (replace -1) (("1" (assert) (("1" (expand "info" -4) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "cyl_intersect_time_id") (("3" (inst - "s" "nnt" "v") (("3" (assert) (("3" (split -) (("1" (skosimp*) (("1" (typepred "cimi") (("1" (inst - "eps!1") (("1" (assert) (("1" (expand "info" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT FORALL (zz:real): cyl_norm_sq(s+zz*v) = sqv(vect2(s) + zz*vect2(v))/sq(D)") (("1" (hide-all-but (1 2)) (("1" (skosimp*) (("1" (inst + "zz!1") (("1" (expand "cyl_norm_sq") (("1" (expand "max") (("1" (lift-if) (("1" (ground) (("1" (hide +) (("1" (grind) nil nil)) nil) ("2" (hide 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "normeq" -1) (("2" (copy -1) (("2" (hide "normeq") (("2" (hide 1) (("2" (inst-cp - "nnt") (("2" (inst-cp - "tca_3D(s,v)") (("2" (inst - "0") (("2" (assert) (("2" (replace -2) (("2" (replace -3) (("2" (case "vect2(v) = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "sqv(vect2(s) + nnt * vect2(v)) / sq(D) >= hvmi`min_dist") (("1" (assert) nil nil) ("2" (hide 3) (("2" (expand "hvmi" 1) (("2" (typepred "horiz_vert_min_info(s,v)") (("2" (assert) (("2" (case "horizontal_tca(s,v) >= 0") (("1" (assert) (("1" (expand "info" -3) (("1" (reveal "normeq") (("1" (copy "normeq") (("1" (hide "normeq") (("1" (inst - "horizontal_tca(s,v)") (("1" (replace -1) (("1" (assert) (("1" (case "sqv(vect2(s) + horizontal_tca(vect2(s), vect2(v)) * vect2(v)) / sq(D) <= sqv(vect2(s) + nnt (("1" (assert) nil nil) ("2" (lemma "horizontal_tca_min") (("2" (inst - "v" "s" "nnt") (("2" (lemma "horizontal_sq_dtca_eq") (("2" (inst - "v" "s") (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (cross-mult 1) (("2" (mult-by -1 "sq(D)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "dot_pos_divergent") (("2" (inst - "s" "v") (("2" (split -1) (("1" (expand "divergent?") (("1" (inst - "nnt") (("1" (assert) (("1" (expand "dist") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (lemma "sqrt_lt") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sq_lt") (("1" (inst?) (("1" (assert) (("1" (lemma "vectors_2D.norm_le_sqv") (("1" (inst - "s" "vect2(s)+nnt*vect2(v)") (("1" (assert) (("1" (expand "info" -4) (("1" (assert) (("1" (reveal "normeq") (("1" (copy -1) (("1" (hide "normeq") (("1" (inst - "0") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (cross-mult -4) (("1" (cross-mult 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" (assert) (("2" (hide-all-but (1 2 4)) (("2" (expand "horizontal_tca") (("2" (cross-mult 2) (("2" (ground) (("2" (lemma "vectors_2D.sqv_eq_0") (("2" (inst?) (("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)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "MIB" +) (("2" (hide-all-but 1) (("2" (expand "tca_3D") (("2" (expand "minimum_info") (("2" (lift-if) (("2" (ground) (("1" (hide -) (("1" (expand "horiz_vert_min_info") (("1" (lift-if) (("1" (ground) (("1" (expand "horizontal_min_info") (("1" (lift-if) (("1" (expand "info") (("1" (assert) (("1" (expand "minimum_info") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "horizontal_min_info") (("2" (expand "info") (("2" (expand "minimum_info") (("2" (lift-if) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "minimum_info") (("3" (lift-if) (("3" (ground) (("1" (hide -) (("1" (expand "horizontal_min_info") (("1" (lift-if) (("1" (ground) (("1" (expand "info") (("1" (propax) nil nil)) nil) ("2" (expand "info") (("2" (propax) nil nil)) nil) ("3" (expand "minimum_info") (("3" (lift-if) (("3" (ground) (("1" (expand "info") (("1" (propax) nil nil)) nil) ("2" (expand "info") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "info") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (expand "cyl_intersect_min_info") (("2" (lift-if) (("2" (ground) (("1" (expand "horizontal_min_info") (("1" (lift-if) (("1" (ground) (("1" (expand "info") (("1" (propax) nil nil)) nil) ("2" (expand "info") (("2" (propax) nil nil)) nil) ("3" (expand "minimum_info") (("3" (lift-if) (("3" (ground) (("1" (expand "info") (("1" (propax) nil nil)) nil) ("2" (expand "info") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "minimum_info") (("2" (lift-if) (("2" (propax) 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) ((tca_3D const-decl "nnreal" tca_3D nil) (MIB skolem-const-decl "{MI: Min_Info | (MI = horiz_vert_min_info(s, v) OR MI = cyl_intersect_min_info(s, v)) AND MI`min_dist <= horiz_vert_min_info(s, v)`min_dist AND MI`min_dist <= cyl_intersect_min_info(s, v)`min_dist}" tca_3D nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (horizontal_min_info const-decl "{MI: Min_Info | MI`min_dist <= info(s, v, 0)`min_dist AND (vect2(v) /= zero AND horizontal_tca(vect2(s), vect2(v)) >= 0 IMPLIES MI`min_dist <= info(s, v, horizontal_tca(vect2(s), vect2(v)))`min_dist)}" tca_3D nil) (add_zero_right formula-decl nil vectors_3D "vectors/") (scal_0 formula-decl nil vectors_3D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (scal_zero formula-decl nil vectors_2D "vectors/") (horizontal_tca_min formula-decl nil definitions nil) (horizontal_sq_dtca_eq formula-decl nil definitions nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_mult_pos_le2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_le1 formula-decl nil real_props nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (div_mult_pos_neg_ge1 formula-decl nil extra_real_props nil) (divergent? const-decl "bool" closest_approach_2D "vectors/") (add_zero_left formula-decl nil vectors_2D "vectors/") (sq_dist_norm formula-decl nil distance_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (sqrt_lt formula-decl nil sqrt "reals/") (sq_lt formula-decl nil sq "reals/") (div_mult_pos_ge1 formula-decl nil real_props nil) (norm_le_sqv formula-decl nil vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (dist const-decl "nnreal" distance_2D "vectors/") (dot_pos_divergent formula-decl nil definitions nil) (hvmi skolem-const-decl "{MI: Min_Info | MI`min_dist <= info(s, v, 0)`min_dist AND (vect2(v) /= zero AND horizontal_tca(vect2(s), vect2(v)) >= 0 IMPLIES MI`min_dist <= info(s, v, horizontal_tca(vect2(s), vect2(v)))`min_dist) AND (v`z /= 0 AND -s`z / v`z >= 0 IMPLIES MI`min_dist <= info(s, v, -s`z / v`z)`min_dist)}" tca_3D nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "real" vectors_2D "vectors/") (D formal-const-decl "posreal" tca_3D nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (cyl_intersect_time_id formula-decl nil tca_3D nil) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (NOT const-decl "[bool -> bool]" booleans nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cyl_intersect_min_info const-decl "{MI: Min_Info | FORALL (eps: Sign): cyl_intersect_time(s, v, eps) > 0 IMPLIES MI`min_dist <= info(s, v, cyl_intersect_time(s, v, eps))`min_dist}" tca_3D nil) (cyl_intersect_time const-decl "real" tca_3D nil) (> const-decl "bool" reals nil) (Sign type-eq-decl nil sign "reals/") (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) (horiz_vert_min_info const-decl "{MI: Min_Info | MI`min_dist <= info(s, v, 0)`min_dist AND (vect2(v) /= zero AND horizontal_tca(vect2(s), vect2(v)) >= 0 IMPLIES MI`min_dist <= info(s, v, horizontal_tca(vect2(s), vect2(v)))`min_dist) AND (v`z /= 0 AND -s`z / v`z >= 0 IMPLIES MI`min_dist <= info(s, v, -s`z / v`z)`min_dist)}" tca_3D nil) (- const-decl "[numfield -> numfield]" number_fields 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) (horizontal_tca const-decl "real" definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (info const-decl "Min_Info" tca_3D nil) (minimum_info const-decl "{MI: Min_Info | (MI = MI1 OR MI = MI2) AND MI`min_dist <= MI1`min_dist AND MI`min_dist <= MI2`min_dist}" tca_3D nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Min_Info type-eq-decl nil tca_3D nil) (nnreal 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (tca_3D_vect2_zero 0 (tca_3D_vect2_zero-1 nil 3487078639 ("" (skeep) (("" (lemma "cyl_norm_sq_IVT1") (("" (inst - "s" "nnt" "tca_3D(s,v)" "v") (("" (assert) (("" (rewrite "vect2_add" -3) (("" (rewrite "vect2_scal" -3) (("" (expand "cyl_norm_sq_fun" -3) (("" (assert) (("" (split -) (("1" (skosimp*) (("1" (lemma "tca_3D_id") (("1" (inst - "t!1" "s" "v") (("1" (assert) (("1" (rewrite "vect2_add" -1) (("1" (rewrite "vect2_scal" -1) (("1" (rewrite "vz_distr_add" -1) (("1" (rewrite "vz_scal" -1) (("1" (assert) (("1" (replace -3 -1) (("1" (replace -4) (("1" (assert) (("1" (expand "cyl_norm_sq_fun") (("1" (replace -5) (("1" (expand "cyl_norm_sq" -1 1) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (replace -4) (("1" (assert) (("1" (expand "max") (("1" (hide -2) (("1" (lift-if) (("1" (ground) (("1" (replace -3) (("1" (propax) 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" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -2) (("2" (assert) (("2" (expand "cyl_norm_sq_fun") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cyl_norm_sq_IVT1 formula-decl nil tca_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (t!1 skolem-const-decl "real" tca_3D nil) (vz_distr_add formula-decl nil vectors_3D "vectors/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (vz_scal formula-decl nil vectors_3D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (tca_3D_id formula-decl nil tca_3D nil) (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (vect2_add formula-decl nil vect_3D_2D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (tca_3D const-decl "nnreal" tca_3D nil) (nnreal 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (tca_3D_vz_zero 0 (tca_3D_vz_zero-1 nil 3487079704 ("" (skeep) (("" (lemma "cyl_norm_sq_IVT2") (("" (inst - "s" "nnt" "tca_3D(s,v)" "v") (("" (assert) (("" (rewrite "vz_distr_add") (("" (rewrite "vz_scal") (("" (expand "cyl_norm_sq_fun" -3) (("" (assert) (("" (split -) (("1" (skosimp*) (("1" (lemma "tca_3D_id") (("1" (inst - "t!1" "s" "v") (("1" (assert) (("1" (replace -4) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (replace -3 -1) (("1" (replace -4) (("1" (assert) (("1" (expand "cyl_norm_sq_fun") (("1" (replace -5) (("1" (hide -2) (("1" (expand "cyl_norm_sq" -1 1) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (replace -3) (("1" (assert) (("1" (expand "max") (("1" (lift-if) (("1" (ground) (("1" (replace -2) (("1" (propax) 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" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "cyl_norm_sq_fun(s,v)(tca_3D(s,v)) = sq(s`z + tca_3D(s,v)*v`z)/sq(H)") (("1" (replace -3) (("1" (assert) (("1" (expand "cyl_norm_sq_fun") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "cyl_norm_sq_fun" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cyl_norm_sq_IVT2 formula-decl nil tca_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (vz_scal formula-decl nil vectors_3D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (H formal-const-decl "posreal" tca_3D nil) (t!1 skolem-const-decl "real" tca_3D nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (cyl_norm_sq const-decl "nnreal" tca_3D nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (vect2_add formula-decl nil vect_3D_2D "vectors/") (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (tca_3D_id formula-decl nil tca_3D nil) (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (vz_distr_add formula-decl nil vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (* const-decl "Vector" vectors_3D "vectors/") (tca_3D const-decl "nnreal" tca_3D nil) (nnreal 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) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (tca_3D_def 0 (tca_3D_def-1 nil 3486908162 ("" (case "FORALL (aa:nnreal,bb,cc,zz:real): (aa/=0 OR bb/=0) AND (NOT (aa/=0 AND zz = -bb/(2*aa (("1" (label "quadlem" -1) (("1" (hide -1) (("1" (skeep) (("1" (lemma "cyl_norm_min_exists_inf") (("1" (inst - "s" "v") (("1" (skosimp*) (("1" (label "tzlem" -1) (("1" (case "cyl_norm_sq(s+tz!1*v) >= cyl_norm_sq(s+tca_3D(s,v)*v)") (("1" (inst - "nnt") (("1" (expand "cyl_norm_sq_fun") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "tca_3D_id") (("2" (inst - "tz!1" "s" "v") (("2" (assert) (("2" (flatten) (("2" (case "cyl_norm_sq(s+tz!1*v) = sqv(vect2(s+tz!1*v))/sq(D)") (("1" (case "EXISTS (epsilon:posreal): FORALL (t: real): abs(tz!1-t) < epsilon IMPLIES t > 0 AND cyl_norm_s (("1" (reveal "quadlem") (("1" (inst - "sqv(vect2(v))" "2*vect2(s)*vect2(v)" "sqv(vect2(s))" "tz!1") (("1" (assert) (("1" (split -) (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst - "xx!1") (("1" (assert) (("1" (flatten) (("1" (inst "tzlem" "xx!1") (("1" (expand "cyl_norm_sq_fun") (("1" (replace -4) (("1" (replace -5) (("1" (hide-all-but ("quadlem" "tzlem")) (("1" (cross-mult -3) (("1" (mult-by -2 "sq(D)") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "vect2(v) = zero") (("1" (lemma "tca_3D_vect2_zero") (("1" (inst - "tz!1" "s" "v") (("1" (assert) (("1" (split -) (("1" (expand "cyl_norm_sq_fun") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (expand "cyl_norm_sq_fun") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "vectors_2D.sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (flatten) (("3" (replace -4) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "df" "LAMBDA (t:real): (sqv(vect2(s) + t*vect2(v))/sq(D) - sq(s`z+t*v`z)/sq(H))") (("2" (lemma "cyl_norm_sq_diff_cont") (("2" (inst - "s" "v") (("2" (replace -2) (("2" (case "df(tz!1) > 0") (("1" (case "EXISTS (epsilon:posreal): FORALL (t:real): abs(tz!1-t) < epsilon IMPLIES t > 0 AND df(t)>0") (("1" (skosimp*) (("1" (inst + "epsilon!1") (("1" (skosimp*) (("1" (inst - "t!1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "df" -2) (("1" (expand "cyl_norm_sq_fun" 1) (("1" (expand "cyl_norm_sq" 1) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (expand "max") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1 3)) (("2" (expand "continuous?") (("2" (inst - "tz!1") (("1" (expand "continuous_at?") (("1" (inst - "df(tz!1)") (("1" (skosimp*) (("1" (inst + "min(delta!1,tz!1)") (("1" (skosimp*) (("1" (inst - "t!1") (("1" (grind) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "df" 1) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (expand "cyl_norm_sq" -3) (("2" (expand "max" -3) (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (assert) (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("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) ("2" (case "cyl_norm_sq(s+tz!1*v) = sq((s+tz!1*v)`z)/sq(H)") (("1" (case "EXISTS (epsilon:posreal): FORALL (t: real): abs(tz!1-t) < epsilon IMPLIES t > 0 AND cyl_norm_s (("1" (reveal "quadlem") (("1" (assert) (("1" (inst - "sq(v`z)" "2*s`z*v`z" "sq(s`z)" "tz!1") (("1" (assert) (("1" (split -) (("1" (skosimp*) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst - "xx!1") (("1" (assert) (("1" (flatten) (("1" (inst "tzlem" "xx!1") (("1" (expand "cyl_norm_sq_fun") (("1" (replace -4) (("1" (replace -5) (("1" (hide-all-but ("quadlem" "tzlem")) (("1" (cross-mult -3) (("1" (mult-by -2 "sq(H)") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "v`z = 0") (("1" (replace -1) (("1" (assert) (("1" (hide -2) (("1" (hide -2) (("1" (lemma "tca_3D_vz_zero") (("1" (inst - "tz!1" "s" "v") (("1" (assert) (("1" (split -) (("1" (expand "cyl_norm_sq_fun") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (expand "cyl_norm_sq_fun") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "df" "LAMBDA (t:real): (sqv(vect2(s) + t*vect2(v))/sq(D) - sq(s`z+t*v`z)/sq(H))") (("2" (lemma "cyl_norm_sq_diff_cont") (("2" (inst - "s" "v") (("2" (replace -2) (("2" (case "df(tz!1) < 0") (("1" (case "EXISTS (epsilon:posreal): FORALL (t:real): abs(tz!1-t) < epsilon IMPLIES t > 0 AND df(t)<0") (("1" (skosimp*) (("1" (inst + "epsilon!1") (("1" (skosimp*) (("1" (inst - "t!1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "df" -2) (("1" (expand "cyl_norm_sq_fun" 1) (("1" (expand "cyl_norm_sq" 1) (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (expand "max") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1 4)) (("2" (expand "continuous?") (("2" (inst - "tz!1") (("1" (expand "continuous_at?") (("1" (inst - "-df(tz!1)") (("1" (skosimp*) (("1" (inst + "min(delta!1,tz!1)") (("1" (skosimp*) (("1" (inst - "t!1") (("1" (grind) nil nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "df" 1) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (expand "cyl_norm_sq" -3) (("2" (expand "max" -3) (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (assert) (("1" (rewrite "vz_distr_add") (("1" (rewrite "vz_scal") (("1" (rewrite "vect2_add") (("1" (rewrite "vect2_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (assert) (("2" (expand "cyl_norm_sq" (1 2)) (("2" (expand "max" (1 2)) (("2" (rewrite "vz_distr_add") (("2" (rewrite "vz_scal") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (lift-if) (("2" (ground) 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" (hide 2) (("2" (skeep) (("2" (case "aa = 0") (("1" (assert) (("1" (hide 1) (("1" (flatten) (("1" (expand "quadratic") (("1" (replace -1) (("1" (assert) (("1" (skosimp*) (("1" (name "xy" "zz-sign(bb)*epsilon!1/2") (("1" (inst + "xy") (("1" (split +) (("1" (replace -1 :dir rl) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (assert) (("2" (hide -1) (("2" (expand "sign") (("2" (lift-if) (("2" (ground) (("1" (case "epsilon!1 / 2 * bb >= 0") (("1" (assert) nil nil) ("2" (mult-by -1 "epsilon!1/2") (("2" (assert) nil nil)) nil)) nil) ("2" (case "-1 * epsilon!1 / 2 * bb >= 0") (("1" (assert) nil nil) ("2" (mult-by 2 "epsilon!1/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "aa > 0") (("1" (hide -2) (("1" (hide 1) (("1" (assert) (("1" (case "zz > -bb/(2*aa)") (("1" (skosimp*) (("1" (name "ep2" "zz+bb/(2*aa)") (("1" (name "myep" "min(ep2,epsilon!1)") (("1" (name "xy" "zz-myep/2") (("1" (inst + "xy") (("1" (split) (("1" (replace -1 :dir rl) (("1" (assert) (("1" (expand "abs" +) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (replace -3 -1 :dir rl) (("1" (expand "min" -1) (("1" (lift-if) (("1" (ground) (("1" (case "ep2 > 0") (("1" (assert) nil nil) ("2" (assert) (("2" (replace -4 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -2 :dir rl) (("2" (expand "min" 2) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "quad_min_mono_inc") (("2" (inst - "aa" "bb" "cc" "zz" "xy") (("2" (assert) (("2" (split -) (("1" (assert) nil nil) ("2" (case "myep/2>0") (("1" (assert) nil nil) ("2" (case "myep > 0") (("1" (assert) nil nil) ("2" (expand "myep" 1) (("2" (case "ep2 > 0") (("1" (assert) (("1" (expand "min" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand "ep2" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "xy" 1) (("3" (case "zz-myep >= -bb/(2*aa)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "myep" 1) (("2" (case "zz-ep2 >= -bb/(2*aa)") (("1" (assert) nil nil) ("2" (expand "ep2" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "zz < -bb/(2*aa)") (("1" (hide 1) (("1" (hide 1) (("1" (skosimp*) (("1" (name "ep2" "-zz-bb/(2*aa)") (("1" (case "ep2 > 0") (("1" (name "myep" "min(ep2,epsilon!1)") (("1" (name "xy" "zz+myep/2") (("1" (inst + "xy") (("1" (split) (("1" (replace -1 :dir rl) (("1" (assert) (("1" (expand "abs" +) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (replace -3 -1 :dir rl) (("1" (expand "min" -1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "myep > 0") (("1" (assert) nil nil) ("2" (expand "myep" 1) (("2" (expand "min" 1) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "quad_min_mono_dec") (("2" (inst - "aa" "bb" "cc" "zz" "xy") (("2" (assert) (("2" (assert) (("2" (hide 2) (("2" (split +) (("1" (case "myep > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "myep" +) (("2" (expand "min" +) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "xy" +) (("2" (case "zz + myep <= -bb/(2*aa)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "myep" 1) (("2" (case "ep2 + zz <= -bb/(2*aa)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "ep2" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "ep2" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (Sign type-eq-decl nil sign "reals/") (sign const-decl "Sign" sign "reals/") (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (quad_min_mono_dec formula-decl nil quad_minmax "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (xy skolem-const-decl "real" tca_3D nil) (ep2 skolem-const-decl "real" tca_3D nil) (myep skolem-const-decl "{p: real | p <= ep2 AND p <= epsilon!1}" tca_3D nil) (quad_min_mono_inc formula-decl nil quad_minmax "reals/") (xy skolem-const-decl "real" tca_3D nil) (myep skolem-const-decl "{p: real | p <= ep2 AND p <= epsilon!1}" tca_3D nil) (ep2 skolem-const-decl "real" tca_3D nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (delta!1 skolem-const-decl "posreal" tca_3D nil) (t!1 skolem-const-decl "real" tca_3D nil) (df skolem-const-decl "[real -> real]" tca_3D nil) (xx!1 skolem-const-decl "real" tca_3D nil) (sq_0 formula-decl nil sq "reals/") (tca_3D_vz_zero formula-decl nil tca_3D nil) (sq_eq_0 formula-decl nil sq "reals/") (* const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_ge2 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (xx!1 skolem-const-decl "real" tca_3D nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (zero const-decl "Vector" vectors_2D "vectors/") (tca_3D_vect2_zero formula-decl nil tca_3D nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (sqv_zero formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (cyl_norm_sq_diff_cont formula-decl nil tca_3D nil) (df skolem-const-decl "[real -> real]" tca_3D nil) (vect2_scal formula-decl nil vect_3D_2D "vectors/") (vz_scal formula-decl nil vectors_3D "vectors/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (vz_distr_add formula-decl nil vectors_3D "vectors/") (vect2_add formula-decl nil vect_3D_2D "vectors/") (continuous? const-decl "bool" continuity_ms_def "analysis/") (continuous_at? const-decl "bool" continuity_ms_def "analysis/") (member const-decl "bool" sets nil) (ball const-decl "set[T]" metric_spaces "analysis/") (real_dist const-decl "nnreal" real_metric_space "analysis/") (t!1 skolem-const-decl "real" tca_3D nil) (delta!1 skolem-const-decl "posreal" tca_3D nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (nonneg_real_min application-judgement "{z: nonneg_real | z <= x AND z <= y}" real_defs nil) (tz!1 skolem-const-decl "nnreal" tca_3D nil) (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil) (H formal-const-decl "posreal" tca_3D nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "Vector" vectors_2D "vectors/") (D formal-const-decl "posreal" tca_3D nil) (sq const-decl "nonneg_real" sq "reals/") (vect2 const-decl "Vect2" vect_3D_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (real_times_real_is_real application-judgement "real" reals nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (tca_3D_id formula-decl nil tca_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (tca_3D const-decl "nnreal" tca_3D nil) (* const-decl "Vector" vectors_3D "vectors/") (+ const-decl "Vector" vectors_3D "vectors/") (Vector type-eq-decl nil vectors_3D "vectors/") (cyl_norm_sq const-decl "nnreal" tca_3D nil) (cyl_norm_min_exists_inf formula-decl nil tca_3D nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (< const-decl "bool" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (quadratic const-decl "real" quadratic "reals/")) shostak)) (tca_3D_conflict 0 (tca_3D_conflict-1 nil 3487083368 ("" (skeep) (("" (ground) (("1" (expand "conflict?") (("1" (skosimp*) (("1" (lemma "conflict_at_cyl_norm_sq") (("1" (inst - "s" "nnt!1" "v") (("1" (assert) (("1" (lemma "tca_3D_def") (("1" (inst - "nnt!1" "s" "v") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "conflict?") (("2" (inst + "tca_3D(s,v)") (("2" (lemma "conflict_at_cyl_norm_sq") (("2" (inst - "s" "tca_3D(s,v)" "v") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (tca_3D_def formula-decl nil tca_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D "vect_analysis/") (sq_nz_pos application-judgement "posreal" sq "reals/") (conflict_at_cyl_norm_sq formula-decl nil tca_3D nil) (conflict? const-decl "bool" space_3D nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (tca_3D const-decl "nnreal" tca_3D nil)) shostak)) (tca_3D_conflict_at 0 (tca_3D_conflict_at-1 nil 3487083490 ("" (skeep) (("" (rewrite "tca_3D_conflict") (("" (rewrite "conflict_at_cyl_norm_sq") (("" (assert) nil nil)) nil)) nil)) nil) ((tca_3D_conflict formula-decl nil tca_3D nil) (real nonempty-type-from-decl nil reals nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (tca_3D const-decl "nnreal" tca_3D nil) (nnreal 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) (conflict_at_cyl_norm_sq formula-decl nil tca_3D nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (tca_3D_left_decreasing 0 (tca_3D_left_decreasing-1 nil 3487679489 ("" (skeep) (("" (lemma "convex_btw_pt_left_lt") (("" (inst - "nnt" "tca_3D(s,v)" "cyl_norm_sq_fun(s,v)(pt)" "cyl_norm_sq_fun(s,v)" "pt") (("" (assert) (("" (lemma "cyl_norm_sq_fun_convex") (("" (inst?) (("" (assert) (("" (lemma "tca_3D_def") (("" (inst - "nnt" "s" "v") (("" (assert) (("" (expand "cyl_norm_sq_fun") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convex_btw_pt_left_lt formula-decl nil convex_functions "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (tca_3D_def formula-decl nil tca_3D nil) (cyl_norm_sq_fun_convex formula-decl nil tca_3D nil) (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (tca_3D const-decl "nnreal" tca_3D nil) (Vect3 type-eq-decl nil vectors_3D_def "vectors/") (nnreal type-eq-decl nil real_types nil) (>= 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)) shostak)) (tca_3D_right_increasing 0 (tca_3D_right_increasing-1 nil 3487680435 ("" (skeep) (("" (lemma "convex_btw_pt_left_lt") (("" (inst - "tca_3D(s,v)" "pt" "cyl_norm_sq_fun(s,v)(nnt)" "cyl_norm_sq_fun(s,v)" "nnt") (("" (assert) (("" (lemma "cyl_norm_sq_fun_convex") (("" (inst?) (("" (assert) (("" (lemma "tca_3D_def") (("" (inst-cp - "nnt" "s" "v") (("" (inst - "pt" "s" "v") (("" (expand "cyl_norm_sq_fun") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convex_btw_pt_left_lt formula-decl nil convex_functions "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (tca_3D_def formula-decl nil tca_3D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cyl_norm_sq_fun_convex formula-decl nil tca_3D nil) (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil) (tca_3D const-decl "nnreal" tca_3D nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Vect3 type-eq-decl nil vectors_3D_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)) nil)))
¤ Dauer der Verarbeitung: 1.82 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26