| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 MB |
|
Quelle circle_optimum_2D.prfSprache: Lisp |
|||||||||||||||
|
(circle_optimum_2D (intersects_circle_fun_scal 0 (intersects_circle_fun_scal-1 nil 3527949260 ("" (case "FORALL (R: posreal, c: Vect2, k: posreal, v: Vect2): intersects_circle_fun?(v, c, R) IMPLIES intersects_circle_fun?(k * v, c, R)") (("1" (skeep) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst - "R" "c" "1/k" "k*v") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "intersects_circle_fun?") (("2" (flatten) (("2" (case "v = zero") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case "k*v /= zero") (("1" (assert) (("1" (flatten) (("1" (lemma "Delta_scal[R]") (("1" (inst - "-c" "k" "v") (("1" (replace -1) (("1" (hide -1) (("1" (mult-by -1 "sq(k)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (mult-by -2 "k") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (expand "zero") (("2" (decompose-equality -1) (("2" (decompose-equality +) (("1" (mult-by 1 "k") (("1" (rewrite "vx_scal") (("1" (assert) nil nil)) nil)) nil) ("2" (mult-by 1 "k") (("2" (rewrite "vy_scal") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (zero const-decl "Vector" vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (sqv_neg formula-decl nil vectors_2D "vectors/") (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) (sq_nz_pos application-judgement "posreal" sq "reals/") (vx_scal formula-decl nil vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (vy_scal formula-decl nil vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (Delta_scal formula-decl nil horizontal nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (sq const-decl "nonneg_real" sq "reals/") (Delta const-decl "real" horizontal nil) (* const-decl "real" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (- const-decl "Vector" vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (scal_assoc formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/")) shostak)) (intersects_circle_fun_def 0 (intersects_circle_fun_def-1 nil 3527524122 ("" (skeep) (("" (case "v = zero") (("1" (replace -1) (("1" (expand "intersects_circle_fun?") (("1" (expand "circle?") (("1" (expand "segment?") (("1" (ground) (("1" (inst + "zero") (("1" (assert) (("1" (rewrite "sq_eq" 1 :dir rl) (("1" (rewrite "sq_norm") nil nil)) nil)) nil)) nil) ("2" (skeep -1) (("2" (skeep -2) (("2" (replace -2) (("2" (assert) (("2" (rewrite "sqrt_eq" 1 :dir rl) (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("1" (expand "intersects_circle_fun?") (("1" (flatten) (("1" (inst + "Theta_D[R](-c,v,1)*v") (("1" (split +) (("1" (expand "circle?") (("1" (lemma "Theta_D_unique[R]") (("1" (inst - "v" "-c" "Theta_D[R](-c, v, 1)") (("1" (assert) (("1" (rewrite "sqrt_eq" :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (hide-all-but (-1 1)) (("1" (grind :exclude ("norm" "Theta_D")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "segment?") (("2" (inst?) (("2" (lemma "Theta_D_ge_0[R]") (("2" (case "NOT sqv(-c) <= sq(R)") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (split -) (("1" (lemma "Theta_D_le[R]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -4) (("2" (hide -2) (("2" (lemma "horizontal_los_inside_Theta[R]") (("2" (inst?) (("2" (inst - "0") (("2" (assert) (("2" (lemma "Theta_D_unique[R]") (("2" (inst?) (("2" (inst - "0") (("2" (assert) (("2" (lemma "Theta_D_le[R]") (("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) ("2" (skeep -) (("2" (expand "segment?") (("2" (skeep -2) (("2" (replaces -2) (("2" (expand "intersects_circle_fun?") (("2" (case "NOT Delta[R](-c, v) >= 0") (("1" (hide 2) (("1" (rewrite "Delta_ge_0") (("1" (inst + "t") (("1" (expand "circle?") (("1" (rewrite "sqrt_eq" 1 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (grind :exclude "norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case "t = 0") (("1" (replace -1) (("1" (expand "circle?") (("1" (assert) (("1" (rewrite "sqrt_le" 2 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "circle?") (("2" (lemma "horizontal_conflict[norm(c)]") (("1" (inst - "v" "-c") (("1" (flatten) (("1" (hide -2) (("1" (split -) (("1" (flatten) (("1" (split -) (("1" (hide-all-but -1) (("1" (rewrite "sqrt_lt" :dir rl) (("1" (assert) (("1" (rewrite "sqrt_sqv_norm") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 2)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "horizontal_conflict?") (("2" (inst + "t") (("2" (rewrite "sqrt_lt" 1 :dir rl) (("2" (assert) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_le" 4 :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (assert) (("2" (hide -1) (("2" (grind :exclude "norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (segment? const-decl "bool" circle_optimum_2D nil) (sqrt_eq formula-decl nil sqrt "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (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) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sq_eq formula-decl nil sq "reals/") (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (sq_norm formula-decl nil vectors_2D "vectors/") (norm_neg formula-decl nil vectors_2D "vectors/") (sub_zero_left formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (scal_zero formula-decl nil vectors_2D "vectors/") (circle? const-decl "bool" circle_optimum_2D nil) (sqrt_le formula-decl nil sqrt "reals/") (horizontal_conflict formula-decl nil horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_lt formula-decl nil sqrt "reals/") (horizontal_conflict? const-decl "bool" horizontal nil) (dot_zero_left formula-decl nil vectors_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (neg_zero formula-decl nil vectors_2D "vectors/") (norm_zero formula-decl nil vectors_2D "vectors/") (norm_eq_0 formula-decl nil vectors_2D "vectors/") (Delta_ge_0 formula-decl nil horizontal nil) (v skolem-const-decl "Vect2" circle_optimum_2D nil) (c skolem-const-decl "Vect2" circle_optimum_2D nil) (- const-decl "Vector" vectors_2D "vectors/") (Delta const-decl "real" horizontal nil) (R skolem-const-decl "posreal" circle_optimum_2D nil) (* const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Theta_D const-decl "real" horizontal nil) (Theta_D_ge_0 formula-decl nil horizontal nil) (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (horizontal_los_inside_Theta formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "real" vectors_2D "vectors/") (Theta_D_le formula-decl nil horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (<= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sqv_neg formula-decl nil vectors_2D "vectors/") (Theta_D_unique formula-decl nil horizontal nil)) nil)) (intersects_circle_fun_inc 0 (intersects_circle_fun_inc-1 nil 3527947389 ("" (case "FORALL (R: posreal, c: Vect2, u, v: Vect2): sqv(u) = 1 AND sqv(v) = 1 AND intersects_circle_fun?(v, c, R) AND ^(v) * c <= ^(u) * c IMPLIES intersects_circle_fun?(u, c, R)") (("1" (skeep) (("1" (inst - "R" "c" "^(u)" "^(v)") (("1" (assert) (("1" (split -) (("1" (lemma "intersects_circle_fun_scal") (("1" (inst - "R" "c" "1/norm(u)" "u") (("1" (assert) (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil) ("2" (split +) (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "norm_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (ground) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (ground) (("3" (lemma "norm_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^") (("2" (rewrite "sqv_scal") (("2" (rewrite "sq_div") (("1" (rewrite "sq_norm") (("1" (assert) nil nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "^") (("3" (rewrite "sqv_scal") (("3" (rewrite "sq_div") (("1" (rewrite "sq_norm") (("1" (assert) nil nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "intersects_circle_fun_scal") (("4" (inst - "R" "c" "1/norm(v)" "v") (("1" (assert) (("1" (expand "^") (("1" (propax) nil nil)) nil)) nil) ("2" (split +) (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "norm_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (ground) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "norm_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (case "FORALL (zpt:Nz_vect2): ^(^(zpt)) = ^(zpt)") (("1" (inst-cp - "u") (("1" (inst - "v") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (expand "^" + 1) (("2" (typepred "^(zpt)") (("2" (assert) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (label "sqvuv" (-1 -2)) (("2" (case "^(v) = v AND ^(u) = u") (("1" (flatten) (("1" (replaces -1) (("1" (replaces -1) (("1" (hide "sqvuv") (("1" (expand "intersects_circle_fun?") (("1" (case "NOT (v = zero OR u = zero)") (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (label "uvnz" (1 2)) (("1" (hide "uvnz") (("1" (case "FORALL (bl1,bl2:bool): (bl1 OR bl2) IFF (bl1 OR (bl2 AND not bl1))") (("1" (label "final" 1) (("1" (hide "final") (("1" (rewrite -1) (("1" (hide -1) (("1" (reveal "final") (("1" (split -) (("1" (split +) (("1" (expand "Delta") (("1" (reveal "sqvuv") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (case "sq(u*perpR(c)) <= sq(v*perpR(c))") (("1" (hide -4) (("1" (grind) nil nil)) nil) ("2" (hide (-2 2)) (("2" (lemma "orthogonal_basis") (("2" (inst - "c" "perpR(c)" _) (("2" (inst-cp - "u") (("2" (inst - "v") (("2" (assert) (("2" (case "c /= zero AND perpR(c) /= zero AND orthogonal?(c, perpR(c))") (("1" (flatten) (("1" (assert) (("1" (lemma "orthogonal_basis_sqv") (("1" (inst?) (("1" (assert) (("1" (label "ddvc1" -3) (("1" (hide "ddvc1") (("1" (label "ddvc2" -1) (("1" (hide "ddvc2") (("1" (lemma "orthogonal_basis_sqv") (("1" (inst?) (("1" (assert) (("1" (reveal "ddvc1") (("1" (reveal "ddvc2") (("1" (delabel "ddvc1") (("1" (delabel "ddvc2") (("1" (case "sqv(perpR(c)) = sqv(c)") (("1" (replace -1) (("1" (hide -1) (("1" (reveal "sqvuv") (("1" (replace -1) (("1" (replace -2) (("1" (case "sq(u*c) >= sq(v*c)") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (mult-by 3 "sqv(c)/sq(sqv(c))") (("1" (mult-by -1 "sqv(c)/sq(sqv(c))") (("1" (ground) nil nil) ("2" (real-props) nil nil)) nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) (("2" (rewrite "sq_ge") (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sq_ge") (("1" (hide-all-but (-8 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-8 -9 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (flatten) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "c = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (expand "perpR") (("2" (flatten) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (-1 -3 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "Delta_ge_0_2[R]") (("2" (inst?) (("2" (assert) (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but -1) (("2" (reveal "sqvuv") (("2" (split -) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "norm(u) = 1 and norm(v) = 1") (("1" (expand "^" 1) (("1" (flatten) (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (rewrite "sqrt_eq" -1 :dir rl) (("2" (rewrite "sqrt_eq" -2 :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_sqv_norm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (replace -4) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (replace -4) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_eq formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_1 formula-decl nil sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sqv_zero formula-decl nil vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (Delta_ge_0_2 formula-decl nil horizontal nil) (orthogonal? const-decl "bool" vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (c skolem-const-decl "Vect2" circle_optimum_2D nil) (pos_div_ge formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (sq_ge formula-decl nil sq "reals/") (div_mult_pos_ge1 formula-decl nil real_props nil) (orthogonal_basis_sqv formula-decl nil basis_2D "vectors/") (perpR_eq_zero formula-decl nil perpendicular_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (sq_0 formula-decl nil sq "reals/") (orthogonal_basis formula-decl nil basis_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (perpR const-decl "Vect2" perpendicular_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (Delta const-decl "real" horizontal nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (sqv_neg formula-decl nil vectors_2D "vectors/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (scal_1 formula-decl nil vectors_2D "vectors/") (norm_normalize formula-decl nil vectors_2D "vectors/") (v skolem-const-decl "Vect2" circle_optimum_2D nil) (sq_div formula-decl nil sq "reals/") (sq_1 formula-decl nil sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (sq_norm formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_scal formula-decl nil vectors_2D "vectors/") (intersects_circle_fun_scal formula-decl nil circle_optimum_2D nil) (norm_eq_0 formula-decl nil vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_ge1 formula-decl nil extra_real_props nil) (div_mult_pos_neg_gt1 formula-decl nil extra_real_props 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) (u skolem-const-decl "Vect2" circle_optimum_2D 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) (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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (<= const-decl "bool" reals nil) (* const-decl "real" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vector type-eq-decl nil vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (Normalized type-eq-decl nil vectors_2D "vectors/") (^ const-decl "Normalized" vectors_2D "vectors/")) nil)) (inter_circle_max_time_TCC1 0 (inter_circle_max_time_TCC1-1 nil 3527524768 ("" (subtype-tcc) nil nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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) (/= const-decl "boolean" notequal nil) (- const-decl "Vector" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (Delta const-decl "real" horizontal nil) (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (inter_circle_max_time_TCC2 0 (inter_circle_max_time_TCC2-1 nil 3527524768 ("" (skeep) (("" (lemma "intersects_circle_fun_def") (("" (inst?) (("" (assert) (("" (skeep -1) (("" (expand "segment?") (("" (skeep -2) (("" (replace -2) (("" (hide -2) (("" (expand "circle?") (("" (lemma "Theta_D_unique[R]") (("" (inst?) (("" (inst - "-c") (("" (assert) (("" (expand "intersects_circle_fun?") (("" (flatten) (("" (assert) (("" (flatten) (("" (hide -2) (("" (split -) (("1" (lemma "Theta_D_le[R]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "sqrt_eq" 1 :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (assert) (("2" (hide-all-but (-1 1)) (("2" (grind :exclude "norm") 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) ((intersects_circle_fun_def formula-decl nil circle_optimum_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (segment? const-decl "bool" circle_optimum_2D nil) (circle? const-decl "bool" circle_optimum_2D nil) (nnreal type-eq-decl nil real_types nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (Theta_D_le formula-decl nil horizontal nil) (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_eq formula-decl nil sqrt "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (sqv_neg formula-decl nil vectors_2D "vectors/") (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (- const-decl "Vector" vectors_2D "vectors/") (Theta_D_unique formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real 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)) (inter_circle_max_time_scal 0 (inter_circle_max_time_scal-1 nil 3529411095 ("" (skeep) (("" (cross-mult 1) (("" (expand "inter_circle_max_time") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (assert) (("" (ground) (("1" (lemma "Theta_D_scal[R]") (("1" (inst?) (("1" (assert) (("1" (expand "intersects_circle_fun?") (("1" (flatten) (("1" (assert) (("1" (expand "sign" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil) ("3" (expand "intersects_circle_fun?") (("3" (assert) (("3" (flatten) (("3" (assert) (("3" (split +) (("1" (flatten) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "Delta_scal[R]") (("2" (inst?) (("2" (assert) (("2" (mult-by 1 "sq(pt)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (mult-by 1 "pt") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (case "(1/pt)*(pt*v) = zero") (("1" (assert) nil nil) ("2" (replace -2) (("2" (assert) nil nil)) nil)) nil) ("5" (expand "intersects_circle_fun?") (("5" (flatten) (("5" (split 3) (("1" (flatten) (("1" (case "(1/pt)*(pt*v) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "Delta_scal[R]") (("2" (inst?) (("2" (assert) (("2" (mult-by -2 "sq(pt)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (mult-by -2 "pt") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (inter_circle_max_time const-decl "nnreal" circle_optimum_2D nil) (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (nonzero_real 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) (times_div2 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" 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) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (sqv_neg formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (sign const-decl "Sign" sign "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Theta_D_scal formula-decl nil horizontal nil) (scal_zero formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "real" vectors_2D "vectors/") (Delta_scal formula-decl nil horizontal nil) (Delta const-decl "real" horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (both_sides_times_pos_ge1 formula-decl nil real_props nil) (scal_1 formula-decl nil vectors_2D "vectors/") (scal_assoc formula-decl nil vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil)) shostak)) (inter_circle_max_time_def 0 (inter_circle_max_time_def-1 nil 3527525027 ("" (skeep) (("" (name "tcm" "inter_circle_max_time(v, c, R)") (("" (replace -1) (("" (assert) (("" (split +) (("1" (flatten) (("1" (lemma "intersects_circle_fun_def") (("1" (inst?) (("1" (assert) (("1" (case "NOT circle?(c, R)(tcm * v)") (("1" (hide 2) (("1" (expand "circle?") (("1" (expand "inter_circle_max_time") (("1" (lift-if) (("1" (ground) (("1" (lemma "Theta_D_unique[R]") (("1" (inst?) (("1" (inst - "-c") (("1" (assert) (("1" (copy -4) (("1" (expand "intersects_circle_fun?" -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "sqrt_eq" -3 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (assert) (("1" (hide-all-but (-3 2)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (skeep -3) (("2" (expand "segment?") (("2" (skeep -4) (("2" (assert) (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (expand "inter_circle_max_time") (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (lemma "Theta_D_unique[R]") (("1" (inst - _ _ "nnt") (("1" (inst?) (("1" (assert) (("1" (expand "intersects_circle_fun?") (("1" (flatten) (("1" (assert) (("1" (copy -5) (("1" (expand "circle?" -1) (("1" (case "sqv(-c+nnt*v) = sq(R)") (("1" (assert) (("1" (case "nnt = tcm") (("1" (assert) nil nil) ("2" (assert) (("2" (case "nnt = 0") (("1" (replace -1) (("1" (assert) (("1" (rewrite "norm_scal") (("1" (expand "abs" +) (("1" (lemma "posreal_times_posreal_is_posreal") (("1" (inst?) (("1" (assert) nil nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "nnt < tcm") (("1" (mult-by -1 "norm(v)") (("1" (case "forall (aannrr:nnreal): aannrr = abs(aannrr)") (("1" (inst-cp - "nnt") (("1" (inst - "tcm") (("1" (replace -1 -3) (("1" (replace -2 -3) (("1" (hide (-1 -2)) (("1" (rewrite "norm_scal" :dir rl) (("1" (rewrite "norm_scal" :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "Theta_D_le[R]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "norm_eq_sqv_eq" 1) (("2" (hide-all-but (-1 1)) (("2" (grind :exclude "norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (replace -1 :dir rl) (("2" (assert) (("2" (case "NOT intersects_circle_fun?(v, c, R)") (("1" (lemma "intersects_circle_fun_def") (("1" (inst?) (("1" (assert) (("1" (inst + "nnt*v") (("1" (assert) (("1" (expand "segment?") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inter_circle_max_time const-decl "nnreal" circle_optimum_2D nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (norm_eq_sqv_eq formula-decl nil vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (Theta_D_le formula-decl nil horizontal nil) (both_sides_times_pos_lt1 formula-decl nil real_props 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) (< const-decl "bool" reals nil) (norm_scal formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (norm_eq_0 formula-decl nil vectors_2D "vectors/") (v skolem-const-decl "Vect2" circle_optimum_2D nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (norm_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (circle? const-decl "bool" circle_optimum_2D nil) (NOT const-decl "[bool -> bool]" booleans nil) (segment? const-decl "bool" circle_optimum_2D nil) (norm_neg formula-decl nil vectors_2D "vectors/") (sub_zero_left formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (Theta_D_unique formula-decl nil horizontal nil) (- const-decl "Vector" vectors_2D "vectors/") (sqv_neg formula-decl nil vectors_2D "vectors/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "Vector" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_eq formula-decl nil sqrt "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (intersects_circle_fun_def formula-decl nil circle_optimum_2D nil)) shostak)) (inter_circle_max_norm_scal 0 (inter_circle_max_norm_scal-1 nil 3527585618 ("" (skeep) (("" (expand "inter_circle_max_norm") (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (expand "inter_circle_max_time") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "Theta_D_scal[R]") (("1" (inst?) (("1" (split -) (("1" (assert) (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (assert) (("1" (expand "sign" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "intersects_circle_fun?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil) ("3" (case "v = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality -) (("2" (rewrite "vx_scal") (("2" (rewrite "vy_scal") (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "intersects_circle_fun?") (("2" (flatten) (("2" (lemma "Delta_scal[R]") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (split -) (("1" (flatten) (("1" (case "NOT Delta[R](-c,v) >=0") (("1" (hide 2) (("1" (mult-by 1 "sq(pt)") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "v/=zero") (("1" (assert) (("1" (hide -1) (("1" (flatten) (("1" (assert) (("1" (mult-by 2 "pt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "v = zero") (("1" (assert) nil nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality -) (("2" (rewrite "vy_scal") (("2" (rewrite "vx_scal") (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 1) (("3" (expand "intersects_circle_fun?") (("3" (flatten) (("3" (split -) (("1" (flatten) (("1" (assert) (("1" (lemma "Delta_scal[R]") (("1" (inst?) (("1" (assert) (("1" (case "NOT Delta[R](-c,pt*v) >=0") (("1" (mult-by -2 "sq(pt)") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (case "pt*v /= zero") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (mult-by -4 "pt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (expand "zero") (("2" (decompose-equality -) (("2" (rewrite "vx_scal") (("2" (rewrite "vy_scal") (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inter_circle_max_norm const-decl "nnreal" circle_optimum_2D nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" 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) (/= const-decl "boolean" notequal 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/") (nzreal nonempty-type-eq-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (intersects_circle_fun? const-decl "bool" circle_optimum_2D nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sign const-decl "Sign" sign "reals/") (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (norm_scal formula-decl nil vectors_2D "vectors/") (Theta_D_scal formula-decl nil horizontal 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (scal_zero formula-decl nil vectors_2D "vectors/") (norm_zero formula-decl nil vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "Vector" vectors_2D "vectors/") (vy_scal formula-decl nil vectors_2D "vectors/") (vx_scal formula-decl nil vectors_2D "vectors/") (inter_circle_max_time const-decl "nnreal" circle_optimum_2D nil) (Delta_scal formula-decl nil horizontal nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_neg formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (Delta const-decl "real" horizontal nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (sq const-decl "nonneg_real" sq "reals/") (* const-decl "real" vectors_2D "vectors/") (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (dot_zero_right formula-decl nil vectors_2D "vectors/")) shostak)) (max_norm_increasing 0 (max_norm_increasing-1 nil 3527584737 ("" (case "FORALL (R: posreal, c: Vect2, u, v: Vect2): norm(u) = 1 AND norm(v) = 1 IMPLIES ^(v) * c <= ^(u) * c IMPLIES inter_circle_max_norm(v, c, R) <= inter_circle_max_norm(u, c, R)") (("1" (skeep) (("1" (split -) (("1" (inst - "R" "c" "^(u)" "^(v)") (("1" (assert) (("1" (flatten) (("1" (split -) (("1" (expand "^") (("1" (lemma "inter_circle_max_norm_scal") (("1" (inst - "R" "c" _ _) (("1" (inst-cp - "v" "1/norm(v)") (("1" (inst - "u" "1/norm(u)") (("1" (assert) nil nil) ("2" (split +) (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "norm_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (ground) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "norm_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (ground) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (vvz:Vect2): norm(vvz) = 1 IMPLIES ^(vvz) = vvz") (("1" (inst-cp - "^(v)") (("1" (inst - "^(u)") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (expand "^") (("2" (assert) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skeep) (("3" (replace -2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2) (("2" (flatten) (("2" (case "v = zero") (("1" (hide -2) (("1" (replace -1) (("1" (expand "inter_circle_max_norm") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replaces -1) (("2" (assert) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (case "FORALL (vvz:Vect2): norm(vvz) = 1 IMPLIES ^(vvz) = vvz") (("1" (inst-cp - "v") (("1" (inst - "u") (("1" (assert) (("1" (replaces -1) (("1" (replaces -1) (("1" (label "normu" -1) (("1" (label "normv" -2) (("1" (case "u/=zero AND v/=zero") (("1" (flatten) (("1" (label "uvnz" (1 2)) (("1" (hide "uvnz") (("1" (case "sqv(u) = 1 AND sqv(v) = 1") (("1" (flatten) (("1" (label "sqvu" -1) (("1" (label "sqvv" -2) (("1" (hide ("sqvu" "sqvv" "normu" "normv")) (("1" (expand "inter_circle_max_norm") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (name "pu" "inter_circle_max_time(u, c, R) * u") (("1" (name "pv" "inter_circle_max_time(v, c, R) * v") (("1" (lemma "law_cosines_alt") (("1" (inst - "zero" "c" "pu") (("1" (lemma "law_cosines_alt") (("1" (inst - "zero" "c" "pv") (("1" (assert) (("1" (lemma "law_cosines_alt") (("1" (inst - "c" "pu" "pv") (("1" (assert) (("1" (label "dlem" -1) (("1" (hide "dlem") (("1" (expand "dist") (("1" (rewrite "sq_sqrt") (("1" (rewrite "sq_sqrt") (("1" (rewrite "sq_sqrt") (("1" (rewrite "sq_sqrt") (("1" (rewrite "sq_sqrt") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (case "sq(norm(pv)) <= sq(norm(pu))") (("1" (rewrite "sq_le" -1) (("1" (hide-all-but (-1 1)) (("1" (expand "pv") (("1" (expand "pu") (("1" (rewrite "norm_scal") (("1" (rewrite "norm_scal") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "sq(norm(pv-c)) = sq(norm(pu-c))") (("1" (replace -1) (("1" (hide -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) (("1" (case "c*(c-pu) <= c*(c-pv)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "c*pv <= c*pu") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (expand "intersects_circle_fun?") (("2" (case "FORALL (b1,b2:bool): (b1 OR b2) IFF (b1 OR (b2 AND NOT b1))") (("1" (reveal "uvnz") (("1" (assert) (("1" (hide "uvnz") (("1" (rewrite -1) (("1" (label "hyp1" -4) (("1" (hide "hyp1") (("1" (rewrite -1) (("1" (reveal "hyp1") (("1" (delabel "hyp1") (("1" (hide -2) (("1" (flatten) (("1" (case "NOT (sq(-c * u) + sq(R) - sqv(c) >= 0 AND sq(-c * v) + sq(R) - sqv(c) >= 0)") (("1" (lemma "Delta_discr2b[R]") (("1" (hide-all-but (-1 -2 -6 1)) (("1" (expand "discr2b") (("1" (split +) (("1" (inst?) (("1" (assert) (("1" (reveal "sqvu") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (inst?) (("2" (assert) (("2" (reveal "sqvv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (ground) (("1" (hide (-6 -7)) (("1" (expand "pv") (("1" (expand "pu") (("1" (case "inter_circle_max_time(v, c, R) <=inter_circle_max_time(u, c, R)") (("1" (mult-ineq -1 -8) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand "inter_circle_max_time") (("2" (expand "Theta_D") (("2" (expand "root2b") (("2" (expand "discr2b") (("2" (reveal ("sqvu" "sqvv")) (("2" (replace -1) (("2" (replace -2) (("2" (assert) (("2" (case "FORALL (zzpr:real): zzpr/1 = zzpr") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (hide -1) (("1" (case-replace "-(-c * v) = v*c") (("1" (case-replace "-(-c * u) = u*c") (("1" (hide -1 -2) (("1" (case "sqrt(sq(-c * v) + sq(R) - sqv(c)) <= sqrt(sq(-c * u) + sq(R) - sqv(c))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "sqrt_le") (("2" (lemma "sq_le") (("2" (inst - "v*c" "u*c") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (mult-by -2 "inter_circle_max_time(u, c, R)") (("2" (mult-by 1 "inter_circle_max_time(v, c, R)") (("2" (expand "pv" +) (("2" (expand "pu" +) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-1 -9 1)) (("3" (grind) nil nil)) nil) ("4" (reveal "dlem") (("4" (case "sq(dist(pv, c)) = sq(R) AND sq(dist(pu, c)) = sq(R)") (("1" (flatten) (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) (("1" (case "sq(dist(pv,pu)) = sqv(pu-pv)") (("1" (replace -1) (("1" (hide -1) (("1" (both-sides "-" "sqv(pu-pv)" -1) (("1" (assert) (("1" (mult-by -1 "-1") (("1" (assert) (("1" (case "(pu*c-sqv(c))^2 + (pu*perpR(c))^2 = (pv*c-sqv(c))^2 + (pv*perpR(c))^2") (("1" (case "(pu * perpR(c)) ^ 2 >= (pv * perpR(c)) ^ 2 AND (pu * c - sqv(c)) ^ 2 > (pv * c - sqv(c)) ^ 2") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide -1) (("2" (lemma "orthogonal_basis") (("2" (case "FORALL (e1, e2, w1,w2: Vect2): e1 /= zero AND e2 /= zero AND orthogonal?(e1, e2) AND norm(e1) = norm(e2) AND sqv(w1) = sqv(w2) IM ((sq(w1*e1) >= sq(w2*e1) AND sq(w1*e2) <= sq(w2*e2)) OR (sq(w1*e1) < sq(w2*e1) AND sq(w1*e2) > sq( (("1" (hide -2) (("1" (inst - "c" "perpR(c)" _ _) (("1" (inst-cp - "v" "u") (("1" (inst - "pv-c" "pu-c") (("1" (assert) (("1" (case "perpR(c) /= zero AND orthogonal?(c, perpR(c))") (("1" (flatten) (("1" (assert) (("1" (case "norm(c) = norm(perpR(c)) AND sqv(v) = sqv(u) AND sqv(pv - c) = sqv(pu - c)") (("1" (flatten) (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (case "c*pv <= 0") (("1" (lemma "sq_gt") (("1" (inst - "-((pu-c)*c)" "-((pv-c)*c)") (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") (("1" (assert) (("1" (hide-all-but (1 6)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (typepred "sqv(c)") (("2" (grind) nil nil)) nil)) nil) ("3" (hide-all-but (-1 1 6)) (("3" (typepred "sqv(c)") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (mult-by 4 "inter_circle_max_time(v, c, R)") (("2" (assert) (("2" (hide-all-but (1 4)) (("2" (expand "pv") (("2" (grind :exclude "inter_circle_max_time") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (flatten) (("1" (name "puc" "inter_circle_max_time(u, c, R)") (("1" (name "pvc" "inter_circle_max_time(v, c, R)") (("1" (replaces -1) (("1" (replaces -1) (("1" (case "pvc <= puc") (("1" (case "sq(pvc) <= sq(puc)") (("1" (mult-ineq -1 -4) (("1" (rewrite "sq_times" :dir rl) (("1" (rewrite "sq_times" :dir rl) (("1" (split +) (("1" (hide-all-but (-1 1)) (("1" (expand "pvc") (("1" (expand "pu") (("1" (expand "puc") (("1" (expand "pv") (("1" (grind :exclude ("inter_circle_max_time" "perpR")) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_gt") (("2" (inst - "- (pu * c - sqv(c))" "-(pv * c - sqv(c))") (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") (("1" (flatten) (("1" (hide -1) (("1" (split -) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (case "c*pu <=0") (("1" (hide-all-but (-1 1 6)) (("1" (grind) nil nil)) nil) ("2" (mult-by 6 "puc") (("1" (hide-all-but (1 6)) (("1" (expand "pu") (("1" (expand "puc") (("1" (grind :exclude ("inter_circle_max_time")) nil nil)) nil)) nil)) nil) ("2" (case "puc = 0") (("1" (expand "puc" -1) (("1" (expand "pu" 2) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (mult-by 4 "pvc") (("1" (hide-all-but (1 4)) (("1" (typepred "sqv(c)") (("1" (expand "pvc") (("1" (expand "pv") (("1" (grind :exclude ("inter_circle_max_time")) nil nil)) nil)) nil)) nil)) nil) ("2" (case "pvc = 0") (("1" (replace -1) (("1" (assert) (("1" (replace -19 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (mult-by 5 "puc") (("1" (hide-all-but (1 5)) (("1" (typepred "sqv(c)") (("1" (expand "pu") (("1" (expand "puc") (("1" (grind :exclude ("inter_circle_max_time")) nil nil)) nil)) nil)) nil)) nil) ("2" (case "puc = 0") (("1" (replace -1) (("1" (assert) (("1" (replace -20 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_le") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "FORALL (a1,a2,b1,b2:nnreal): a1<=a2 AND b1<=b2 IMPLIES a1*b1<=a2*b2") (("1" (inst - "puc" "pvc" "-(c*u)" "-(c*v)") (("1" (assert) (("1" (split -) (("1" (hide-all-but (-1 6)) (("1" (expand "pv") (("1" (expand "pu") (("1" (expand "pvc") (("1" (expand "puc") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-18 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (mult-ineq -1 -2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sq_lt") (("2" (inst - "-(v*c)" "-(u*c)") (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (grind) nil nil)) nil) ("3" (hide-all-but (1 4)) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (reveal "sqvv") (("2" (reveal "sqvu") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "inter_circle_max_time_def") (("3" (inst - "R" "c" _) (("3" (inst-cp - "v") (("3" (inst - "u") (("3" (assert) (("3" (flatten) (("3" (hide (-2 -4 -6 -7)) (("3" (expand "circle?") (("3" (case "FORALL (vv1,vv2:Vect2): norm(vv1) = R AND norm(vv2) = R IMPLIES sqv(vv1) = sqv(vv2)") (("1" (rewrite -1) nil nil) ("2" (hide-all-but 1) (("2" (case "FORALL (vvv1:Vect2): norm(vvv1) = R IMPLIES sqv(vvv1) = sq(R)") (("1" (skeep) (("1" (inst-cp - "vv1") (("1" (inst - "vv2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (rewrite "sqrt_eq" 1 :dir rl) (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide (-1 -2)) (("2" (split +) (("1" (flatten) (("1" (case "c = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "perpR") (("2" (expand "zero") (("2" (flatten) (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skeep) (("2" (inst - "e1" "e2" _) (("2" (assert) (("2" (case "FORALL (w: Vect2): sqv(w) = sq((w * e1) / sqv(e1))*sqv(e1) + sq((w * e2) / sqv(e2))*sqv(e2)") (("1" (hide -5) (("1" (inst-cp - "w1") (("1" (inst - "w2") (("1" (case "sqv(w1) = sqv(w2)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (case "sqv(e1) = sqv(e2)") (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (mult-by -1 "sqv(e1)") (("1" (expand "sq") (("1" (ground) nil nil)) nil)) nil) ("2" (rewrite "sqv_eq_0" :dir rl) nil nil)) nil) ("2" (rewrite "sqv_eq_0" :dir rl) nil nil)) nil) ("2" (rewrite "sqv_eq_0" :dir rl) nil nil)) nil) ("2" (rewrite "sqrt_eq" :dir rl) (("2" (rewrite "sqv_eq_0" :dir rl) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sqrt_eq" :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "w") (("2" (name "cv1" "sq((w * e1) / sqv(e1)) * sqv(e1) + sq((w * e2) / sqv(e2)) * sqv(e2)") (("2" (replace -1) (("2" (replace -5 +) (("2" (case "sqv(e1) = sqv(e2)") (("1" (replace -1 :dir rl) (("1" (rewrite "sqv_add") (("1" (expand "orthogonal?") (("1" (replace -3) (("1" (assert) (("1" (hide-all-but (1 2 3)) (("1" (expand "cv1") (("1" (rewrite "sqv_scal") (("1" (rewrite "sqv_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sqrt_eq" :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (rewrite "sqv_eq_0" :dir rl) (("3" (assert) (("3" (rewrite "sqv_eq_0" :dir rl) nil nil)) nil)) nil) ("4" (rewrite "sqv_eq_0" :dir rl) (("4" (rewrite "sqv_eq_0" :dir rl) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "sqv(pu-c) = sq(R) AND sqv(pv-c) = sq(R)") (("1" (flatten) (("1" (lemma "orthogonal_basis") (("1" (inst - "c" "perpR(c)" _) (("1" (inst-cp - "pu-c") (("1" (inst - "pv-c") (("1" (assert) (("1" (case "perpR(c) /= zero AND orthogonal?(c, perpR(c))") (("1" (flatten) (("1" (assert) (("1" (hide -1) (("1" (lemma "orthogonal_basis_sqv") (("1" (inst?) (("1" (assert) (("1" (replace -5) (("1" (hide -2) (("1" (lemma "orthogonal_basis_sqv") (("1" (inst?) (("1" (assert) (("1" (replace -4) (("1" (replace -1 -2) (("1" (hide (-1 -3)) (("1" (case "sqv(perpR(c)) = sqv(c)") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "dot_sub_left") (("1" (rewrite "dot_sub_left") (("1" (rewrite "dot_sub_left") (("1" (rewrite "dot_sub_left") (("1" (case "c*perpR(c) = 0") (("1" (replace -1) (("1" (assert) (("1" (case "c*c = sqv(c)") (("1" (replace -1) (("1" (case "FORALL (zpop:real): zpop^2 = sq(zpop)") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (mult-by 2 "sqv(c)/sq(sqv(c))") (("1" (assert) nil nil) ("2" (flatten) (("2" (cross-mult -1) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sqv" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "sqv_eq_0") nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "sqv_eq_0") nil nil)) nil)) nil) ("2" (flatten) (("2" (rewrite "sqv_eq_0") nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (case "c = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (expand "zero") (("2" --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.377Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26