| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 419 kB |
|
Quellcode-Bibliothek horizontal.prfSprache: Lisp |
|||||||||||||||
|
(horizontal (ss_nzv 0 (ss_nzv-1 nil 3432031102 ("" (judgement-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) (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "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" horizontal nil) (Ss_vect2 type-eq-decl nil horizontal nil) (comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil)) nil)) (ss_sp 0 (ss_sp-1 nil 3432031102 ("" (judgement-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) (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" horizontal nil) (Ss_vect2 type-eq-decl nil horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_plus_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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* 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)) nil)) (neg_ss 0 (neg_ss-1 nil 3431439330 ("" (skeep) (("" (rewrite "sqv_neg") (("" (assert) nil nil)) nil)) nil) ((sqv_neg formula-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "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" horizontal nil) (Ss_vect2 type-eq-decl nil horizontal nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) nil)) (neg_sp 0 (neg_sp-1 nil 3432031102 ("" (judgement-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) (>= const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_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) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (horizontal_conflict_sum_closed 0 (horizontal_conflict_sum_closed-4 nil 3467395174 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (skosimp*) (("" (case "nnt!1 = 0 and nnt!2 = 0") (("1" (flatten) (("1" (inst + "0") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)") (("1" (label "ttname" -1) (("1" (case "0<=tt AND tt<=1") (("1" (flatten) (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)") (("1" (label "newtname" -1) (("1" (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt") (("1" (flatten) (("1" (label "newttt" -1) (("1" (label "newtomtt" -2) (("1" (inst + "newt") (("1" (name "VV" "s + nnt!1 * v") (("1" (label "vvname" -1) (("1" (name "WW" "s + nnt!2 * w") (("1" (label "wwname" -1) (("1" (name "VVt" "s+nnt!1*v") (("1" (label "vvtname" -1) (("1" (name "WWt" "s+nnt!2*w") (("1" (label "wwtname" -1) (("1" (replace "wwname") (("1" (replace "vvname") (("1" (lemma "horiz_dist_convex_scaf") (("1" (inst - "VVt" "WWt-VVt") (("1" (case "s + newt * (v + w) = tt*VV+(1-tt)*WW") (("1" (label "vectfin" -1) (("1" (replace "vectfin") (("1" (assert) (("1" (lemma "convex_wtd_av_lt") (("1" (inst - "0" "LAMBDA (ttt: real): horiz_dist_scaf(VVt)(ttt, WWt - VVt)" "0" "1") (("1" (assert) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (assert) (("1" (case "VVt = VV AND VVt+(WWt-VVt) = WW") (("1" (flatten) (("1" (assert) (("1" (inst - "tt") (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (case-replace "VVt + (1 - tt) * (WWt - VVt) = tt * VV + (1 - tt) * WW") (("1" (assert) nil nil) ("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but ("vvtname" "vvname" "wwtname" "wwname" 1)) (("2" (replace "wwtname" + rl) (("2" (replace "vvtname" + rl) (("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("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" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (assert) (("2" (hide (2 3 4 5)) (("2" (hide-all-but ("newttt" "newtomtt" 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "(nnt!1*nnt!2)" "nnt!1 + nnt!2") (("1" (replace "newtname") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace "newtname" + rl) (("2" (replace "ttname" + rl) (("2" (hide-all-but (1 2)) (("2" (split 1) (("1" (field) nil nil) ("2" (field) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "nnt!2" "nnt!1 + nnt!2") (("1" (replace "ttname") (("1" (assert) (("1" (replace "ttname" + rl) (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict? const-decl "bool" horizontal nil) (nnreal 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) (= const-decl "[T, T -> boolean]" equalities nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (div_mult_pos_le1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (zero_times1 formula-decl nil real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (both_sides_times1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel2 formula-decl nil real_props nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnreal_div_posreal_is_nnreal judgement-tcc nil real_types nil) (nnt!2 skolem-const-decl "nnreal" horizontal nil) (nnt!1 skolem-const-decl "nnreal" horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (horiz_dist_convex_scaf formula-decl nil horizontal_dist_convexity nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (D formal-const-decl "posreal" horizontal nil) (real_minus_real_is_real application-judgement "real" reals nil) (convex_wtd_av_lt formula-decl nil convex_functions "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (scal_1 formula-decl nil vectors_2D "vectors/") (horiz_dist_scaf const-decl "real" horizontal_dist_convexity nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "Vector" vectors_2D "vectors/") (newt skolem-const-decl "real" horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil) (horizontal_conflict_sum_closed-3 nil 3467395009 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (skosimp*) (("" (case "nnt!1 = 0 and nnt!2 = 0") (("1" (flatten) (("1" (inst + "0") (("1" (assert) (("1" (replace -1) (("1" (assert) nil))))))))) ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)") (("1" (label "ttname" -1) (("1" (case "0<=tt AND tt<=1") (("1" (flatten) (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)") (("1" (label "newtname" -1) (("1" (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt") (("1" (flatten) (("1" (label "newttt" -1) (("1" (label "newtomtt" -2) (("1" (inst + "newt") (("1" (name "VV" "vect2(s) + nnt!1 * vect2(v)") (("1" (label "vvname" -1) (("1" (name "WW" "vect2(s) + nnt!2 * vect2(w)") (("1" (label "wwname" -1) (("1" (name "VVt" "s+nnt!1*v") (("1" (label "vvtname" -1) (("1" (name "WWt" "s+nnt!2*w") (("1" (label "wwtname" -1) (("1" (replace "wwname") (("1" (replace "vvname") (("1" (lemma "horiz_dist_convex_scaf") (("1" (inst - "VVt" "WWt-VVt") (("1" (case "vect2(s) + newt * vect2(v + w) = tt*VV+(1-tt)*WW") (("1" (label "vectfin" -1) (("1" (replace "vectfin") (("1" (assert) (("1" (lemma "convex_wtd_av_lt") (("1" (inst - "0" "LAMBDA (ttt): horiz_dist_scaf(VVt)(ttt, WWt - VVt)" "0" "1") (("1" (assert) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (assert) (("1" (case "vect2(VVt) = VV AND vect2(VVt)+vect2(WWt-VVt) = WW") (("1" (flatten) (("1" (assert) (("1" (inst - "tt") (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (case-replace "vect2(VVt) + (1 - tt) * vect2(WWt - VVt) = tt * VV + (1 - tt) * WW") (("1" (assert) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil))))))))))))))) ("2" (hide-all-but ("vvtname" "vvname" "wwtname" "wwname" 1)) (("2" (replace "wwtname" + rl) (("2" (replace "vvtname" + rl) (("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_sub") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vect2_scal") (("2" (hide-all-but 1) (("2" (grind) nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (assert) (("2" (hide (2 3 4 5)) (("2" (hide-all-but ("newttt" "newtomtt" 1)) (("2" (grind) nil))))))))))))))))))))))))))))))))))))) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "(nnt!1*nnt!2)" "nnt!1 + nnt!2") (("1" (replace "newtname") (("1" (propax) nil))) ("2" (assert) nil))))))))))))) ("2" (replace "newtname" + rl) (("2" (replace "ttname" + rl) (("2" (hide-all-but (1 2)) (("2" (split 1) (("1" (field) nil) ("2" (field) nil))))))))))))))))) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "nnt!2" "nnt!1 + nnt!2") (("1" (replace "ttname") (("1" (assert) (("1" (replace "ttname" + rl) (("1" (cross-mult 1) (("1" (assert) nil))))))))) ("2" (assert) nil))))))))) ("2" (assert) nil)))))))))) nil) nil nil) (horizontal_conflict_sum_closed-2 nil 3467392944 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (skosimp*) (("" (case "nnt!1 = 0 and nnt!2 = 0") (("1" (flatten) (("1" (inst + "0") (("1" (assert) (("1" (replace -1) (("1" (assert) nil))))))))) ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)") (("1" (label "ttname" -1) (("1" (case "0<=tt AND tt<=1") (("1" (flatten) (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)") (("1" (label "newtname" -1) (("1" (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt") (("1" (flatten) (("1" (label "newttt" -1) (("1" (label "newtomtt" -2) (("1" (inst + "newt") (("1" (name "VV" "s + nnt!1 * v") (("1" (label "vvname" -1) (("1" (name "WW" "s + nnt!2 * w") (("1" (label "wwname" -1) (("1" (name "VVt" "s+nnt!1*v") (("1" (label "vvtname" -1) (("1" (name "WWt" "s+nnt!2*w") (("1" (label "wwtname" -1) (("1" (replace "wwname") (("1" (replace "vvname") (("1" (lemma "horiz_dist_convex_scaf") (("1" (inst - "VVt" "WWt-VVt") (("1" (case "s + newt * (v + w) = tt*VV+(1-tt)*WW") (("1" (label "vectfin" -1) (("1" (replace "vectfin") (("1" (assert) (("1" (lemma "convex_wtd_av_lt") (("1" (inst - "0" "LAMBDA (ttt): horiz_dist_scaf(VVt)(ttt, WWt - VVt)" "0" "1") (("1" (assert) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (assert) (("1" (case "VVt = VV AND VVt+(WWt-VVt) = WW") (("1" (flatten) (("1" (assert) (("1" (inst - "tt") (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (case-replace "VVt + (1 - tt) * (WWt - VVt) = tt * VV + (1 - tt) * WW") (("1" (assert) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil))))))))))))))) ("2" (hide-all-but ("vvtname" "vvname" "wwtname" "wwname" 1)) (("2" (replace "wwtname" + rl) (("2" (replace "vvtname" + rl) (("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (hide-all-but 1) (("2" (grind) nil))))))))))))))))))))))))))))))))) ("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (assert) (("2" (hide (2 3 4 5)) (("2" (hide-all-but ("newttt" "newtomtt" 1)) (("2" (grind) nil))))))))))))))))))))))))))))))))))))) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "(nnt!1*nnt!2)" "nnt!1 + nnt!2") (("1" (replace "newtname") (("1" (propax) nil))) ("2" (assert) nil))))))))))))) ("2" (replace "newtname" + rl) (("2" (replace "ttname" + rl) (("2" (hide-all-but (1 2)) (("2" (split 1) (("1" (field) nil) ("2" (field) nil))))))))))))))))) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "nnt!2" "nnt!1 + nnt!2") (("1" (replace "ttname") (("1" (assert) (("1" (replace "ttname" + rl) (("1" (cross-mult 1) (("1" (assert) nil))))))))) ("2" (assert) nil))))))))) ("2" (assert) nil)))))))))) nil) nil nil) (horizontal_conflict_sum_closed-1 nil 3467392723 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (skosimp*) (("" (case "nnt!1 = 0 and nnt!2 = 0") (("1" (flatten) (("1" (inst + "0") (("1" (assert) (("1" (replace -1) (("1" (assert) nil))))))))) ("2" (name "tt" "nnt!2/(nnt!1 + nnt!2)") (("1" (label "ttname" -1) (("1" (case "0<=tt AND tt<=1") (("1" (flatten) (("1" (name "newt" "(nnt!1*nnt!2)/(nnt!1 + nnt!2)") (("1" (label "newtname" -1) (("1" (case "tt*nnt!1 = newt AND (1-tt)*nnt!2 = newt") (("1" (flatten) (("1" (label "newttt" -1) (("1" (label "newtomtt" -2) (("1" (inst + "newt") (("1" (name "VV" "vect2(s) + nnt!1 * vect2(v)") (("1" (label "vvname" -1) (("1" (name "WW" "vect2(s) + nnt!2 * vect2(w)") (("1" (label "wwname" -1) (("1" (name "VVt" "s+nnt!1*v") (("1" (label "vvtname" -1) (("1" (name "WWt" "s+nnt!2*w") (("1" (label "wwtname" -1) (("1" (replace "wwname") (("1" (replace "vvname") (("1" (lemma "horiz_dist_convex_scaf") (("1" (inst - "VVt" "WWt-VVt") (("1" (case "vect2(s) + newt * vect2(v + w) = tt*VV+(1-tt)*WW") (("1" (label "vectfin" -1) (("1" (replace "vectfin") (("1" (assert) (("1" (lemma "convex_wtd_av_lt") (("1" (inst - "0" "LAMBDA (ttt): horiz_dist_scaf(VVt)(ttt, WWt - VVt)" "0" "1") (("1" (assert) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (expand "horiz_dist_scaf" -1 1) (("1" (assert) (("1" (case "vect2(VVt) = VV AND vect2(VVt)+vect2(WWt-VVt) = WW") (("1" (flatten) (("1" (assert) (("1" (inst - "tt") (("1" (assert) (("1" (expand "horiz_dist_scaf") (("1" (case-replace "vect2(VVt) + (1 - tt) * vect2(WWt - VVt) = tt * VV + (1 - tt) * WW") (("1" (assert) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (grind) nil))))))))))))))) ("2" (hide-all-but ("vvtname" "vvname" "wwtname" "wwname" 1)) (("2" (replace "wwtname" + rl) (("2" (replace "vvtname" + rl) (("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_sub") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_add") (("2" (rewrite "vect2_scal") (("2" (rewrite "vect2_scal") (("2" (hide-all-but 1) (("2" (grind) nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (replace "vvname" + rl) (("2" (replace "wwname" + rl) (("2" (assert) (("2" (hide (2 3 4 5)) (("2" (hide-all-but ("newttt" "newtomtt" 1)) (("2" (grind) nil))))))))))))))))))))))))))))))))))))) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "(nnt!1*nnt!2)" "nnt!1 + nnt!2") (("1" (replace "newtname") (("1" (propax) nil))) ("2" (assert) nil))))))))))))) ("2" (replace "newtname" + rl) (("2" (replace "ttname" + rl) (("2" (hide-all-but (1 2)) (("2" (split 1) (("1" (field) nil) ("2" (field) nil))))))))))))))))) ("2" (lemma "nnreal_div_posreal_is_nnreal") (("2" (inst - "nnt!2" "nnt!1 + nnt!2") (("1" (replace "ttname") (("1" (assert) (("1" (replace "ttname" + rl) (("1" (cross-mult 1) (("1" (assert) nil))))))))) ("2" (assert) nil))))))))) ("2" (assert) nil)))))))))) nil) nil nil)) (horizontal_conflict_neg 0 (horizontal_conflict_neg-1 nil 3451899914 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (skeep -1) (("" (inst? 1) (("" (rewrite "sqv_add") (("" (rewrite "sqv_add") (("" (rewrite "sqv_scal") (("" (rewrite "sqv_scal") (("" (rewrite "neg_dot_neg") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict? const-decl "bool" 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) (nnreal type-eq-decl nil real_types nil) (neg_dot_neg formula-decl nil vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (sqv_neg formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (sqv_add formula-decl nil vectors_2D "vectors/")) nil)) (horizontal_conflict_symm 0 (horizontal_conflict_symm-1 nil 3451899566 ("" (skeep) (("" (split) (("1" (flatten) (("1" (lemma "horizontal_conflict_neg") (("1" (inst -1 "s" "v") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "horizontal_conflict_neg") (("2" (inst -1 "-s" "-v") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict_neg formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (neg_neg formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/")) shostak)) (horizontal_conflict_scal 0 (horizontal_conflict_scal-2 nil 3443393415 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (split 1) (("1" (flatten) (("1" (skeep -1) (("1" (inst 1 "nnt/pt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skeep -1) (("2" (rewrite "scal_assoc") (("2" (inst? 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict? const-decl "bool" horizontal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_div_posreal_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) (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) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (scal_assoc formula-decl nil vectors_2D "vectors/")) nil) (horizontal_conflict_scal-1 nil 3443392437 ("" (skeep) (("" (expand "horizontal_conflict?") (("" (skeep -1) (("" (inst 1 "nnt/pk") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (scal_assoc formula-decl nil vectors_2D "vectors/")) nil)) (horizontal_conflict_ever 0 (horizontal_conflict_ever-1 nil 3431265661 ("" (skeep) (("" (expand* "horizontal_conflict_ever?" "horizontal_conflict?") (("" (skeep -1) (("" (inst?) nil nil)) nil)) nil)) nil) ((horizontal_conflict? const-decl "bool" horizontal nil) (horizontal_conflict_ever? const-decl "bool" horizontal nil) (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)) (horizontal_conflict_ever_scal 0 (horizontal_conflict_ever_scal-1 nil 3443389923 ("" (skeep) (("" (expand "horizontal_conflict_ever?") (("" (split 1) (("1" (flatten) (("1" (skeep -1) (("1" (inst 1 "t/nzk") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skeep -1) (("2" (rewrite "scal_assoc") (("2" (inst? 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict_ever? const-decl "bool" horizontal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (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) (nzreal nonempty-type-eq-decl nil reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (scal_assoc formula-decl nil vectors_2D "vectors/")) shostak)) (Delta_zero_eq_0 0 (Delta_zero_eq_0-1 nil 3468062263 ("" (skeep) (("" (expand "Delta") (("" (rewrite "det_zero_right") (("" (assert) nil nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Delta const-decl "real" horizontal nil) (sqv_zero formula-decl nil vectors_2D "vectors/") (sq_0 formula-decl nil sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (det_zero_right formula-decl nil det_2D "vectors/")) shostak)) (Delta_scal 0 (Delta_scal-1 nil 3467395830 ("" (skeep) (("" (expand "Delta") (("" (rewrite "sqv_scal") (("" (rewrite "det_scal_right") (("" (rewrite "sq_times") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Delta const-decl "real" horizontal nil) (det_scal_right formula-decl nil det_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sq_times formula-decl nil sq "reals/") (det const-decl "real" det_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "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) (sqv_scal formula-decl nil vectors_2D "vectors/")) shostak)) (Delta_eq 0 (Delta_eq-1 nil 3451317378 ("" (skeep) (("" (expand "Delta") (("" (rewrite "det_add_left") (("" (rewrite "det_scal_left") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Delta const-decl "real" horizontal nil) (det_scal_left formula-decl nil det_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (det_eq_0 formula-decl nil det_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (det_add_left formula-decl nil det_2D "vectors/")) shostak)) (Delta_symm 0 (Delta_symm-1 nil 3417876952 ("" (skeep) (("" (expand "Delta") (("" (rewrite "det_symm") (("" (rewrite "sqv_neg") nil nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Delta const-decl "real" horizontal nil) (sqv_neg formula-decl nil vectors_2D "vectors/") (neg_neg formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (- const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (det_symm formula-decl nil det_2D "vectors/")) shostak)) (Delta_discr2b 0 (Delta_discr2b-1 nil 3430227627 ("" (skeep) (("" (beta) (("" (expand* "Delta" "discr2b") (("" (rewrite "sq_det") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (sq_det formula-decl nil det_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (Delta const-decl "real" horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (discr2b const-decl "real" quadratic_2b "reals/")) shostak)) (Delta_gt_0_nzv 0 (Delta_gt_0_nzv-1 nil 3431077225 ("" (skeep) (("" (replaces -2) (("" (expand "Delta") (("" (assert) nil nil)) nil)) nil)) nil) ((sqv_zero formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_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) (Delta const-decl "real" horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/")) shostak)) (ground_speed 0 (ground_speed-1 nil 3418048147 ("" (skeep :preds? t) (("" (expand "horizontal_conflict_ever?") (("" (replaces -3) (("" (assert) nil nil)) nil)) nil)) nil) ((horizontal_conflict_ever? const-decl "bool" horizontal nil) (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (Delta_gt_0 0 (Delta_gt_0-2 nil 3420987182 ("" (skeep) (("" (case "v/=zero") (("1" (assert) (("1" (hide -2) (("1" (lemma "Delta_discr2b") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (rewrite "discr2b_discr_gt_0") (("1" (expand "horizontal_conflict_ever?") (("1" (skeep -2) (("1" (lemma "a_gt_0_discr_gt_0") (("1" (inst?) (("1" (inst -1 "t") (("1" (assert) (("1" (rewrite "sqv_add") (("1" (rewrite "sqv_scal") (("1" (assert) (("1" (lemma "v_neq_zero") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "ground_speed") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal 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) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (horizontal_conflict_ever? const-decl "bool" horizontal nil) (a_gt_0_discr_gt_0 formula-decl nil quadratic "reals/") (* const-decl "Vector" vectors_2D "vectors/") (sqv_add formula-decl nil vectors_2D "vectors/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (v_neq_zero formula-decl nil vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "real" 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) (nzreal nonempty-type-eq-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) (discr2b_discr_gt_0 formula-decl nil quadratic_2b "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (Delta_discr2b formula-decl nil horizontal nil) (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) (sq_nz_pos application-judgement "posreal" sq "reals/") (ground_speed formula-decl nil horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil)) nil) (Delta_gt_0-1 nil 3417877237 ("" (skeep) (("" (expand "Delta_gt_0?") (("" (flatten) (("" (expand "Delta") (("" (skolem -1 "T") (("" (lemma "a_gt_0_discr_gt_0") (("" (inst - "sqv(v)" "2*(s*v)" "s*s-sq(D)" "T") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (Delta_gt_0_on_D 0 (Delta_gt_0_on_D-1 nil 3466503266 ("" (skeep) (("" (expand "Delta") (("" (expand "det") (("" (replace -1 + rl) (("" (lemma "cauchy_schwarz") (("" (inst - "s" "perpR(v)") (("" (lemma "sqv_perpR") (("" (inst - "v") (("" (replace -1) (("" (hide -1) (("" (case-replace "s`x * v`y - s`y * v`x = s*perpR(v)") (("1" (hide -1) (("1" (lemma "parallel_dot_1") (("1" (expand "^") (("1" (assert) (("1" (case "not (s = zero or v = zero)") (("1" (flatten) (("1" (inst - "s" "perpR(v)") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst-cp - "1" "norm(s)") (("1" (inst - "1" "norm(perpR(v))") (("1" (expand "abs" -3 2) (("1" (assert) (("1" (expand "abs" -3 2) (("1" (assert) (("1" (case "abs((s * perpR(v))) = norm(s)*norm(perpR(v))") (("1" (assert) (("1" (expand "parallel?") (("1" (skosimp*) (("1" (hide-all-but (-4 3)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "sq(abs((s * perpR(v)))) = sq(norm(s) * norm(perpR(v)))") (("1" (lemma "sq_eq") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "sq_times") (("2" (rewrite "sq_abs") (("2" (assert) (("2" (case "forall (w: Vect2): sq(norm(w)) = sqv(w)") (("1" (inst-cp - "s") (("1" (inst - "perpR(v)") (("1" (replace -1) (("1" (replace -2) (("1" (lemma "sqv_perpR") (("1" (inst - "v") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "sqrt_sqv_norm") (("2" (inst - "w") (("2" (case "sq(sqrt(sqv(w))) = sq(norm(w))") (("1" (lemma "sq_sqrt") (("1" (inst - "sqv(w)") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "norm(perpR(v))") (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) (("2" (hide-all-but (-1 3)) (("2" (expand "perpR") (("2" (expand "zero") (("2" (flatten) (("2" (neg-formula -2) (("2" (grind) (("2" (apply-extensionality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (expand "perpR") (("2" (expand "zero") (("2" (flatten) (("2" (apply-extensionality) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) 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) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Delta const-decl "real" horizontal nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (perpR const-decl "Vect2" perpendicular_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (^ const-decl "Normalized" vectors_2D "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (zero const-decl "Vector" vectors_2D "vectors/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/= const-decl "boolean" notequal nil) (s skolem-const-decl "Vect2" horizontal nil) (v skolem-const-decl "Vect2" horizontal nil) (Nz_vector type-eq-decl nil vectors_2D "vectors/") (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (mult_neg formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (norm_eq_0 formula-decl nil vectors_2D "vectors/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (parallel? const-decl "bool" vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "Vector" vectors_2D "vectors/") (sq_times formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq_eq formula-decl nil sq "reals/") (sq_abs formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (abs_mult formula-decl nil real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (real_le_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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (parallel_dot_1 formula-decl nil parallel_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-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) (real_minus_real_is_real application-judgement "real" reals nil) (sqv_perpR formula-decl nil perpendicular_2D "vectors/") (cauchy_schwarz formula-decl nil vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (Delta_eq_0_dot_on_D 0 (Delta_eq_0_dot_on_D-1 nil 3471094666 ("" (skeep) (("" (expand "Delta") (("" (grind) nil nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Delta const-decl "real" horizontal nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (det const-decl "real" det_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/")) shostak)) (Delta_ge_0 0 (Delta_ge_0-3 nil 3463322733 (";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (skeep) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (lemma "Delta_discr2b") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (inst - "nzv" "s") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (assert) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (replace -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (hide -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (lemma "discr2b_discr") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (inst - "sqv(nzv)" "s * nzv" "sqv(s) - sq(D)") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (replace -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (hide -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (prop) (("1" (mult-by -1 "4") (("1" (assert) (("1" (lemma "solvable_quadratic") (("1" (inst - "sqv(nzv)" "2 * (s * nzv)" "sqv(s) - sq(D)") (("1" (assert) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (hide -2) (("1" (grind) nil))))))))))))))))) ("2" (lemma "discr_ge_0") (("2" (skosimp*) (("2" (inst - "sqv(nzv)" "2 * (s * nzv)" "sqv(s) - sq(D)" "t!1") (("2" (assert) (("2" (hide 2) (("2" (grind) nil)))))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") ((Delta_discr2b formula-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (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) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (nzreal nonempty-type-eq-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) (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (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" horizontal nil) (discr_ge_0 formula-decl nil quadratic "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (discr const-decl "real" quadratic "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (div_cancel2 formula-decl nil real_props nil) (solvable_quadratic formula-decl nil quadratic "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" 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) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (discr2b_discr formula-decl nil quadratic_2b "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil) (Delta_ge_0-2 nil 3463322706 (";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (skeep) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (lemma "Delta_discr2b") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (inst - "v" "s") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (assert) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (replace -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (hide -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (lemma "discr2b_discr") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (inst - "sqv(v)" "s * v" "sqv(s) - sq(D)") ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (replace -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (hide -1) ((";;; Proof Delta_ge_0-1 for formula horizontal.Delta_ge_0" (prop) (("1" (mult-by -1 "4") (("1" (assert) (("1" (lemma "solvable_quadratic") (("1" (inst - "sqv(v)" "2 * (s * v)" "sqv(s) - sq(D)") (("1" (assert) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (hide -2) (("1" (grind) nil))))))))))))))))) ("2" (lemma "discr_ge_0") (("2" (skosimp*) (("2" (inst - "sqv(v)" "2 * (s * v)" "sqv(s) - sq(D)" "t!1") (("2" (assert) (("2" (hide 2) (("2" (grind) nil)))))))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil) (Delta_ge_0-1 nil 3463319539 ("" (skeep) (("" (lemma "Delta_discr2b") (("" (inst - "nzv" "s") (("" (assert) (("" (replace -1) (("" (hide -1) (("" (lemma "discr2b_discr") (("" (inst - "sqv(nzv)" "s * nzv" "sqv(s) - sq(D)") (("" (replace -1) (("" (hide -1) (("" (prop) (("1" (mult-by -1 "4") (("1" (assert) (("1" (lemma "solvable_quadratic") (("1" (inst - "sqv(nzv)" "2 * (s * nzv)" "sqv(s) - sq(D)") (("1" (assert) (("1" (skosimp*) (("1" (inst + "x!1") (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "discr_ge_0") (("2" (skosimp*) (("2" (inst - "sqv(nzv)" "2 * (s * nzv)" "sqv(s) - sq(D)" "t!1") (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (discr_ge_0 formula-decl nil quadratic "reals/") (discr const-decl "real" quadratic "reals/") (solvable_quadratic formula-decl nil quadratic "reals/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (discr2b_discr formula-decl nil quadratic_2b "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/")) shostak)) (Delta_ge_0_2 0 (Delta_ge_0_2-1 nil 3463322277 ("" (skeep) (("" (prop) (("1" (lemma "Delta_ge_0") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst + "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "sqv(s + t!1*nzv) < sq(D)") (("1" (lemma "Delta_gt_0") (("1" (inst?) (("1" (assert) (("1" (expand "horizontal_conflict_ever?") (("1" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "Delta_ge_0") (("2" (inst?) (("2" (assert) (("2" (inst + "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Delta_ge_0 formula-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal 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/") (+ 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) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (horizontal_conflict_ever? const-decl "bool" horizontal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Delta_gt_0 formula-decl nil horizontal nil)) shostak)) (Delta_eq_0_eq_tca 0 (Delta_eq_0_eq_tca-1 nil 3571393692 ("" (skeep) (("" (label "onDs" -2) (("" (lemma "Delta_gt_0") (("" (inst - "s" "nzv") (("" (assert) (("" (expand "horizontal_conflict_ever?") (("" (case "t = horizontal_tca(s,nzv)") (("1" (assert) (("1" (replaces -1) (("1" (hide-all-but 2) (("1" (grind) (("1" (field) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (name "tca2" "horizontal_tca(s,nzv)") (("2" (inst + "tca2") (("2" (assert) (("2" (name "aa" "sqv(nzv)") (("2" (name "bb" "2*(s*nzv)") (("2" (name "cc" "sqv(s)") (("2" (name "ff" "quadratic(aa,bb,cc)") (("2" (lemma "quad_min_mono_inc") (("2" (lemma "sqv_eq_0") (("2" (inst - "nzv") (("2" (flatten) (("2" (hide -2) (("2" (split -) (("1" (assert) nil nil) ("2" (case "NOT aa > 0") (("1" (assert) nil nil) ("2" (assert) (("2" (inst - "aa" "bb" "cc" "t" "tca2") (("2" (case "tca2 = -bb/(2*aa)") (("1" (assert) (("1" (replace -1 :dir rl) (("1" (assert) (("1" (lemma "quad_min_mono_dec") (("1" (inst - "aa" "bb" "cc" "t" "tca2") (("1" (assert) (("1" (replace -2 :dir rl) (("1" (assert) (("1" (case "ff(t) = sq(D)") (("1" (ground) (("1" (hide-all-but (-1 -2 -3 +)) (("1" (hide 2) (("1" (expand "ff") (("1" (expand "aa") (("1" (expand "bb") (("1" (expand "cc") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -3 +)) (("2" (hide -3) (("2" (expand "ff") (("2" (hide 3) (("2" (expand "aa") (("2" (expand "bb") (("2" (expand "cc") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "aa") (("3" (expand "bb") (("3" (hide-all-but (-1 -2 +)) (("3" (hide 3) (("3" (expand "ff") (("3" (expand "aa") (("3" (expand "bb") (("3" (expand "cc") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but ("onDs" 1)) (("2" (expand "ff") (("2" (expand "aa") (("2" (expand "bb") (("2" (expand "cc") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (expand "tca2" 1) (("2" (expand "horizontal_tca" 1) (("2" (cross-mult 1) 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 nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (horizontal_conflict_ever? const-decl "bool" horizontal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (quadratic const-decl "real" quadratic "reals/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (quad_min_mono_dec formula-decl nil quad_minmax "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (aa skolem-const-decl "posreal" horizontal nil) (cc skolem-const-decl "nnreal" horizontal nil) (bb skolem-const-decl "real" horizontal nil) (ff skolem-const-decl "[real -> real]" horizontal nil) (D formal-const-decl "posreal" horizontal nil) (sq const-decl "nonneg_real" sq "reals/") (tca2 skolem-const-decl "real" horizontal nil) (times_div1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (div_cancel4 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (quad_min_mono_inc formula-decl nil quad_minmax "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) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (real_minus_real_is_real application-judgement "real" reals nil) (zero_times1 formula-decl nil real_props nil) (both_sides_times1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (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) (real_div_nzreal_is_real application-judgement "real" reals nil) (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (horizontal_tca const-decl "real" definitions nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Delta_gt_0 formula-decl nil horizontal nil)) shostak)) (sdotv_lt_0 0 (sdotv_lt_0-1 nil 3429963031 ("" (skeep :preds? t) (("" (lemma "horizontal_conflict_ever") (("" (inst? -1) (("" (assert) (("" (lemma "Delta_gt_0") (("" (inst?) (("" (assert) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) (("" (lemma "Delta_discr2b") (("" (inst?) (("" (beta) (("" (replaces -1) (("" (rewrite "discr2b_discr_gt_0") (("" (expand "horizontal_conflict?") (("" (skeep -5) (("" (rewrite "sqv_add") (("" (rewrite "sqv_scal") (("" (name-replace "a" "sqv(v)") (("" (name-replace "b" "sp*v") (("" (lemma "quadratic_lt_0") (("" (inst?) (("" (inst -1 "nnt") (("" (assert) (("" (flatten) (("" (hide -7) (("" (move-terms -6 r 1) (("" (name-replace "c" "sqv(sp) - sq(D)") (("" (case "b=0") (("1" (lemma "roots_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "root_gt_0") (("2" (inst -1 "a" "2*b" "c" "1") (("2" (assert) (("2" (rewrite "sign_eq_1") (("2" (case "c=0") (("1" (assert) (("1" (mult-by 3 "2*a") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "a * c > 0") (("1" (assert) (("1" (mult-by -3 "2*b") (("1" (assert) nil nil)) nil)) nil) ("2" (mult-cases 1) 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) ((horizontal_conflict_ever formula-decl nil horizontal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Delta_gt_0_nzv formula-decl nil horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (horizontal_conflict? const-decl "bool" horizontal nil) (* const-decl "Vector" vectors_2D "vectors/") (sqv_add formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot_scal_canon formula-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (quadratic_lt_0 formula-decl nil quadratic "reals/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (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) (roots_eq_0 formula-decl nil quadratic "reals/") (sign_eq_1 formula-decl nil sign "reals/") (pos_times_gt formula-decl nil real_props nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (root_gt_0 formula-decl nil quadratic "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqv_scal formula-decl nil vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (discr2b_discr_gt_0 formula-decl nil quadratic_2b "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (* const-decl "real" vectors_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (Delta_discr2b formula-decl nil horizontal nil) (Delta_gt_0 formula-decl nil horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal 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) (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 "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_TCC1 0 (Theta_D_TCC1-1 nil 3431346983 ("" (skosimp* :preds? t) (("" (lemma "Delta_discr2b") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((Delta_discr2b formula-decl nil horizontal nil) (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) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (>= const-decl "bool" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Delta const-decl "real" horizontal 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)) nil)) (Theta_D_on_D 0 (Theta_D_on_D-2 nil 3565275422 ("" (skeep) (("" (skoletin 1 :postfix "t") (("" (expand "Theta_D") (("" (rewrite "sqv_add") (("" (rewrite "sqv_scal") (("" (move-terms 1 l 2) (("" (lemma "Delta_discr2b") (("" (inst?) (("" (skoletin* -1 :old? t) (("" (replaces -2) (("" (lemma "quad2b_eq_0") (("" (inst?) (("" (inst -1 "tt") (("" (expand "quadratic") (("" (assert) (("" (assert) (("" (inst 1 "eps") (("" (assert) 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/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "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) (>= const-decl "bool" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Delta const-decl "real" horizontal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (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" horizontal nil) (sqv_add formula-decl nil vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot_scal_canon formula-decl nil vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic "reals/") (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (Delta_discr2b formula-decl nil horizontal nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/")) nil) (Theta_D_on_D-1 nil 3471112100 ("" (skeep) (("" (skoletin 1 :postfix "t") (("" (expand "Theta_D") (("" (rewrite "sqv_add") (("" (rewrite "sqv_scal") (("" (move-terms 1 l 2) (("" (lemma "Delta_discr2b") (("" (inst?) (("" (skoletin* -1) (("" (replaces -2) (("" (lemma "quad2b_eq_0") (("" (inst?) (("" (inst -1 "tt") (("" (expand "quadratic") (("" (assert) (("" (inst 1 "eps") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Sign type-eq-decl nil sign "reals/") (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 type-eq-decl nil vectors_2D_def "vectors/") (sq const-decl "nonneg_real" sq "reals/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv_add formula-decl nil vectors_2D "vectors/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (quadratic const-decl "real" quadratic "reals/") (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/")) nil)) (Theta_D_unique_eps 0 (Theta_D_unique_eps-1 nil 3463581075 ("" (skeep) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (assert) (("" (lemma "quad2b_eq_0") (("" (inst?) (("" (expand "quadratic") (("" (rewrite "sqv_add") (("" (rewrite "sqv_scal") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (quad2b_eq_0 formula-decl nil quadratic_2b "reals/") (real_times_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (quadratic const-decl "real" quadratic "reals/") (sqv_scal formula-decl nil vectors_2D "vectors/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (sqv_add formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "real" 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) (nzreal nonempty-type-eq-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) (real_minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Delta_discr2b formula-decl nil horizontal nil)) nil)) (Theta_D_unique 0 (Theta_D_unique-1 nil 3463314173 ("" (skeep) (("" (lemma "Theta_D_unique_eps") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (ground) (("1" (skeep -1 :preds? t) (("1" (ground) nil nil)) nil) ("2" (inst? 1) nil nil) ("3" (inst? 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Theta_D_unique_eps formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (bool nonempty-type-eq-decl nil booleans 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_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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_symm_TCC1 0 (Theta_D_symm_TCC1-1 nil 3431347102 ("" (skeep) (("" (rewrite "Delta_symm") nil nil)) nil) ((Delta_symm formula-decl nil horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")) nil)) (Theta_D_symm 0 (Theta_D_symm-1 nil 3431347102 ("" (skeep) (("" (expand "Theta_D") (("" (rewrite "neg_dot_neg") (("" (rewrite "sqv_neg") (("" (rewrite "sqv_neg") nil nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (sqv_neg formula-decl nil vectors_2D "vectors/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (neg_dot_neg formula-decl nil vectors_2D "vectors/")) nil)) (Theta_D_scal_TCC1 0 (Theta_D_scal_TCC1-1 nil 3467396128 ("" (skeep) (("" (lemma "Delta_scal") (("" (inst - "s" "nzk" "nzv") (("" (lemma nnreal_times_nnreal_is_nnreal) (("" (inst - "sq(nzk)" "Delta(s,nzv)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Delta_scal formula-decl nil horizontal nil) (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Delta const-decl "real" horizontal nil) (s skolem-const-decl "Vect2" horizontal nil) (nzv skolem-const-decl "Nz_vect2" horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_scal 0 (Theta_D_scal-1 nil 3467396128 ("" (skeep) (("" (expand "Theta_D") (("" (expand "root2b") (("" (expand "discr2b") (("" (lemma "dot_comm") (("" (label "dc" -1) (("" (inst-cp -1 "s" "nzk*nzv") (("" (replace -2) (("" (label "cdlem" -1) (("" (lemma "sq_times") (("" (label "sqt" -1) (("" (inst-cp -1 "nzk" "nzv*s") (("" (label "sqtlem" -1) (("" (inst "cdlem" "s" "nzv") (("" (lemma "dot_assoc") (("" (label "assoc" -1) (("" (inst - "nzk" "nzv" "s") (("" (replace -1 + rl) (("" (replace "sqt") (("" (replace "cdlem" + rl) (("" (rewrite "sqv_scal") (("" (case-replace "sq(nzk) * sq(s * nzv) + sq(D) * (sq(nzk) * sqv(nzv)) - sq(nzk) * sqv(nzv) * sqv(s) = sq(nzk)*(sq(s*nzv)+sq(D)*sqv(nzv)-sqv(nzv)*sqv(s))") (("1" (lemma "sqrt_times") (("1" (inst - "sq(nzk)" "sq(s*nzv)+sq(D)*sqv(nzv)-sqv(nzv)*sqv(s)") (("1" (replace -1) (("1" (case "forall (x: nzreal): sqrt(sq(x)) = sign(x)*x") (("1" (label "sqrtlem" -1) (("1" (inst - "nzk") (("1" (replace -1) (("1" (hide-all-but 1) (("1" (cross-mult 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (expand "sign") (("2" (lift-if) (("2" (lemma "sqrt_sq") (("2" (split) (("1" (flatten) (("1" (inst - "x") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst - "-x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "Delta_discr2b") (("2" (inst?) (("2" (assert) (("2" (expand "discr2b") (("2" (assert) 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)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (discr2b const-decl "real" quadratic_2b "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sq_times formula-decl nil sq "reals/") (* const-decl "real" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" horizontal 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 "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (s skolem-const-decl "Vect2" horizontal nil) (nzv skolem-const-decl "Nz_vect2" horizontal nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (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 "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (sign const-decl "Sign" sign "reals/") (div_cancel4 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div1 formula-decl nil real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_sq_neg formula-decl nil sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (Delta_discr2b formula-decl nil horizontal nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (sqrt_times formula-decl nil sqrt "reals/") (sqv_scal formula-decl nil vectors_2D "vectors/") (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (dot_assoc formula-decl nil vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (* const-decl "Vector" vectors_2D "vectors/") (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (dot_comm formula-decl nil vectors_2D "vectors/") (root2b const-decl "real" quadratic_2b "reals/") (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (Theta_D_neg_nzv_TCC1 0 (Theta_D_neg_nzv_TCC1-1 nil 3466420967 ("" (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) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (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) (- const-decl "Vector" vectors_2D "vectors/") (real_times_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) (minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (Theta_D_neg_nzv 0 (Theta_D_neg_nzv-1 nil 3466420967 ("" (skeep) (("" (expand "Theta_D") (("" (expand "root2b") (("" (expand "discr2b") (("" (lemma "sqv_neg") (("" (inst - "nzv") (("" (replace -1) (("" (hide -1) (("" (case-replace "sq(s* -nzv) = sq(s*nzv)") (("1" (case-replace "-(s* -nzv) = s*nzv") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (discr2b const-decl "real" quadratic_2b "reals/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (sq const-decl "nonneg_real" sq "reals/") (* const-decl "real" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (real_div_nzreal_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/") (root2b const-decl "real" quadratic_2b "reals/") (sign_neg_clos application-judgement "Sign" sign "reals/")) shostak)) (Theta_D_le 0 (Theta_D_le-1 nil 3431347163 ("" (skeep) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (rewrite "root2b_root") (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "root_le") (("" (inst?) (("" (assert) (("" (rewrite "sign_eq_1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (root_le formula-decl nil quadratic "reals/") (sign_eq_1 formula-decl nil sign "reals/") (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (real_times_real_is_real application-judgement "real" reals nil) (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) (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "real" 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) (nzreal nonempty-type-eq-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) (root2b_root formula-decl nil quadratic_2b "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Delta_discr2b formula-decl nil horizontal nil)) nil)) (Theta_D_lt_TCC1 0 (Theta_D_lt_TCC1-1 nil 3431347262 ("" (skeep) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((Delta_gt_0_nzv formula-decl nil horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_lt 0 (Theta_D_lt-1 nil 3431347262 ("" (skeep) (("" (expand "Theta_D") (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) (("" (lemma "Delta_discr2b") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (rewrite "root2b_root") (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_gt_0") (("" (lemma "root_lt") (("" (inst?) (("" (assert) (("" (rewrite "sign_eq_1") 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/") (Theta_D const-decl "real" horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (Delta_discr2b formula-decl nil horizontal nil) (root2b_root formula-decl nil quadratic_2b "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) (nzreal nonempty-type-eq-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) (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (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" horizontal 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/") (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (discr2b_discr_gt_0 formula-decl nil quadratic_2b "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (sign_eq_1 formula-decl nil sign "reals/") (root_lt formula-decl nil quadratic "reals/") (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Delta_gt_0_nzv formula-decl nil horizontal nil)) nil)) (Theta_D_Delta_eq_0 0 (Theta_D_Delta_eq_0-1 nil 3463397993 ("" (skeep) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (rewrite "root2b_root") (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_eq_0") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "root_eq") (("" (inst?) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (root_eq formula-decl nil quadratic "reals/") (discr2b_discr_eq_0 formula-decl nil quadratic_2b "reals/") (real_times_real_is_real application-judgement "real" reals nil) (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) (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "real" 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) (nzreal nonempty-type-eq-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) (root2b_root formula-decl nil quadratic_2b "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Delta_discr2b formula-decl nil horizontal nil)) nil)) (Theta_D_eq_0 0 (Theta_D_eq_0-1 nil 3431351490 ("" (skeep) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (assert) (("" (replaces -1) (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "root_eq_0") (("" (inst?) (("" (assert) (("" (rewrite "sign_eq_neg1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (sign_nat formula-decl nil sign "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) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (sign_eq_neg1 formula-decl nil sign "reals/") (root_eq_0 formula-decl nil quadratic "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) (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "real" 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) (nzreal nonempty-type-eq-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) (root2b_root formula-decl nil quadratic_2b "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Delta_discr2b formula-decl nil horizontal nil)) nil)) (Theta_D_ge_0 0 (Theta_D_ge_0-2 nil 3565277314 ("" (skeep :preds? t) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (skoletin* -1 :old? t) (("" (replaces -2) (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "roots_ge_0") (("" (inst -1 "a" "2*b" "c" "-1") (("" (assert) (("" (real-props 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (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) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_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" horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (pos_times_ge formula-decl nil real_props nil) (neg_times_le formula-decl nil real_props nil) (pos_times_le formula-decl nil real_props nil) (roots_ge_0 formula-decl nil quadratic "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (root2b_root formula-decl nil quadratic_2b "reals/") (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 "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (Delta const-decl "real" horizontal nil) (nzreal nonempty-type-eq-decl nil reals nil) (discr2b const-decl "real" quadratic_2b "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (Delta_discr2b formula-decl nil horizontal nil)) nil) (Theta_D_ge_0-1 nil 3431352792 ("" (skeep :preds? t) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (skoletin* -1) (("" (replaces -2) (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "roots_ge_0") (("" (inst -1 "a" "2*b" "c" "-1") (("" (assert) (("" (real-props 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (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/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (roots_ge_0 formula-decl nil quadratic "reals/") (Sign type-eq-decl nil sign "reals/") (root2b_root formula-decl nil quadratic_2b "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (* const-decl "real" vectors_2D "vectors/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")) nil)) (Theta_D_neq_0 0 (Theta_D_neq_0-2 nil 3565277334 ("" (skeep :preds? t) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (skoletin* -1 :old? t) (("" (replaces -2) (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "root_neq_0") (("" (inst -1 "a" "2*b" "c" "eps") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "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" horizontal nil) (Ss_vect2 type-eq-decl nil horizontal nil) (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (root_neq_0 formula-decl nil quadratic "reals/") (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) (real_times_real_is_real application-judgement "real" reals nil) (root2b_root formula-decl nil quadratic_2b "reals/") (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 "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (* const-decl "real" vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (discr2b const-decl "real" quadratic_2b "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (Delta const-decl "real" horizontal nil) (real_minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (Delta_discr2b formula-decl nil horizontal nil)) nil) (Theta_D_neq_0-1 nil 3432553520 ("" (skeep :preds? t) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("" (skoletin* -1) (("" (replaces -2) (("" (rewrite "root2b_root") (("" (rewrite "discr2b_discr_ge_0") (("" (lemma "root_neq_0") (("" (inst -1 "a" "2*b" "c" "eps") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_nz_pos application-judgement "posreal" sq "reals/") (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/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (discr2b_discr_ge_0 formula-decl nil quadratic_2b "reals/") (root_neq_0 formula-decl nil quadratic "reals/") (Sign type-eq-decl nil sign "reals/") (root2b_root formula-decl nil quadratic_2b "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (* const-decl "real" vectors_2D "vectors/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")) nil)) (horizontal_conflict 0 (horizontal_conflict-1 nil 3431450389 ("" (skeep) (("" (split) (("1" (flatten) (("1" (lemma "horizontal_conflict_ever") (("1" (inst?) (("1" (assert) (("1" (lemma "Delta_gt_0") (("1" (inst?) (("1" (assert) (("1" (lemma "sdotv_lt_0 ") (("1" (inst?) (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "horizontal_conflict?") (("2" (split -2) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil) ("2" (name "tt1" "Theta_D(s,nzv,-1)") (("1" (case "tt1 >= 0") (("1" (name "tt2" "Theta_D(s,nzv,1)") (("1" (lemma "Theta_D_on_D") (("1" (inst-cp -1 "1" "nzv" "s") (("1" (assert) (("1" (inst -1 "-1" "nzv" "s") (("1" (assert) (("1" (lemma "Theta_D_lt") (("1" (inst?) (("1" (assert) (("1" (lemma "t1_lt_t2_lt_D") (("1" (inst -1 "s" "nzv" _ "tt1" "tt2" "sq(D)") (("1" (assert) (("1" (inst -1 "(tt1+tt2)/2") (("1" (assert) (("1" (inst? 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "0") (("2" (lemma "Theta_D_ge_0") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict_ever formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sdotv_lt_0 formula-decl nil horizontal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Sp_vect2 type-eq-decl nil horizontal 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (s skolem-const-decl "Vect2" horizontal nil) (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" horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (Delta_gt_0 formula-decl nil horizontal nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (horizontal_conflict? const-decl "bool" horizontal nil) (Theta_D const-decl "real" horizontal nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (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) (Delta const-decl "real" horizontal nil) (= const-decl "[T, T -> boolean]" equalities nil) (Theta_D_ge_0 formula-decl nil horizontal nil) (Theta_D_lt formula-decl nil horizontal nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (t1_lt_t2_lt_D formula-decl nil closest_approach_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (Theta_D_on_D formula-decl nil horizontal nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/")) nil)) (horizontal_conflict_on_D 0 (horizontal_conflict_on_D-1 nil 3469977604 ("" (skeep) (("" (case "v /= zero") (("1" (flatten) (("1" (lemma "horizontal_conflict") (("1" (inst - "v" "s") (("1" (replace -1) (("1" (hide -1) (("1" (ground) (("1" (expand "Delta") (("1" (case "s*v /= 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (flatten) (("2" (hide -2) (("2" (lemma "parallel_det_0") (("2" (inst - "s" "perpR(v)") (("1" (case "det(s,perpR(v)) = 0") (("1" (assert) (("1" (hide -1) (("1" (expand "parallel?") (("1" (skosimp*) (("1" (replace -1 -) (("1" (hide-all-but (-3 -4)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (flatten) (("2" (expand "zero") (("2" (expand "perpR") (("2" (flatten) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replace -1) (("3" (expand "sqv") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Delta") (("2" (case "sq(D) * sqv(v) - sq(det(s, v)) >= 0") (("1" (assert) (("1" (case "sq(D) * sqv(v) - sq(det(s, v)) /= 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -1) (("2" (flatten) (("2" (lemma "parallel_dot_1") (("2" (inst - "s" "perpR(v)") (("1" (ground) (("1" (expand "parallel?") (("1" (skosimp*) (("1" (replace -1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "det_perpR") (("2" (expand "^") (("2" (lemma "sq_eq") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (cross-mult 1) (("1" (lemma "sq_norm") (("1" (inst-cp - "perpR(v)") (("1" (inst - "s") (("1" (replace -1) (("1" (hide -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sqv_perpR") (("1" (assert) 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) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) (("2" (hide-all-but (-1 3)) (("2" (expand "zero") (("2" (expand "perpR") (("2" (flatten) (("2" (decompose-equality) nil nil)) 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 1)) (("2" (expand "zero") (("2" (expand "perpR") (("2" (flatten) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replace -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -2 + rl) (("2" (lemma "cauchy_schwarz") (("2" (inst - "s" "perpR(v)") (("2" (rewrite "det_perpR") (("2" (rewrite "sqv_perpR") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "horizontal_conflict?") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal 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) (horizontal_conflict formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers 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/") (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) (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) (* const-decl "real" vectors_2D "vectors/") (parallel_det_0 formula-decl nil parallel_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (dot_zero_left formula-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (det const-decl "real" det_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (* const-decl "Vector" vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (parallel? const-decl "bool" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Nz_vector type-eq-decl nil vectors_2D "vectors/") (perpR const-decl "Vect2" perpendicular_2D "vectors/") (s skolem-const-decl "Vect2" horizontal nil) (Delta const-decl "real" horizontal nil) (nnreal type-eq-decl nil real_types nil) (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (parallel_dot_1 formula-decl nil parallel_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (^ const-decl "Normalized" vectors_2D "vectors/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (det_perpR formula-decl nil det_2D "vectors/") (sq_eq formula-decl nil sq "reals/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (sq_abs formula-decl nil sq "reals/") (sq_1 formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (sq_div formula-decl nil sq "reals/") (norm_eq_0 formula-decl nil vectors_2D "vectors/") (norm_zero formula-decl nil vectors_2D "vectors/") (sq_0 formula-decl nil sq "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (times_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel3 formula-decl nil real_props nil) (sqv_perpR formula-decl nil perpendicular_2D "vectors/") (sq_norm formula-decl nil vectors_2D "vectors/") (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (cauchy_schwarz formula-decl nil 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/") (v skolem-const-decl "Vect2" horizontal nil) (horizontal_conflict? const-decl "bool" horizontal nil) (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/")) shostak)) (horizontal_entry_le 0 (horizontal_entry_le-1 nil 3445266437 ("" (skeep) (("" (case-replace "v=zero") (("1" (assert) nil nil) ("2" (lemma "sqv_eq_0") (("2" (inst -1 "v") (("2" (assert) (("2" (rewrite "sqv_add") (("2" (rewrite "sqv_add") (("2" (rewrite "sqv_scal") (("2" (rewrite "sqv_scal") (("2" (lemma "quad_min_mono_dec") (("2" (inst -1 "sqv(v)" "2*(s*v)" "-sq(D)" "t1" "t2") (("2" (assert) (("2" (expand "quadratic") (("2" (cross-mult 1) (("2" (rewrite "dot_add_left") (("2" (rewrite "sqv" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (sqv_add formula-decl nil vectors_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot_scal_canon formula-decl nil vectors_2D "vectors/") (sqv_scal formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (quad_min_mono_dec formula-decl nil quad_minmax "reals/") (real_gt_is_strict_total_order name-judgement "(strict_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) (div_mult_pos_le2 formula-decl nil real_props nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_add_left formula-decl nil vectors_2D "vectors/") (quadratic const-decl "real" quadratic "reals/") (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-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) (sqv const-decl "nnreal" vectors_2D "vectors/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (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" horizontal nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/")) shostak)) (not_horizontal_entry_lt 0 (not_horizontal_entry_lt-1 nil 3445271454 ("" (skeep) (("" (expand "horizontal_tca") (("" (name-replace "tt1" "max(0,-(s*nzv)/sqv(nzv))" :hide? nil) (("" (flatten) (("" (case "tt1 < t2") (("1" (assert) (("1" (lemma "quad_min_mono_inc") (("1" (inst -1 "sqv(nzv)" "2*(s*nzv)" "-sq(D)" "t2" "tt1") (("1" (assert) (("1" (expand "quadratic") (("1" (rewrite "sqv_add") (("1" (rewrite "sqv_add") (("1" (rewrite "sqv_scal") (("1" (rewrite "sqv_scal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (replaces -1 :dir rl) (("2" (rewrite "max_lt") (("2" (assert) (("2" (cross-mult 1) (("2" (rewrite "dot_add_left") (("2" (rewrite "sqv" :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (horizontal_tca const-decl "real" definitions nil) (max_lt formula-decl nil real_defs nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_add_left formula-decl nil vectors_2D "vectors/") (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/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (D formal-const-decl "posreal" horizontal 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 "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (quadratic const-decl "real" quadratic "reals/") (sqv_scal formula-decl nil vectors_2D "vectors/") (dot_scal_canon formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_add formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (quad_min_mono_inc formula-decl nil quad_minmax "reals/") (< const-decl "bool" reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "real" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (/ 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (horizontal_los_inside_Theta 0 (horizontal_los_inside_Theta-1 nil 3448810543 ("" (skeep) (("" (lemma "Theta_D_on_D") (("" (inst -1 "-1" "nzv" "s") (("" (assert) (("" (lemma "Theta_D_on_D") (("" (inst -1 "1" "nzv" "s") (("" (assert) (("" (split) (("1" (flatten) (("1" (lemma "t1_lt_t2_lt_D") (("1" (inst?) (("1" (inst -1 "Theta_D(s,nzv,-1)" "Theta_D(s,nzv,1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "lt_D_t1_lt_t2") (("2" (inst -1 "s" "nzv" "t" "Theta_D(s,nzv,-1)" "Theta_D(s,nzv,1)" "sq(D)") (("2" (assert) (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide -2 -3 2) (("2" (lemma "Theta_D_lt") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "Delta_gt_0") (("2" (inst?) (("2" (assert) (("2" (expand "horizontal_conflict_ever?") (("2" (inst? 1) 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) ((Theta_D_on_D formula-decl nil horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (t1_lt_t2_lt_D formula-decl nil closest_approach_2D "vectors/") (Theta_D const-decl "real" horizontal nil) (Delta const-decl "real" horizontal nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (>= const-decl "bool" reals nil) (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" horizontal nil) (lt_D_t1_lt_t2 formula-decl nil closest_approach_2D "vectors/") (Theta_D_lt formula-decl nil horizontal nil) (Delta_gt_0 formula-decl nil horizontal nil) (horizontal_conflict_ever? const-decl "bool" horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "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) (bool nonempty-type-eq-decl nil booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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 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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (horizontal_sep_outside_Theta 0 (horizontal_sep_outside_Theta-1 nil 3463397290 ("" (skosimp*) (("" (case "Delta(s!1,nzv!1) = 0") (("1" (lemma "Theta_D_Delta_eq_0") (("1" (inst?) (("1" (assert) (("1" (lemma "horizontal_los_inside_Theta") (("1" (inst - "nzv!1" "s!1" "t!1") (("1" (assert) (("1" (lemma "Theta_D_unique") (("1" (inst - "nzv!1" "s!1" "t!1") (("1" (assert) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "horizontal_los_inside_Theta") (("2" (inst - "nzv!1" "s!1" "t!1") (("2" (lemma "Theta_D_unique") (("2" (inst - "nzv!1" "s!1" "t!1") (("2" (lemma "Theta_D_lt") (("2" (inst - "s!1" "nzv!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (Delta const-decl "real" horizontal 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) (horizontal_los_inside_Theta formula-decl nil horizontal nil) (Theta_D_unique formula-decl nil horizontal 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D_Delta_eq_0 formula-decl nil horizontal nil) (Theta_D_lt formula-decl nil horizontal nil)) nil)) (not_horiz_sep_inside_closed_Theta 0 (not_horiz_sep_inside_closed_Theta-1 nil 3466352902 ("" (skeep) (("" (lemma "horizontal_los_inside_Theta") (("" (inst?) (("" (assert) (("" (lemma "Theta_D_unique") (("" (inst?) (("" (assert) (("" (lemma "horizontal_sep_outside_Theta") (("" (inst?) (("" (assert) (("" (name-replace "AA" "Theta_D(s,nzv,-1)") (("" (name-replace "BB" "Theta_D(s,nzv,1)") (("" (name-replace "CC" "sqv(s+t*nzv)") (("" (name-replace "SQD" "sq(D)") (("" (hide -4) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_los_inside_Theta formula-decl nil horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (horizontal_sep_outside_Theta formula-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal 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) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (Theta_D const-decl "real" horizontal nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (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) (Delta const-decl "real" horizontal nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_D_unique formula-decl nil horizontal 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_entry_gt_0_TCC1 0 (Theta_D_entry_gt_0_TCC1-1 nil 3460765023 ("" (skeep) (("" (rewrite "horizontal_conflict") (("" (assert) nil nil)) nil)) nil) ((horizontal_conflict formula-decl nil horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "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" horizontal nil) (Ss_vect2 type-eq-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers 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/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (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)) nil)) (Theta_D_entry_gt_0 0 (Theta_D_entry_gt_0-1 nil 3460765023 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma "Theta_D_neq_0") (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma "Theta_D_ge_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict formula-decl nil horizontal 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/") (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_D_neq_0 formula-decl nil horizontal nil) (Theta_D_ge_0 formula-decl nil horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (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) (Ss_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal nil) (posreal nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_exit_gt_0 0 (Theta_D_exit_gt_0-4 nil 3460763196 ("" (skeep) (("" (use "Delta_gt_0_nzv") (("" (assert) (("" (flatten) (("" (case "sqv(v) > 0") (("1" (split) (("1" (flatten) (("1" (lemma "horizontal_conflict") (("1" (inst?) (("1" (assert) (("1" (replaces -1 :dir rl) (("1" (expand "horizontal_conflict?") (("1" (skeep -1) (("1" (lemma "horizontal_los_inside_Theta") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "Theta_D") (("2" (lemma "Delta_discr2b") (("2" (inst?) (("2" (beta) (("2" (expand "root2b") (("2" (replaces -1) (("2" (cross-mult -1) (("2" (real-props) (("2" (move-terms -1 l 2) (("2" (real-props) (("2" (lemma "sqrt_gt") (("2" (inst -1 "discr2b(sqv(v), s * v, sqv(s) - sq(D))" "sq(s*v)") (("2" (assert) (("2" (hide (-2 -4)) (("2" (expand "discr2b") (("2" (move-terms -1 l 1) (("2" (assert) (("2" (mult-by 1 "sqv(v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Delta_gt_0_nzv formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (horizontal_conflict formula-decl nil horizontal nil) (horizontal_conflict? const-decl "bool" horizontal nil) (horizontal_los_inside_Theta formula-decl nil horizontal nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Theta_D const-decl "real" horizontal nil) (root2b const-decl "real" quadratic_2b "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (D formal-const-decl "posreal" horizontal nil) (posreal nonempty-type-eq-decl nil real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (s skolem-const-decl "Vect2" horizontal nil) (* const-decl "real" vectors_2D "vectors/") (discr2b const-decl "real" quadratic_2b "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (v skolem-const-decl "Vect2" horizontal nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (sqrt_gt formula-decl nil sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (< const-decl "bool" reals nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (zero_times1 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (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) (Delta_discr2b 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) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil) (Theta_D_exit_gt_0-3 nil 3460762752 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (hide -2) (("" (expand "horizontal_conflict?") (("" (skeep -2) (("" (lemma "horizontal_los_inside_Theta") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (sq_nz_pos application-judgement "posreal" sq "reals/")) nil) (Theta_D_exit_gt_0-2 nil 3460762595 (";;; Proof Delta_gt_0_Theta_D_exit_gt_0-1 for formula horizontal.Delta_gt_0_Theta_D_ (skeep) ((";;; Proof Delta_gt_0_Theta_D_exit_gt_0-1 for formula horizontal.Delta_gt_0_Theta_D (use "Delta_gt_0_nzv") ((";;; Proof Delta_gt_0_Theta_D_exit_gt_0-1 for formula horizontal.Delta_gt_0_Theta_D (assert) ((";;; Proof Delta_gt_0_Theta_D_exit_gt_0-1 for formula horizontal.Delta_gt_0_Theta_D (flatten) ((";;; Proof Delta_gt_0_Theta_D_exit_gt_0-1 for formula horizontal.Delta_gt_0_Theta_D (case "sqv(v) > 0") (("1" (split) (("1" (flatten) (("1" (lemma "Theta_D_exit_gt_0") (("1" (inst? -1) (("1" (assert) (("1" (lemma "horizontal_conflict") (("1" (inst?) (("1" (assert) nil))))))))))))) ("2" (flatten) (("2" (assert) (("2" (expand "Theta_D") (("2" (lemma "Delta_discr2b") (("2" (inst?) (("2" (beta) (("2" (expand "root2b") (("2" (replaces -1) (("2" (cross-mult -1) (("2" (real-props) (("2" (move-terms -1 l 2) (("2" (real-props) (("2" (lemma "sqrt_gt") (("2" (inst -1 "discr2b(sqv(v), s * v, sqv(s) - sq(D))" "sq(s*v)") (("2" (assert) (("2" (hide (-2 -4)) (("2" (expand "discr2b") (("2" (move-terms -1 l 1) (("2" (assert) (("2" (mult-by 1 "sqv(v)") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil)))))))))))))) ";;; developed with shostak decision procedures") nil nil) (Theta_D_exit_gt_0-1 nil 3451150216 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (hide -2) (("" (expand "horizontal_conflict?") (("" (skeep -2) (("" (lemma "horizontal_los_inside_Theta") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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/") (sq_nz_pos application-judgement "posreal" sq "reals/")) nil)) (Theta_D_entry_lt_t_TCC1 0 (Theta_D_entry_lt_t_TCC1-1 nil 3460762246 ("" (subtype-tcc) nil nil) ((nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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) (comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (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) (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) (/= const-decl "boolean" notequal nil) (real_times_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)) (Theta_D_entry_lt_t 0 (Theta_D_entry_lt_t-1 nil 3460631023 ("" (skeep) (("" (beta) (("" (flatten) (("" (use "Delta_gt_0_nzv") (("" (assert) (("" (flatten) (("" (case "sqv(v) > 0") (("1" (expand "Theta_D") (("1" (expand "root2b") (("1" (lemma "Delta_discr2b") (("1" (inst?) (("1" (assert) (("1" (replaces -1 :dir rl) (("1" (name-replace "dd" "Delta(s,v)") (("1" (split) (("1" (flatten) (("1" (cross-mult 1) (("1" (case "s * v + sqv(v) * t >= 0") (("1" (assert) nil nil) ("2" (assert) (("2" (case "-sqrt(dd) < s * v + sqv(v) * t") (("1" (assert) nil nil) ("2" (hide 3) (("2" (name-replace "aa" "s * v + sqv(v) * t") (("2" (neg-formula 1) (("2" (both-sides-f 1 "sq") (("1" (sq-simp) nil nil) ("2" (rewrite "sq_lt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (cross-mult -1) (("2" (case "-sqrt(dd) < s * v + sqv(v) * t") (("1" (hide -2) (("1" (name-replace "aa" "s * v + sqv(v) * t") (("1" (neg-formula -1) (("1" (both-sides-f -1 "sq") (("1" (sq-simp) nil nil) ("2" (rewrite "sq_lt") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Delta_gt_0_nzv formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (Theta_D const-decl "real" horizontal nil) (Delta_discr2b formula-decl nil horizontal nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (Delta const-decl "real" horizontal nil) (= const-decl "[T, T -> boolean]" equalities nil) (negreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (sq_neg formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sq_lt formula-decl nil sq "reals/") (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props nil) (mult_neg formula-decl nil extra_tegies nil) (neg_neg formula-decl nil extra_tegies nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (dd skolem-const-decl "real" horizontal nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (- const-decl "[numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (root2b const-decl "real" quadratic_2b "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals 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) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals 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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (horizontal_conflict_entry_TCC1 0 (horizontal_conflict_entry_TCC1-1 nil 3451241048 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((horizontal_conflict formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Sp_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal 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) (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) (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (horizontal_conflict_entry 0 (horizontal_conflict_entry-1 nil 3451241217 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (expand "horizontal_conflict?") (("" (skeep -3) (("" (inst 1 "nnt-t") (("1" (rewrite "add_assoc" :dir rl) (("1" (rewrite "scal_add_left" :dir rl) nil nil)) nil) ("2" (lemma "horizontal_los_inside_Theta") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict formula-decl nil horizontal 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/") (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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (horizontal_conflict? const-decl "bool" horizontal nil) (real_minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnt skolem-const-decl "nnreal" horizontal nil) (t skolem-const-decl "real" horizontal nil) (real_plus_real_is_real application-judgement "real" reals nil) (scal_add_left formula-decl nil vectors_2D "vectors/") (add_assoc formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (horizontal_los_inside_Theta formula-decl nil horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal 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) (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) (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (not_horizontal_conflict_exit_TCC1 0 (not_horizontal_conflict_exit_TCC1-1 nil 3463397521 ("" (skeep) (("" (lemma "Delta_ge_0_2") (("" (inst?) (("" (assert) (("" (expand "horizontal_conflict?") (("" (skosimp*) (("" (inst + "nnt!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Delta_ge_0_2 formula-decl nil horizontal 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) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (horizontal_conflict? const-decl "bool" horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (not_horizontal_conflict_exit 0 (not_horizontal_conflict_exit-1 nil 3451319212 ("" (skeep) (("" (lemma "horizontal_conflict") (("" (inst?) (("" (assert) (("" (flatten) (("" (expand "horizontal_conflict?" -5) (("" (skeep -5) (("" (lemma "horizontal_los_inside_Theta") (("" (inst -1 "nzv" "s" "t+nnt") (("" (split -1) (("1" (rewrite "scal_add_left") (("1" (rewrite "add_assoc") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (horizontal_conflict? const-decl "bool" horizontal nil) (horizontal_los_inside_Theta formula-decl nil horizontal nil) (* const-decl "Vector" vectors_2D "vectors/") (add_assoc formula-decl nil vectors_2D "vectors/") (scal_add_left formula-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (Theta_D_horizontal_dir_TCC1 0 (Theta_D_horizontal_dir_TCC1-1 nil 3463413713 ("" (subtype-tcc) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (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) (real_times_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)) (Theta_D_horizontal_dir 0 (Theta_D_horizontal_dir-1 nil 3463413719 ("" (skeep) (("" (rewrite "dot_add_left") (("" (rewrite "sqv" :dir rl) (("" (expand "Theta_D") (("" (lemma "Delta_discr2b") (("" (inst?) (("1" (beta) (("1" (expand "root2b") (("1" (replaces -1 :dir rl) (("1" (field) (("1" (hide-all-but 1) (("1" (typepred "eps") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Delta_gt_0_nzv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (dot_add_left formula-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_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) (* const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Delta const-decl "real" horizontal 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/") (Theta_D const-decl "real" horizontal nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (v skolem-const-decl "Vect2" horizontal nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (root2b const-decl "real" quadratic_2b "reals/") (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (nnreal type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "real" vectors_2D "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ 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) (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) (Delta_gt_0_nzv formula-decl nil horizontal nil) (Delta_discr2b formula-decl nil horizontal nil) (sqv const-decl "nnreal" vectors_2D "vectors/")) nil)) (horizontal_tca_midpoint 0 (horizontal_tca_midpoint-1 nil 3448792764 ("" (skeep) (("" (hide -1) (("" (grind) nil nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (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) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Theta_D const-decl "real" horizontal nil) (root2b const-decl "real" quadratic_2b "reals/") (discr2b const-decl "real" quadratic_2b "reals/") (sq const-decl "nonneg_real" sq "reals/") (horizontal_tca const-decl "real" definitions nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/")) shostak)) (horizontal_tca_entry_exit_TCC1 0 (horizontal_tca_entry_exit_TCC1-1 nil 3463397521 ("" (subtype-tcc) nil nil) ((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) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (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) (real_times_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)) (horizontal_tca_entry_exit 0 (horizontal_tca_entry_exit-1 nil 3448791091 ("" (skeep) (("" (rewrite "horizontal_tca_midpoint") (("" (lemma "Theta_D_lt") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((horizontal_tca_midpoint formula-decl nil horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (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) (Theta_D_lt formula-decl nil horizontal nil)) shostak)) (horizontal_tca_los 0 (horizontal_tca_los-1 nil 3448810376 ("" (skeep) (("" (lemma "horizontal_tca_entry_exit") (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma "horizontal_los_inside_Theta") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_tca_entry_exit formula-decl nil horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (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) (horizontal_los_inside_Theta formula-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (horizontal_tca const-decl "real" definitions 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (horizontal_tca_le_D 0 (horizontal_tca_le_D-1 nil 3598223991 ("" (skeep) (("" (rewrite "Delta_ge_0") (("" (skeep) (("" (lemma "horizontal_tca_min") (("" (inst?) (("" (rewrite "horizontal_sq_dtca_eq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Delta_ge_0 formula-decl nil horizontal nil) (real nonempty-type-from-decl nil reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (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/") (horizontal_tca_min formula-decl nil definitions nil) (horizontal_sq_dtca_eq formula-decl nil definitions nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (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)) nil)) (horizontal_tca_pos 0 (horizontal_tca_pos-1 nil 3448814244 ("" (skeep) (("" (lemma "horizontal_tca_entry_exit") (("" (inst?) (("" (assert) (("" (flatten) (("" (lemma "Theta_D_ge_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_tca_entry_exit formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_D_ge_0 formula-decl nil horizontal nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Sp_vect2 type-eq-decl nil horizontal nil) (D formal-const-decl "posreal" horizontal 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) (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) (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) shostak)) (Theta_D_positive_conflict 0 (Theta_D_positive_conflict-1 nil 3467564658 ("" (skeep) (("" (split) (("1" (flatten) (("1" (expand "horizontal_conflict?") (("1" (skosimp*) (("1" (lemma "horizontal_los_inside_Theta") (("1" (inst - "v" "s" "nnt!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "Theta_D(s,v,-1) < 0") (("1" (expand "horizontal_conflict?") (("1" (inst + "0") (("1" (lemma "horizontal_los_inside_Theta") (("1" (inst - "v" "s" "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "horizontal_tca_entry_exit") (("2" (inst - "v" "s") (("2" (assert) (("2" (flatten) (("2" (expand "horizontal_conflict?") (("2" (inst + "horizontal_tca(s,v)") (("1" (lemma "horizontal_los_inside_Theta") (("1" (inst - "v" "s" "horizontal_tca(s,v)") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ((horizontal_conflict? const-decl "bool" horizontal nil) (horizontal_los_inside_Theta formula-decl nil horizontal 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) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (Theta_D const-decl "real" horizontal nil) (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) (Delta const-decl "real" horizontal nil) (< const-decl "bool" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (s skolem-const-decl "Vect2" horizontal nil) (v skolem-const-decl "Vect2" horizontal nil) (horizontal_tca_entry_exit formula-decl nil horizontal nil)) shostak)) (circle_solution_2D_horizontal_sep 0 (circle_solution_2D_horizontal_sep-1 nil 3466182088 ("" (skeep) (("" (skeep) (("" (expand "circle_solution_2D?") (("" (flatten) (("" (lemma "horizontal_entry_le") (("" (inst -1 "s" "tt" "t" "v") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (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) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (horizontal_entry_le formula-decl nil horizontal nil) (circle_solution_2D? const-decl "bool" horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (Theta_D_circle_solution_2D 0 (Theta_D_circle_solution_2D-3 nil 3463413379 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (lemma "Theta_D_on_D") (("" (inst?) (("1" (split) (("1" (assert) (("1" (lemma "Theta_D_horizontal_dir") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (lemma "Delta_gt_0_nzv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution_2D? const-decl "bool" horizontal nil) (zero const-decl "Vector" vectors_2D "vectors/") (v skolem-const-decl "Vect2" horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals 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) (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) (bool nonempty-type-eq-decl nil booleans 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/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_D_horizontal_dir formula-decl nil horizontal nil) (Delta_gt_0_nzv formula-decl nil horizontal nil) (Theta_D_on_D formula-decl nil horizontal nil)) nil) (Theta_D_circle_solution_2D-2 nil 3463413254 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (lemma "Theta_D_on_D") (("" (inst?) (("1" (split) (("1" (assert) (("1" (lemma "Theta_D_horizontal_dir") (("1" (inst?) (("1" (assert) nil))))))) ("2" (assert) nil))) ("2" (assert) (("2" (flatten) (("2" (lemma "Delta_gt_0_nzv") (("2" (inst?) (("2" (assert) nil)))))))))))))))) nil) nil nil) (Theta_D_circle_solution_2D-1 nil 3463413151 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (lemma "Theta_D_on_D") (("" (inst?) (("1" (split) (("1" (assert) (("1" (lemma "Theta_D_horizontal_dir") (("1" (inst?) (("1" (assert) nil))))))) ("2" (assert) nil))) ("2" (assert) (("2" (flatten) (("2" (lemma "Delta_gt_0_nzv") (("2" (inst?) (("2" (assert) nil)))))))))))))))) nil) nil nil)) (circle_solution_2D_Delta_ge_0 0 (circle_solution_2D_Delta_ge_0-1 nil 3466349793 ("" (skeep) (("" (lemma "Delta_ge_0") (("" (inst?) (("" (assert) (("" (expand "circle_solution_2D?") (("" (flatten) (("" (inst 1 "t") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Delta_ge_0 formula-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (circle_solution_2D? const-decl "bool" horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil)) nil)) (circle_solution_2D_Theta_D_TCC1 0 (circle_solution_2D_Theta_D_TCC1-1 nil 3466349793 ("" (skeep) (("" (lemma "circle_solution_2D_Delta_ge_0") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((circle_solution_2D_Delta_ge_0 formula-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "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) (bool nonempty-type-eq-decl nil booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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 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)) (circle_solution_2D_Theta_D 0 (circle_solution_2D_Theta_D-2 nil 3466348778 ("" (skeep) (("" (lemma "circle_solution_2D_Delta_ge_0") (("" (inst?) (("" (assert) (("" (expand "circle_solution_2D?") (("" (flatten) (("" (lemma "Theta_D_unique_eps") (("" (inst - "nzv" "s" "t") (("" (assert) (("" (skosimp*) (("" (case "eps!1 = dir") (("1" (assert) nil nil) ("2" (lemma "Theta_D_horizontal_dir") (("2" (inst - "eps!1" "s" "nzv") (("2" (assert) (("2" (replace -2 - rl) (("2" (case "((s + t * nzv) * nzv) = 0") (("1" (lemma "horizontal_tca_los") (("1" (inst - "nzv" "s") (("1" (split -1) (("1" (lemma "sdotv_lt_0") (("1" (inst-cp -1 "s+t*nzv" "nzv") (("1" (inst -1 "s+t*nzv" "-nzv") (("1" (case-replace "(s+t*nzv)*-nzv = 0") (("1" (assert) (("1" (expand "horizontal_conflict?") (("1" (case "t >= horizontal_tca(s,nzv)") (("1" (inst + "t-horizontal_tca(s,nzv)") (("1" (hide 2) (("1" (case-replace "s + t * nzv + (t - horizontal_tca(s, nzv)) * -nzv = s + horizontal_tca(s, nzv) * nzv") (("1" (name "tz" "horizontal_tca(s,nzv)") (("1" (replace -1) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "horizontal_tca(s,nzv) - t") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "horizontal_tca(s,nzv) - t") (("1" (case-replace "s + t * nzv + (horizontal_tca(s, nzv) - t) * nzv = s + horizontal_tca(s, nzv) * nzv") (("1" (name "tz" "horizontal_tca(s,nzv)") (("1" (replace -1) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Theta_D_Delta_eq_0") (("2" (inst - "nzv" "s") (("2" (assert) (("2" (case "(eps!1 = 1 and dir = -1) OR (eps!1 = -1 and dir = 1)") (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (typepred "eps!1") (("2" (typepred "dir") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(s + t * nzv) * nzv > 0") (("1" (lemma "pos_times_le") (("1" (inst - "eps!1" "(s + t * nzv) * nzv") (("1" (assert) (("1" (lemma "pos_times_le") (("1" (inst - "dir" "(s + t * nzv) * nzv") (("1" (assert) (("1" (typepred "dir") (("1" (typepred "eps!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "neg_times_le") (("2" (inst - "-dir" "(s + t * nzv) * nzv") (("2" (assert) (("2" (lemma "neg_times_le") (("2" (inst - "-eps!1" "(s + t * nzv) * nzv") (("2" (assert) (("2" (typepred "eps!1") (("2" (typepred "dir") (("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) ((circle_solution_2D_Delta_ge_0 formula-decl nil horizontal nil) (Theta_D_horizontal_dir formula-decl nil horizontal nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (* const-decl "real" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (Theta_D_Delta_eq_0 formula-decl nil horizontal nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sdotv_lt_0 formula-decl nil horizontal nil) (- const-decl "Vector" vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (neg_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (nzv skolem-const-decl "Nz_vect2" horizontal nil) (s skolem-const-decl "Vect2" horizontal nil) (t skolem-const-decl "real" horizontal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (horizontal_conflict? const-decl "bool" horizontal nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_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" horizontal nil) (Sp_vect2 type-eq-decl nil horizontal nil) (horizontal_tca_los formula-decl nil horizontal nil) (neg_times_le formula-decl nil real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (pos_times_le formula-decl nil real_props 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) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (Theta_D_unique_eps formula-decl nil horizontal nil) (circle_solution_2D? const-decl "bool" horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "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) (bool nonempty-type-eq-decl nil booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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 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) (circle_solution_2D_Theta_D-1 nil 3466346897 ("" (skeep) (("" (expand "circle_solution_2D?") (("" (flatten) (("" (lemma "Theta_D_unique_eps") (("" (inst -1 "nzv" "s" "t") (("" (assert) (("" (skolem -1 "eps1") (("" (case-replace "eps1=dir") (("" (case-replace "eps1=-dir") (("1" (hide -1 1) (("1" (lemma "Theta_D_horizontal_dir") (("1" (inst?) (("1" (replaces -2 :dir rl) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (typepred "eps1" "dir") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil)) (circle_solution_2D_strict_horizontal_sep 0 (circle_solution_2D_strict_horizontal_sep-1 nil 3467651708 ("" (skeep) (("" (lemma "circle_solution_2D_Theta_D") (("" (inst?) (("" (assert) (("" (lemma "horizontal_sep_outside_Theta") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (lemma "Delta_ge_0") (("" (inst?) (("" (assert) (("" (inst + "t") (("" (expand "circle_solution_2D?") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((circle_solution_2D_Theta_D formula-decl nil horizontal nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (circle_solution_2D? const-decl "bool" horizontal nil) (Delta_ge_0 formula-decl nil horizontal nil) (horizontal_sep_outside_Theta formula-decl nil horizontal nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "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) (bool nonempty-type-eq-decl nil booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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 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)) (Theta_D_line_intersection 0 (Theta_D_line_intersection-2 "" 3504655736 ("" (skeep) (("" (skoletin 1) (("" (flatten) (("" (cross-mult 2) (("1" (lemma "Theta_D_unique_eps") (("1" (inst - "v" "s" "Theta_D(s,v,eps)") (("1" (assert) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (name "td" "Theta_D(s,v,eps)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "eps") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (AND const-decl "[bool, 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) (>= const-decl "bool" reals nil) (Delta const-decl "real" horizontal nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "real" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (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" horizontal nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (v skolem-const-decl "Vect2" horizontal nil) (s skolem-const-decl "Vect2" horizontal nil) (real_minus_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Theta_D_unique_eps formula-decl nil horizontal nil)) shostak) (Theta_D_line_intersection-1 nil 3470492680 ("" (skeep) (("" (skoletin 1) (("" (flatten) (("" (cross-mult 2) (("" (lemma "Theta_D_unique_eps") (("" (inst - "v" "s" "Theta_D(s,v,eps)") (("1" (assert) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (name "td" "Theta_D(s,v,eps)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "eps") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Sign type-eq-decl nil sign "reals/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/")) shostak)) (tangent_line_intersection_v_independent 0 (tangent_line_intersection_v_independent-2 "" 3504714516 ("" (skeep) (("" (expand "sqv") (("" (rewrite "dot_add_left") (("" (rewrite "dot_add_left") (("" (case "pt * (v * (s + pt * v)) = pr * (w * (s + pt * v))") (("1" (hide -2) (("1" (name "const34" "v * (s + pt * v)") (("1" (replace -1) (("1" (name "const35" "w * (s + pt * v)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (expand "sign") (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (div-by -2 "pr") (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst - "pt/pr" "const34") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (ground) (("2" (div-by -2 "pt") (("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "pr/pt" "const35") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (both_sides_div1 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sign const-decl "Sign" sign "reals/") (* const-decl "real" vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals 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) (* const-decl "Vector" vectors_2D "vectors/") (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (dot_add_left formula-decl nil vectors_2D "vectors/")) shostak) (tangent_line_intersection_v_independent-1 nil 3471084326 ("" (skeep) (("" (expand "sqv") (("" (rewrite "dot_add_left") (("" (rewrite "dot_add_left") (("" (case "pt * (v * (s + pt * v)) = pr * (w * (s + pt * v))") (("1" (hide -2) (("1" (name "const34" "v * (s + pt * v)") (("1" (replace -1) (("1" (name "const35" "w * (s + pt * v)") (("1" (replace -1) (("1" (hide -1) (("1" (hide -1) (("1" (expand "sign") (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (div-by -2 "pt") (("1" (lemma "nnreal_times_nnreal_is_nnreal") (("1" (inst - "pr/pt" "const35") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (div-by -2 "pr") (("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "pt/pr" "const34") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sqv const-decl "nnreal" vectors_2D "vectors/") (sign const-decl "Sign" sign "reals/") (* const-decl "real" vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (dot_add_left formula-decl nil vectors_2D "vectors/")) shostak)) (tangent_vector_not_conflict 0 (tangent_vector_not_conflict-2 nil 3471108285 ("" (skeep) (("" (lemma "Delta_gt_0_nzv") (("" (inst?) (("" (assert) (("" (name "pp" "s + Theta_D(s, v, dir) * v") (("" (label "ppname" -1) (("" (replace -1) (("" (case "sqv(pp) = sq(D)") (("1" (label "onD" -1) (("1" (expand "horizontal_conflict?") (("1" (skosimp*) (("1" (case "s*pp = sq(D)") (("1" (label "spponD" -1) (("1" (case "(s + nnt!1*v)*pp = sq(D)") (("1" (lemma "cauchy_schwarz") (("1" (inst?) (("1" (replace -2) (("1" (replace "onD") (("1" (expand "sq" -1 1) (("1" (div-by -1 "sq(D)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sqv" "onD") (("2" (name-replace "TD" "Theta_D(s,v,dir)") (("2" (case "v*pp = 0") (("1" (hide-all-but (-1 -2 1)) (("1" (grind) nil nil)) nil) ("2" (case-replace "pp*pp = (s+TD*v)*pp") (("1" (hide -1) (("1" (rewrite "dot_add_left" "onD") (("1" (replace -1) (("1" (move-terms -2 l 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "dot_add_left") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Theta_D_on_D") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Delta_gt_0_nzv formula-decl nil horizontal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_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" horizontal nil) (horizontal_conflict? const-decl "bool" horizontal nil) (* const-decl "real" vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_div_pos_le1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div_cancel2 formula-decl nil extra_real_props nil) (real_le_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) (cauchy_schwarz formula-decl nil vectors_2D "vectors/") (dot_add_left formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (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) (Theta_D_on_D formula-decl nil horizontal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Vector type-eq-decl nil vectors_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "Vector" vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (* const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (zero const-decl "Vector" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (Delta const-decl "real" horizontal 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) (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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil)) nil) (tangent_vector_not_conflict-1 nil 3471108265 ("" (skeep) (("" (postpone) nil nil)) nil) nil shostak)) (horizontal_conflict_is_an_open_set 0 (horizontal_conflict_is_an_open_set-2 nil 3471192141 ("" (skeep) (("" (expand "horizontal_conflict?" -1) (("" (skosimp*) (("" (label "underD" -1) (("" (case "nnt!1 /= 0") (("1" (flatten) (("1" (name "delta" "D - norm(ss + nnt!1 * vv)") (("1" (label "deltaname" -1) (("1" (inst + "delta/(2*nnt!1)") (("1" (skeep 2) (("1" (expand "horizontal_conflict?") (("1" (inst + "nnt!1") (("1" (case "norm(ss + nnt!1 * (vv + ww)) < D") (("1" (lemma "sq_lt") (("1" (inst?) (("1" (assert) (("1" (lemma "vectors_2D.sqrt_sqv_norm") (("1" (inst?) (("1" (hide-all-but (-2 2)) (("1" (name "cv2" "ss + nnt!1*(vv+ww)") (("1" (replace -1) (("1" (case "sq(norm(cv2)) = sqv(cv2)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "sqv") (("2" (expand "norm") (("2" (expand "sqv") (("2" (rewrite "sq_sqrt") (("2" (typepred "sqv(cv2)") (("2" (expand "sqv") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "vectors_2D.norm_add_le") (("2" (inst - "ss + nnt!1*vv" "nnt!1*ww") (("2" (assert) (("2" (case "ss + nnt!1 * vv + nnt!1 * ww = ss + nnt!1 * (vv + ww)") (("1" (case "norm(nnt!1 * ww) + norm(ss + nnt!1 * vv) < D") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide -2) (("2" (hide -1) (("2" (rewrite "norm_scal") (("2" (case "abs(nnt!1) = nnt!1") (("1" (replace -1) (("1" (case "nnt!1*norm(ww) < delta") (("1" (assert) nil nil) ("2" (hide 2) (("2" (div-by 1 "nnt!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (propax) 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) ("2" (case "delta /( 2*nnt!1) > 0") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) (("2" (case "norm(ss+nnt!1*vv) < D") (("1" (assert) nil nil) ("2" (hide (2 3)) (("2" (lemma "sq_lt") (("2" (inst?) (("2" (assert) (("2" (case "sq(norm(ss+nnt!1*vv)) = sqv(ss+nnt!1*vv)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "norm") (("2" (rewrite "sq_sqrt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (inst + "1") (("2" (skosimp*) (("2" (expand "horizontal_conflict?") (("2" (inst + "nnt!1") (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((horizontal_conflict? const-decl "bool" horizontal nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (times_div_cancel1 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (norm_scal formula-decl nil vectors_2D "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (norm_add_le formula-decl nil vectors_2D "vectors/") (sq_lt formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (sq_sqrt formula-decl nil sqrt "reals/") (* const-decl "real" vectors_2D "vectors/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (< const-decl "bool" reals nil) (delta skolem-const-decl "real" horizontal nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nnt!1 skolem-const-decl "nnreal" horizontal nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil 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) (D formal-const-decl "posreal" horizontal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil)) nil) (horizontal_conflict_is_an_open_set-1 nil 3471192120 ("" (skeep) (("" (expand "conflict?" -1) (("" (skosimp*) (("" (label "underH" -1) (("" (label "underD" -2) (("" (case "nnt!1 /= 0") (("1" (flatten) (("1" (name "del1" "H - abs(ss`z + nnt!1 * vv`z)") (("1" (label "del1name" -1) (("1" (name "del2" "D - norm(vect2(ss) + nnt!1 * vect2(vv))") (("1" (label "del2name" -1) (("1" (case "del2 > 0") (("1" (label "del2pos" -1) (("1" (hide "del2pos") (("1" (name "delta" "min(del1,del2)") (("1" (label "deltaname" -1) (("1" (inst + "delta/(2*nnt!1)") (("1" (skeep 2) (("1" (case "norm(ww) >= abs(ww`z) AND norm(ww) >= norm(vect2(ww))") (("1" (label "normlem" -1) (("1" (hide "normlem") (("1" (expand "conflict?") (("1" (inst + "nnt!1") (("1" (split 2) (("1" (lemma "triangle") (("1" (rewrite "vz_distr_add") (("1" (assert) (("1" (inst - "ss`z + vv`z*nnt!1" "ww`z*nnt!1") (("1" (case "abs(ww`z*nnt!1) < del1") (("1" (assert) nil) ("2" (hide 2) (("2" (rewrite "abs_mult") (("2" (case "abs(nnt!1) = nnt!1") (("1" (replace -1) (("1" (reveal "normlem") (("1" (flatten) (("1" (div-by 1 "nnt!1") (("1" (case "del1 / nnt!1 >= delta / (2 * nnt!1)") (("1" (assert) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (div-by 1 "nnt!1") (("2" (assert) nil))))))))))))))))) ("2" (expand "abs") (("2" (propax) nil))))))))))))))))))) ("2" (case "norm(vect2(ss) + nnt!1 * vect2(vv + ww)) < D") (("1" (lemma "sq_lt") (("1" (inst?) (("1" (assert) (("1" (lemma "vectors_2D.sqrt_sqv_norm") (("1" (inst?) (("1" (replace -1 :dir rl) (("1" (rewrite "vect2_add") (("1" (assert) nil))))))))))))))) ("2" (hide 2) (("2" (rewrite "vect2_add") (("2" (lemma "vectors_2D.norm_add_le") (("2" (inst - "vect2(ss) + nnt!1*vect2(vv)" "nnt!1*vect2(ww)") (("2" (assert) (("2" (case "norm(nnt!1 * vect2(ww)) + norm(vect2(ss) + nnt!1 * vect2(vv)) < D") (("1" (case "vect2(ss) + nnt!1 * vect2(vv) + nnt!1 * vect2(ww) = vect2(ss) + nnt!1 * (vect2(vv) + vect2(ww)) (("1" (assert) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (grind) nil))))))) ("2" (case "norm(nnt!1*vect2(ww)) < del2") (("1" (assert) nil) ("2" (hide 2) (("2" (hide 2) (("2" (rewrite "norm_scal") (("2" (case "abs(nnt!1) = nnt!1") (("1" (replace -1) (("1" (div-by 1 "nnt!1") (("1" (case "del2 / nnt!1 >= delta/(2*nnt!1)") (("1" (reveal "normlem") (("1" (flatten) (("1" (assert) nil))))) ("2" (hide 2) (("2" (cross-mult 1) (("2" (div-by 1 "nnt!1") (("2" (case "2*del2 >= delta") (("1" (assert) nil) ("2" (case "del2 > 0") (("1" (hide-all-but (-1 "deltaname" 1)) (("1" (grind) nil))) ("2" (replace "del2name" :dir rl) (("2" (hide-all-but ("underD" 1)) (("2" (case "sqv(vect2(ss) + nnt!1 * vect2(vv)) = sq(norm(vect2(ss) + nnt!1 * vect2(vv)))") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sq_lt") (("1" (inst?) (("1" (assert) nil))))))))) ("2" (hide-all-but 1) (("2" (name "cvect1" "vect2(ss) + nnt!1 * vect2(vv)") (("2" (replace -1) (("2" (hide -1) (("2" (expand "norm") (("2" (lemma "sq_sqrt") (("2" (inst?) (("2" (split -1) (("1" (assert) nil) ("2" (assert) nil))))))))))))))))))))))))))))))))))))))) ("2" (expand "abs") (("2" (propax) nil))))))))))))))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (split) (("1" (expand "norm") (("1" (expand "sqv") (("1" (lemma "sq_ge") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "*") (("1" (expand "sq" 1 2) (("1" (lemma "sqrt_ge") (("1" (inst - "ww`x * ww`x + ww`y * ww`y + ww`z * ww`z" "ww`z*ww`z") (("1" (assert) nil))))))))))))) ("2" (typepred "sqv(ww)") (("2" (expand "sqv") (("2" (propax) nil))))))))))))) ("2" (expand "norm") (("2" (expand "sqv") (("2" (lemma "sqrt_ge") (("2" (inst?) (("1" (assert) (("1" (hide 2) (("1" (grind) nil))))) ("2" (typepred "sqv(vect2(ww))") (("2" (expand "sqv") (("2" (propax) nil))))) ("3" (typepred "sqv(ww)") (("3" (expand "sqv") (("3" (propax) nil))))))))))))))))))))) ("2" (case "delta /( 2*nnt!1) > 0") (("1" (assert) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (reveal "del2pos") (("2" (case "delta = del1 or delta = del2") (("1" (ground) nil) ("2" (hide-all-but ("deltaname" 1)) (("2" (grind) nil))))))))))) ("3" (assert) nil))) ("3" (assert) nil))))))))))) ("2" (lemma "sq_lt") (("2" (inst - "norm(vect2(ss) + nnt!1 * vect2(vv))" "D") (("2" (assert) (("2" (name "cvect3" "vect2(ss) + nnt!1 * vect2(vv)") (("2" (replace -1) (("2" (case "sqv(cvect3) = sq(norm(cvect3))") (("1" (assert) nil) ("2" (hide-all-but 1) (("2" (lemma "vectors_2D.sqrt_sqv_norm") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (lemma "sq_sqrt") (("2" (inst?) (("2" (split -1) (("1" (assert) nil) ("2" (assert) nil))))))))))))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (inst + "1") (("2" (skeep) (("2" (expand "conflict?") (("2" (inst + "0") (("2" (assert) nil)))))))))))))))))))))))))) nil) nil nil)))
¤ 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.588Bemerkung: (vorverarbeitet am 2026-04-28) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26