| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 515 kB |
|
Quelle repulsive.prfSprache: Lisp |
|||||||||||||||
|
(repulsive (tca_TCC1 0 (tca_TCC1-1 nil 3481393354 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (repulsive_simple 0 (repulsive_simple-1 nil 3581756359 ("" (skeep) (("" (case "s*v<0") (("1" (hide 2) (("1" (assert) (("1" (case "tca(s,v) > 0") (("1" (assert) (("1" (skeep) (("1" (expand "repulsive?") (("1" (split -) (("1" (case "s*nv>=0") (("1" (lemma "closest_approach_2D.dot_nneg_divergent") (("1" (inst - "s" "zero" "nv" "zero") (("1" (assert) (("1" (case "norm(s)>=norm(s+tca(s,v)*v)") (("1" (assert) (("1" (split -) (("1" (expand "divergent?") (("1" (case "t = 0") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (inst - "t") (("1" (assert) (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "horizontal_tca_min") (("2" (inst - "v" "s" "0") (("1" (assert) (("1" (rewrite "horizontal_sq_dtca_eq") (("1" (rewrite "sqrt_le" -1 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (rewrite "sqrt_sqv_norm") (("1" (expand "tca" +) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "tca" -1) (("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "horizontal_tca" -1) (("2" (cross-mult -1) (("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "nv = zero OR v = zero") (("1" (split -) (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "tca") (("2" (assert) (("2" (lemma "horizontal_tca_min") (("2" (inst - "nv" "s" "t") (("2" (rewrite "horizontal_sq_dtca_eq") (("2" (rewrite "sqrt_le" -1 :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_sqv_norm") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "tca" 1) (("2" (lift-if) (("2" (ground) (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (expand "horizontal_tca") (("2" (cross-mult 2) (("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (skeep 2) (("2" (expand "repulsive?") (("2" (flatten) (("2" (case "NOT s*nv>=0") (("1" (assert) nil nil) ("2" (hide (-2 -3)) (("2" (lemma "closest_approach_2D.dot_nneg_divergent") (("2" (inst - "s" "zero" "nv" "zero") (("2" (assert) (("2" (case "nv = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "divergent?") (("2" (inst - "t") (("1" (assert) (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "t = 0") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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 "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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_neg_gt1 formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (repulsive? const-decl "bool" repulsive nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals nil) (zero const-decl "Vector" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_left formula-decl nil vectors_2D "vectors/") (dist_norm formula-decl nil distance_2D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (t skolem-const-decl "nnreal" repulsive nil) (divergent? const-decl "bool" closest_approach_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (horizontal_tca_min formula-decl nil definitions nil) (horizontal_tca const-decl "real" definitions nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (sqrt_le formula-decl nil sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (horizontal_sq_dtca_eq formula-decl nil definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (v skolem-const-decl "Vect2" repulsive nil) (/= const-decl "boolean" notequal nil) (sub_zero_right formula-decl nil vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (dot_nneg_divergent formula-decl nil closest_approach_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (tca const-decl "real" repulsive nil) (> const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (t skolem-const-decl "nnreal" repulsive nil)) shostak)) (repulsive_transitive 0 (repulsive_transitive-1 nil 3549787475 ("" (skeep) (("" (expand "repulsive?") (("" (flatten) (("" (assert) (("" (case "v = zero") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "s*v < 0") (("1" (assert) (("1" (flatten) (("1" (hide 4) (("1" (ground) (("1" (expand "tca" -3) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (expand "horizontal_tca") (("2" (cross-mult -1) (("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "tca" 2) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (expand "horizontal_tca") (("2" (cross-mult 2) (("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "tca") (("3" (expand "horizontal_tca") (("3" (cross-mult 2) (("3" (ground) (("3" (lemma "sqv_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "tca") (("4" (lift-if 3) (("4" (ground) (("4" (expand "horizontal_tca") (("4" (cross-mult 2) (("4" (ground) (("4" (lemma "sqv_eq_0") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "tca" 2) (("5" (lift-if) (("5" (ground) (("5" (expand "horizontal_tca") (("5" (cross-mult 2) (("5" (ground) (("5" (lemma "sqv_eq_0") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "tca" 2) (("6" (assert) (("6" (expand "horizontal_tca") (("6" (ground) (("6" (cross-mult 2) (("6" (ground) (("6" (lemma "sqv_eq_0") (("6" (inst?) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (expand "tca" 3) (("7" (assert) (("7" (lift-if) (("7" (ground) (("7" (expand "horizontal_tca") (("7" (ground) (("7" (cross-mult 2) (("7" (ground) (("7" (lemma "sqv_eq_0") (("7" (inst?) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((repulsive? const-decl "bool" repulsive nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_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/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (tca const-decl "real" repulsive nil) (horizontal_tca const-decl "real" definitions nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil) (real_div_nzreal_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) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (* const-decl "real" vectors_2D "vectors/") (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) (real_plus_real_is_real application-judgement "real" reals 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/")) shostak)) (not_repulsive_sum_closed 0 (not_repulsive_sum_closed-1 nil 3481443204 ("" (expand "sum_closed_2D?") (("" (skosimp*) (("" (ground) (("" (expand "repulsive?") (("" (case "tca(s!1,nv!1)>=0 AND tca(s!1,nw!1)>=0") (("1" (flatten) (("1" (assert) (("1" (split -) (("1" (hide-all-but (-1 1 3)) (("1" (expand "tca") (("1" (lift-if) (("1" (ground) (("1" (case "nv!1 = -nw!1") (("1" (replace -1) (("1" (expand "horizontal_tca") (("1" (rewrite "sqv_neg") (("1" (case "sqv(nw!1)>0") (("1" (cross-mult 2) (("1" (cross-mult 4) (("1" (hide-all-but (2 4)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst - "nw!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "sqv(nv!1+nw!1)>0 AND sqv(nv!1)>0 AND sqv(nw!1)>0") (("1" (flatten) (("1" (expand "horizontal_tca") (("1" (cross-mult -4) (("1" (cross-mult 2) (("1" (cross-mult 4) (("1" (hide-all-but (-4 2 4)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst-cp - "nv!1+nw!1") (("2" (inst-cp - "nv!1") (("2" (inst - "nw!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (epsilon: posreal): norm(s!1 + tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)) <=norm(s!1 + (("1" (case "FORALL (epsilon: posreal): norm(s!1 + tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)) < norm(s!1 + tca(s!1, v!1) * v!1) + epsilon") (("1" (inst - "norm(s!1 + tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)) - norm(s!1 + tca(s!1, v!1) * v!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (skosimp*) (("2" (inst - "epsilon!1/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (skosimp*) (("2" (name "A" "norm(s!1 + tca(s!1, v!1) * v!1) + epsilon!1") (("2" (replace -1) (("2" (case "NOT (norm(s!1 + tca(s!1, v!1) * v!1) + epsilon!1 > norm(s!1 + tca(s!1, nw!1) * nw!1) AND nor (("1" (ground) nil nil) ("2" (flatten) (("2" (label "Aname" -3) (("2" (hide "Aname") (("2" (lemma "horizontal_conflict_sum_closed[A]") (("2" (inst - "s!1" "nv!1" "nw!1") (("2" (split -) (("1" (expand "horizontal_conflict?") (("1" (skosimp*) (("1" (lemma "horizontal_tca_los[A]") (("1" (inst - "nv!1 + nw!1" "s!1") (("1" (split -) (("1" (rewrite "sqrt_sqv_norm" :dir rl) (("1" (rewrite "sqrt_sqv_norm" :dir rl) (("1" (lemma "sq_le") (("1" (inst?) (("1" (assert) (("1" (expand "tca" 1) (("1" (lift-if) (("1" (ground) (("1" (case "nv!1=-nw!1") (("1" (replace -1) (("1" (hide-all-but (3 5)) (("1" (expand "tca") (("1" (lift-if) (("1" (ground) (("1" (expand "horizontal_tca") (("1" (rewrite "sqv_neg") (("1" (case "sqv(nw!1)>0") (("1" (cross-mult 2) (("1" (cross-mult 3) (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (vvk: Vect2): sq(norm(vvk)) = sqv(vvk)") (("1" (inst - "s!1 + horizontal_tca(s!1, nv!1 + nw!1) * (nv!1 + nw!1)") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (lemma "sqrt_eq") (("2" (inst?) (("2" (assert) (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Delta_gt_0[A]") (("2" (inst - "s!1" "nv!1+nw!1") (("2" (assert) (("2" (case "nv!1+nw!1 = zero") (("1" (hide-all-but (-1 4 6)) (("1" (case "nv!1=-nw!1") (("1" (replace -1) (("1" (expand "tca") (("1" (lift-if) (("1" (ground) (("1" (expand "horizontal_tca") (("1" (rewrite "sqv_neg") (("1" (case "sqv(nw!1)>0") (("1" (cross-mult 2) (("1" (cross-mult 4) (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "horizontal_conflict_ever?") (("2" (inst + "nnt!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (-1 2 4)) (("2" (case "nv!1=-nw!1") (("1" (replace -1) (("1" (case "sqv(nw!1)>0") (("1" (expand "tca") (("1" (lift-if) (("1" (ground) (("1" (expand "horizontal_tca") (("1" (cross-mult 2) (("1" (cross-mult 4) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) (("2" (expand "tca") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "horizontal_conflict?") (("2" (inst + "tca(s!1,nv!1)") (("2" (case "norm(s!1 + tca(s!1, nv!1) * nv!1) < A") (("1" (assert) (("1" (lemma "sqrt_lt") (("1" (inst - "sqv(s!1 + tca(s!1, nv!1) * nv!1)" "sq(A)") (("1" (assert) (("1" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil) ("2" (reveal "Aname") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "horizontal_conflict?") (("3" (inst + "tca(s!1,nw!1)") (("3" (case "norm(s!1 + tca(s!1, nw!1) * nw!1) < A") (("1" (lemma "sqrt_lt") (("1" (inst - "sqv(s!1 + tca(s!1, nw!1) * nw!1)" "sq(A)") (("1" (assert) (("1" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil) ("2" (reveal "Aname") (("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" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((repulsive? const-decl "bool" repulsive nil) (+ const-decl "Vector" vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (sqv_neg formula-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (neg_add_left formula-decl nil vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (nw!1 skolem-const-decl "Vect2" repulsive nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (horizontal_tca const-decl "real" definitions nil) (- const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (nv!1 skolem-const-decl "Vect2" repulsive nil) (NOT const-decl "[bool -> bool]" booleans nil) (horizontal_conflict_sum_closed formula-decl nil horizontal nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (Delta_gt_0 formula-decl nil horizontal nil) (horizontal_conflict_ever? const-decl "bool" horizontal nil) (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sq_le formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_eq formula-decl nil sqrt "reals/") (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (horizontal_tca_los formula-decl nil horizontal nil) (horizontal_conflict? const-decl "bool" horizontal nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_lt formula-decl nil sqrt "reals/") (< const-decl "bool" reals nil) (v!1 skolem-const-decl "Vect2" repulsive nil) (s!1 skolem-const-decl "Vect2" repulsive nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal 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) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (<= const-decl "bool" reals nil) (norm const-decl "nnreal" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (tca const-decl "real" repulsive nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sum_closed_2D? const-decl "bool" predicate_coordination_2D nil)) shostak)) (repulsive_criteria_scal_s 0 (repulsive_criteria_scal_s-1 nil 3535807732 ("" (case "FORALL (cc: posreal, eps: Sign, nv, s, v: Vect2): repulsive_criteria(s, v, eps)(nv) IMPLIES repulsive_criteria(cc * s, v, eps)(nv)") (("1" (skeep) (("1" (ground) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (inst - "1/cc" "eps" "nv" "cc*s" "v") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "repulsive_criteria") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (lemma "scal_zero") (("1" (inst - "1/cc") (("1" (replace -2 -1 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (mult-by -1 "cc") (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (mult-by -2 "cc") (("3" (assert) (("3" (hide-all-but (-2 1)) (("3" (grind) nil nil)) nil)) nil)) nil) ("4" (flatten) (("4" (split -) (("1" (flatten) (("1" (hide 2) (("1" (assert) (("1" (mult-by -1 "cc") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (copy -1) (("2" (mult-by -1 "cc") (("2" (assert) (("2" (ground) (("1" (replace -1) (("1" (mult-by -2 "cc") (("1" (assert) nil nil)) nil)) nil) ("2" (mult-by -1 "cc") (("2" (assert) nil nil)) nil) ("3" (replace -1) (("3" (assert) (("3" (mult-by -2 "cc") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (mult-by -1 "cc") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((scal_zero formula-decl nil vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (det const-decl "real" det_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (* const-decl "real" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (zero const-decl "Vector" vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (scal_assoc formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (repulsive_criteria const-decl "bool" repulsive nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/")) shostak)) (repulsive_criteria_scal_nv 0 (repulsive_criteria_scal_nv-1 nil 3575288101 ("" (case "FORALL (cc: posreal, eps: Sign, nv, s, v: Vect2): s*v<0 AND repulsive_criteria(s, v, eps)(nv) IMPLIES repulsive_criteria(s, v, eps)(cc*nv)") (("1" (skeep) (("1" (case "s*v<0") (("1" (assert) (("1" (hide 2) (("1" (split) (("1" (flatten) (("1" (inst - "1/cc" "eps" "cc*nv" "s" "v") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "FORALL (cc: posreal, eps: Sign, nv, s, v: Vect2): s*v>=0 AND repulsive_criteria(s, (1/cc)*v, eps)(nv) IMPLIES repulsive_criteria(s, v, eps)(cc*nv)") (("1" (hide 2) (("1" (hide -2) (("1" (split) (("1" (flatten) (("1" (inst - "1/cc" "eps" "cc*nv" "s" "(1/cc)*v") (("1" (assert) (("1" (cross-mult 2) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3 4)) (("2" (hide -1) (("2" (skosimp*) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (assert) (("2" (copy -1) (("2" (mult-by -1 "1/cc!1") (("2" (assert) (("2" (case "v!1=zero") (("1" (replace -1) (("1" (assert) (("1" (mult-by -5 "cc!1") (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (case "(1/cc!1)*(cc!1*nv!1)=zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (flatten) (("3" (mult-by -6 "cc!1") (("3" (grind) nil nil)) nil)) nil) ("4" (assert) (("4" (flatten) (("4" (assert) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case "cc!1*v!1=zero") (("1" (case "(1/cc!1)*(cc!1*v!1)=zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (split +) (("1" (flatten) (("1" (case "(1/cc!1)*(cc!1*nv!1)=zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (mult-by 1 "1/cc!1") (("2" (grind) nil nil)) nil) ("3" (mult-by -4 "cc!1") (("3" (grind) nil nil)) nil) ("4" (assert) (("4" (case "(1/cc!1)*v!1=zero") (("1" (case "cc!1*((1/cc!1)*v!1)=zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (cross-mult -6) nil nil)) nil)) nil)) nil) ("5" (mult-by -7 "cc!1^2") (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (assert) (("2" (split) (("1" (flatten) (("1" (case "(1/cc)*(cc*nv)=zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (mult-by -3 "cc") (("2" (grind) nil nil)) nil) ("3" (mult-by -4 "cc") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((both_sides_times_pos_le1 formula-decl nil real_props nil) (div_mult_pos_gt2 formula-decl nil extra_real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_expt application-judgement "posreal" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posreal_exp application-judgement "posreal" exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (det const-decl "real" det_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (scal_zero formula-decl nil vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_ge1 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) (dot_scal_right formula-decl nil vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (scal_assoc formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil) (* const-decl "Vector" vectors_2D "vectors/")) shostak)) (wedge_containment 0 (xycoord "supposing first that g = (0,1)" 3563211216 ("" (skeep) (("" (case "det(f,g) = 0") (("1" (lemma "parallel_det_0") (("1" (inst - "f" "g") (("1" (assert) (("1" (expand "parallel?") (("1" (skeep -1) (("1" (case "nzk < 0") (("1" (replaces -2) (("1" (mult-by -5 "-nzk") (("1" (hide-all-but (-4 -5)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (mult-by 2 "nzk") (("2" (hide-all-but (-6 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "det(e,g) = 0") (("1" (assert) nil nil) ("2" (assert) (("2" (case "det(e,g) > 0") (("1" (assert) (("1" (hide 4) (("1" (case "EXISTS (ce:nnreal,cf:posreal): g = ce*e + cf*f") (("1" (skeep -1) (("1" (mult-by -6 "ce") (("1" (mult-by -7 "cf") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (case "NOT FORALL (gg,ff,ee:Vect2): det(ff,ee)*gg = det(gg,ee)*ff - det(gg,ff)*ee") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (case "det(f,e) = 0") (("1" (lemma "parallel_det_0") (("1" (inst - "f" "e") (("1" (assert) (("1" (expand "parallel?") (("1" (skeep -1) (("1" (case "nzk > 0") (("1" (replaces -2) (("1" (mult-by -4 "nzk") (("1" (hide-all-but (-4 4)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (mult-by -4 "-nzk") (("2" (hide-all-but (-1 -5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "det(e,f) = 0") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (name "ce" "-det(g,f)/det(f,e)") (("2" (name "cf" "det(g,e)/det(f,e)") (("2" (case "NOT g = ce*e + cf*f") (("1" (expand "ce") (("1" (expand "cf") (("1" (inst - "g" "f" "e") (("1" (decompose-equality 1) (("1" (div-by -3 "det(f,e)") (("1" (grind) nil nil)) nil) ("2" (div-by -3 "det(f,e)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ce>=0 AND cf>0") (("1" (flatten) (("1" (inst + "ce" "cf") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "NOT det(f,e) < 0") (("1" (inst - "g" "f" "e") (("1" (case "det(g,e) < 0 AND det(g,f)>0") (("1" (flatten) (("1" (mult-by -8 "det(g,f)") (("1" (mult-by -9 "-det(g,e)") (("1" (mult-by -10 "det(f,e)") (("1" (hide +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (hide-all-but (-5 1)) (("1" (grind) nil nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (expand "ce" 1) (("1" (cross-mult 1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "cf" 1) (("2" (cross-mult 1) (("2" (hide-all-but (-6 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "det(e,g) < 0") (("1" (hide 1) (("1" (assert) (("1" (hide 3) (("1" (case "EXISTS (ce:nnreal,cf:posreal): g = ce*e + cf*f") (("1" (skeep -1) (("1" (mult-by -6 "ce") (("1" (mult-by -7 "cf") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (case "NOT FORALL (gg,ff,ee:Vect2): det(ff,ee)*gg = det(gg,ee)*ff - det(gg,ff)*ee") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (case "det(f,e) = 0") (("1" (lemma "parallel_det_0") (("1" (inst - "f" "e") (("1" (assert) (("1" (expand "parallel?") (("1" (skeep -1) (("1" (case "nzk > 0") (("1" (replaces -2) (("1" (mult-by -4 "nzk") (("1" (hide-all-but (-4 4)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (mult-by -4 "-nzk") (("2" (hide-all-but (-1 -5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "det(e,f) = 0") (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (name "ce" "-det(g,f)/det(f,e)") (("2" (name "cf" "det(g,e)/det(f,e)") (("2" (case "NOT g = ce*e + cf*f") (("1" (expand "ce") (("1" (expand "cf") (("1" (inst - "g" "f" "e") (("1" (decompose-equality 1) (("1" (div-by -3 "det(f,e)") (("1" (grind) nil nil)) nil) ("2" (div-by -3 "det(f,e)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "ce>=0 AND cf>0") (("1" (flatten) (("1" (inst + "ce" "cf") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "NOT det(f,e) > 0") (("1" (inst - "g" "f" "e") (("1" (case "det(g,e) > 0 AND det(g,f)<0") (("1" (flatten) (("1" (mult-by -8 "-det(g,f)") (("1" (mult-by -9 "det(g,e)") (("1" (mult-by -10 "-det(f,e)") (("1" (hide +) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (hide-all-but (-5 1)) (("1" (grind) nil nil)) nil) ("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (expand "ce" 1) (("1" (cross-mult 1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "cf" 1) (("2" (cross-mult 1) (("2" (hide-all-but (-6 1)) (("2" (grind) nil nil)) nil)) 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)) 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/") (det const-decl "real" det_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) (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) (Nz_vector type-eq-decl nil vectors_2D "vectors/") (parallel? const-decl "bool" vectors_2D "vectors/") (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (* const-decl "real" vectors_2D "vectors/") (> const-decl "bool" reals nil) (nzk skolem-const-decl "nzreal" repulsive nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (parallel_det_0 formula-decl nil parallel_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "Vector" vectors_2D "vectors/") (f skolem-const-decl "Nz_vect2" repulsive nil) (g skolem-const-decl "Nz_vect2" repulsive nil) (e skolem-const-decl "Nz_vect2" repulsive nil) (div_mult_neg_gt1 formula-decl nil extra_real_props nil) (<= const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (div_mult_neg_ge1 formula-decl nil real_props nil) (ce skolem-const-decl "real" repulsive nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_1 formula-decl nil vectors_2D "vectors/") (minus_real_is_real application-judgement "real" reals nil) (cf skolem-const-decl "real" repulsive nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (scal_assoc formula-decl nil vectors_2D "vectors/") (nzk skolem-const-decl "nzreal" repulsive nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nnreal type-eq-decl nil real_types nil) (+ const-decl "Vector" vectors_2D "vectors/") (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (ce skolem-const-decl "real" repulsive nil) (cf skolem-const-decl "real" repulsive nil) (nzk skolem-const-decl "nzreal" repulsive nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil)) shostak) (wedge_containment-1 nil 3535814052 ("" (case "FORALL (v, e, f, g, h: Vect2): sqv(g)=1 AND e * h >= 0 AND f * h > 0 AND g * h > 0 AND (NOT (det(e, g) >= 0 AND det(f, g) > 0)) AND (NOT (det(e, g) <= 0 AND det(f, g) < 0)) AND e * v >= 0 AND f * v > 0 IMPLIES g * v > 0") (("1" (skeep) (("1" (case "norm(g) > 0") (("1" (inst - "v" "e" "f" "(1/norm(g))*g" "h") (("1" (assert) (("1" (split -) (("1" (mult-by 3 "1/norm(g)") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil) ("2" (rewrite "sqv_scal") (("2" (rewrite "sq_div") (("2" (rewrite "sq_norm") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (cross-mult 1) nil nil) ("4" (flatten) (("4" (split 1) (("1" (mult-by 1 "1/norm(g)") (("1" (hide-all-but (-1 1)) (("1" (grind :exclude "norm") nil nil)) nil) ("2" (assert) (("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (mult-by 1 "1/norm(g)") (("1" (hide-all-but (-2 1)) (("1" (grind :exclude "norm") nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("5" (flatten) (("5" (split 2) (("1" (mult-by 1 "1/norm(g)") (("1" (hide-all-but (-1 1)) (("1" (grind :exclude "norm") nil nil)) nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil) ("2" (mult-by 1 "1/norm(g)") (("1" (hide-all-but (-2 1)) (("1" (grind :exclude "norm") nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (case "norm(g) = 1") (("1" (case "norm(perpR(g)) = 1") (("1" (lemma "orthonormal_basis") (("1" (inst - "g" "perpR(g)" _) (("1" (inst-cp - "e") (("1" (inst-cp - "f") (("1" (inst - "h") (("1" (assert) (("1" (case "orthonormal?(g, perpR(g))") (("1" (assert) (("1" (case "det(f,g) > 0") (("1" (assert) (("1" (hide 2) (("1" (case "det(e,g) < 0") (("1" (assert) (("1" (hide 1) (("1" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil) nil shostak)) (repulsive_criteria_transitive 0 (repulsive_criteria_transitive-1 nil 3534694896 ("" (skeep) (("" (expand "repulsive_criteria") (("" (flatten) (("" (assert) (("" (flatten) (("" (assert) (("" (split -) (("1" (flatten) (("1" (assert) (("1" (hide 6) (("1" (split -) (("1" (flatten) (("1" (assert) (("1" (lemma "wedge_containment") (("1" (inst - "-eps*perpR(v)" "s" "nv" "nw" "eps*perpR(s)") (("1" (split -) (("1" (hide-all-but (-1 5)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (flatten) (("5" (typepred "eps") (("5" (split -) (("1" (replaces -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (hide-all-but (-3 -5)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (flatten) (("6" (typepred "eps") (("6" (split -) (("1" (replaces -1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (grind) nil nil) ("8" (grind) nil nil)) nil) ("2" (flatten) (("2" (case "s+zero = -eps*perpR(eps*perpR(s))") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "wedge_containment") (("2" (inst - "-eps*perpR(v)" "s" "eps*perpR(s)" "nw" "eps*perpR(s)") (("1" (assert) (("1" (split -1) (("1" (grind) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (typepred "sqv(perpR(s))") (("3" (lemma "sqv_eq_0") (("3" (inst?) (("3" (assert) (("3" (flatten) (("3" (hide -2) (("3" (split -1) (("1" (case "s +zero = -perpR(perpR(s))") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil) ("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (grind) nil nil) ("5" (flatten) (("5" (typepred "eps") (("5" (grind) nil nil)) nil)) nil) ("6" (flatten) (("6" (typepred "eps") (("6" (grind) nil nil)) nil)) nil) ("7" (grind) nil nil) ("8" (typepred "eps") (("8" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "s+zero = -eps*(perpR(eps*perpR(s)))") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide 5) (("2" (assert) (("2" (case "NOT s*nv>=0") (("1" (ground) nil nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (lemma "wedge_containment") (("2" (inst - "-eps*perpR(v)" "s" "nv" "nw" "eps*perpR(s)") (("1" (split -) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (flatten) (("5" (typepred "eps") (("5" (split -) (("1" (replaces -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (hide-all-but (-3 -13)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (flatten) (("6" (typepred "eps") (("6" (split -) (("1" (replaces -1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (grind) nil nil) ("8" (case "NOT det(nv,v) = 0") (("1" (mult-by 1 "eps") (("1" (grind) nil nil)) nil) ("2" (lemma "parallel_det_0") (("2" (inst?) (("1" (assert) (("1" (expand "parallel?") (("1" (skeep -1) (("1" (case "nzk > 0") (("1" (replaces -2) (("1" (mult-by 2 "nzk") (("1" (grind) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (mult-by -6 "-nzk") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (hide -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "s+zero = -eps*perpR(eps*perpR(s))") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("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) ((repulsive_criteria const-decl "bool" repulsive nil) (real_lt_is_strict_total_order name-judgement "(strict_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (v skolem-const-decl "Vect2" repulsive nil) (Nz_vector type-eq-decl nil vectors_2D "vectors/") (parallel? const-decl "bool" vectors_2D "vectors/") (> const-decl "bool" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzk skolem-const-decl "nzreal" repulsive nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (int_times_even_is_even application-judgement "even_int" integers nil) (parallel_det_0 formula-decl nil parallel_2D "vectors/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (neg_zero formula-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (wedge_containment formula-decl nil repulsive nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (perpR_eq_zero formula-decl nil perpendicular_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (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) (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/") (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/") (eps skolem-const-decl "Sign" repulsive nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (perpR const-decl "Vect2" perpendicular_2D "vectors/") (s skolem-const-decl "Vect2" repulsive nil) (zero const-decl "Vector" vectors_2D "vectors/") (sign_neg_clos application-judgement "Sign" sign "reals/")) shostak)) (repulsive_criteria_transitive_odd1 0 (repulsive_criteria_transitive_odd1-2 nil 3575631768 ("" (skeep) (("" (label "thislem" -2) (("" (hide "thislem") (("" (case "NOT (s+pt*nv+px*nw)-s = pt*nv + px*nw") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (replaces -1) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (assert) (("2" (case "pt*nv=(-px)*nw") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-1 -4 -7)) (("1" (mult-by -2 "pt") (("1" (case "NOT eps*det(s,pt*nv)<0") (("1" (grind) nil nil) ("2" (hide -3) (("2" (replaces -2) (("2" (mult-by -2 "px") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pt*nv+px*nw = zero") (("1" (case "pt*nv - zero = (-px)*nw + (nw-nw)") (("1" (assert) nil nil) ("2" (replaces -1 1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (split -) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case "NOT eps*det(s,nw)<0") (("1" (mult-by -2 "pt") (("1" (grind) nil nil)) nil) ("2" (case "NOT eps * det(s, pt * nv + px * nw) < 0") (("1" (hide-all-but (-1 -8 1)) (("1" (mult-by -1 "px") (("1" (mult-by -2 "pt") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "wedge_containment") (("2" (inst - "-eps*perpR(v)" "s" "nv" "nw" "eps*perpR(s)") (("1" (split -) (("1" (mult-by -1 "px") (("1" (mult-by -9 "pt") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (grind) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (flatten) (("5" (typepred "eps") (("5" (ground) (("5" (replaces -1) (("5" (assert) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (typepred "eps") (("6" (grind) nil nil)) nil) ("7" (grind) nil nil) ("8" (grind) nil nil)) nil) ("2" (flatten) (("2" (case "s+zero = -eps*perpR(eps*perpR(s))") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (reveal "thislem") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* 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) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities 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_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) (repulsive_criteria const-decl "bool" repulsive 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) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (wedge_containment formula-decl nil repulsive nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (perpR_eq_zero formula-decl nil perpendicular_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (s skolem-const-decl "Vect2" repulsive nil) (perpR const-decl "Vect2" perpendicular_2D "vectors/") (eps skolem-const-decl "Sign" repulsive nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (* const-decl "real" vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (sub_eq_args formula-decl nil vectors_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (< const-decl "bool" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (det const-decl "real" det_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (repulsive_criteria_transitive_odd1-1 nil 3575631667 ("" (skeep) (("" (label "thislem" -2) (("" (hide "thislem") (("" (case "NOT (s+pt*nv+px*nw)-s = pt*nv + px*nw") (("1" (hide-all-but 1) (("1" (grind) nil))) ("2" (replaces -1) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (assert) (("2" (case "pt*nv=(-px)*nw") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-1 -4 -7)) (("1" (mult-by -2 "pt") (("1" (case "NOT eps*det(s,pt*nv)<0") (("1" (grind) nil) ("2" (hide -3) (("2" (replaces -2) (("2" (mult-by -2 "px") (("2" (grind) nil))))))))))))))))) ("2" (assert) (("2" (case "pt*nv+px*nw = zero") (("1" (case "pt*nv - zero = (-px)*nw + (nw-nw)") (("1" (assert) nil) ("2" (replaces -1 1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil))))))) ("2" (assert) (("2" (split -) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case "NOT eps*det(s,nw)<0") (("1" (mult-by -2 "pt") (("1" (grind) nil))) ("2" (case "NOT eps * det(s, pt * nv + px * nw) < 0") (("1" (hide-all-but (-1 -8 1)) (("1" (mult-by -1 "px") (("1" (mult-by -2 "pt") (("1" (grind) nil))))))) ("2" (assert) (("2" (lemma "wedge_containment") (("2" (inst - "-eps*perpR(v)" "s" "nv" "nw" "eps*perpR(s)") (("1" (split -) (("1" (mult-by -1 "px") (("1" (mult-by -9 "pt") (("1" (grind) nil))))) ("2" (hide-all-but (-7 1)) (("2" (grind) nil))) ("3" (grind) nil) ("4" (grind) nil) ("5" (flatten) (("5" (typepred "eps") (("5" (ground) (("5" (replaces -1) (("5" (assert) (("5" (grind) nil))))))))))) ("6" (typepred "eps") (("6" (grind) nil))) ("7" (grind) nil) ("8" (grind) nil))) ("2" (flatten) (("2" (case "s+zero = -eps*perpR(eps*perpR(s))") (("1" (replace -2) (("1" (assert) nil))) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil))))))))))))))))))))))))) ("2" (reveal "thislem") (("2" (assert) nil)))))))))))))))))))))))))))) nil) nil nil)) (rep_crit_odd2_ax 0 (rep_crit_odd2_ax-1 nil 3579945082 ("" (skeep) (("" (typepred "eps") (("" (hide -1) (("" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (metit *) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (metit *) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (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 "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_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) (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) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (repulsive_criteria_transitive_odd2 0 (repulsive_criteria_transitive_odd2-2 nil 3575649651 ("" (skeep) (("" (label "thislem" -2) (("" (hide "thislem") (("" (case "NOT (s+pt*nv+px*nw)-s = pt*nv + px*nw") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (replaces -1) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (assert) (("2" (case "pt*nv=(-px)*nw") (("1" (replace -1) (("1" (assert) (("1" (hide-all-but (-1 -4 -7)) (("1" (mult-by -2 "pt") (("1" (case "NOT eps*det(s,pt*nv)<0") (("1" (grind) nil nil) ("2" (hide -3) (("2" (replaces -2) (("2" (mult-by -2 "px") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pt*nv+px*nw = zero") (("1" (case "pt*nv - zero = (-px)*nw + (nw-nw)") (("1" (assert) nil nil) ("2" (replaces -1 1 :dir rl) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (reveal "thislem") (("2" (assert) (("2" (case "NOT eps * det(pt * nv + px * nw, v) < 0") (("1" (hide 8) (("1" (mult-by -5 "pt") (("1" (mult-by -9 "px") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "wedge_containment") (("2" (hide -1) (("2" (lemma "rep_crit_odd2_ax") (("2" (inst - "s`x" "s`y" "v`x" "v`y" "nv`x" "nv`y" "nw`x" "nw`y" "pt" "px" "eps") (("2" (assert) (("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) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "Vector" vectors_2D "vectors/") (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/") (+ const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities 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_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) (repulsive_criteria const-decl "bool" repulsive 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (rep_crit_odd2_ax formula-decl nil repulsive nil) (wedge_containment formula-decl nil repulsive nil) (* const-decl "real" vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (sub_eq_args formula-decl nil vectors_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (< const-decl "bool" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (det const-decl "real" det_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (repulsive_criteria_transitive_odd2-1 nil 3575649494 ("" (postpone) nil nil) nil shostak)) (repulsive_criteria_transitive_odd3 0 (repulsive_criteria_transitive_odd3-2 nil 3576258319 ("" (skeep) (("" (expand "repulsive_criteria") (("" (assert) (("" (case "FORALL (vv:Vect2): vv=zero IFF (vv`x = 0 AND vv`y = 0)") (("1" (case "FORALL (vv:Vect2): vv/=zero IFF (vv`x /= 0 OR vv`y /= 0)") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -2) (("1" (rewrite -2) (("1" (expand "*") (("1" (expand "det") (("1" (expand "+") (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (flatten) (("1" (hide (-1 -2)) (("1" (typepred "px") (("1" (hide -1) (("1" (typepred "eps") (("1" (split -) (("1" (replaces -1) (("1" (assert) (("1" (hide -1) (("1" (assert) (("1" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (assert) (("2" (metit *) nil nil)) nil)) nil) ("3" (assert) (("3" (metit *) nil nil)) nil) ("4" (flatten) (("4" (assert) (("4" (hide -11) (("4" (metit *) nil nil)) nil)) nil)) nil) ("5" (flatten) (("5" (assert) (("5" (metit *) nil nil)) nil)) nil) ("6" (assert) (("6" (metit *) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (assert) (("2" (metit *) nil nil)) nil)) nil) ("3" (flatten) (("3" (assert) (("3" (metit *) nil nil)) nil)) nil) ("4" (flatten) (("4" (assert) (("4" (hide -11) (("4" (assert) (("4" (metit *) nil nil)) nil)) nil)) nil)) nil) ("5" (flatten) (("5" (assert) (("5" (metit *) nil nil)) nil)) nil) ("6" (flatten) (("6" (metit *) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "zero") (("2" (grind) (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "zero") (("2" (grind) (("2" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((repulsive_criteria const-decl "bool" repulsive nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans 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) (det const-decl "real" det_2D "vectors/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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) (vx_distr_sub formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields 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) (NOT const-decl "[bool -> bool]" booleans nil) (vy_distr_sub formula-decl nil vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (* const-decl "real" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (repulsive_criteria_transitive_odd3-1 nil 3576258020 ("" (skeep) (("" (expand "repulsive_criteria") (("" (assert) (("" (flatten) (("" (case "(s + pt * nv) * nv >= 0") (("1" (assert) (("1" (case "NOT (s + pt * nv + px * nw) - s = pt*nv + px*nw") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (repulsive_criteria_sum_closed 0 (repulsive_criteria_sum_closed-1 nil 3481630626 ("" (skeep) (("" (expand "repulsive_criteria") (("" (flatten) (("" (assert) (("" (label "snz" (1 3)) (("" (hide "snz") (("" (split +) (("1" (flatten) (("1" (case "NOT nw = -nv") (("1" (hide-all-but (-1 1)) (("1" (lemma "add_zero_right") (("1" (inst - "-nv") (("1" (replace -1 :dir rl) (("1" (replace -2 :dir rl) (("1" (assert) (("1" (hide-all-but 1) (("1" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (case "NOT det(s,nv) = 0") (("1" (grind) nil nil) ("2" (replace -1) (("2" (assert) (("2" (case "s*v < 0") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (case "NOT s*nv = 0") (("1" (grind) nil nil) ("2" (lemma "orthogonal_basis") (("2" (reveal "snz") (("2" (inst - "s" "perpR(s)" "nv") (("2" (assert) (("2" (split -) (("1" (case "nv*perpR(s) = 0") (("1" (replace -1) (("1" (case "nv*s=0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil) ("2" (hide -1) (("2" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "perpR_perpR") (("2" (inst - "s") (("2" (replace -2) (("2" (assert) (("2" (case "-(-s) = zero") (("1" (assert) nil nil) ("2" (replace -1 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-3 -6)) (("2" (grind) nil nil)) nil) ("3" (flatten) (("3" (case "s*v < 0") (("1" (assert) (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((repulsive_criteria const-decl "bool" repulsive nil) (real_lt_is_strict_total_order name-judgement "(strict_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) (< const-decl "bool" 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) (det const-decl "real" det_2D "vectors/") (/= const-decl "boolean" notequal 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) (* const-decl "real" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (neg_add_right formula-decl nil vectors_2D "vectors/") (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/") (add_zero_right 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) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/")) shostak)) (repulsive_criteria_indep_of_length 0 (repulsive_criteria_indep_of_length-1 nil 3481452864 ("" (case "FORALL (eps: Sign, nv, s, v: Vect2, c: posreal): s*v<0 AND repulsive_criteria(s, v, eps)(nv) IMPLIES repulsive_criteria(s, v, eps)(c * nv)") (("1" (skeep) (("1" (skeep) (("1" (split) (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (inst - "eps" "c*nv" "s" "v" "1/c") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (assert) (("2" (ground) (("1" (lemma "scal_zero") (("1" (inst - "1/c") (("1" (replace -2 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (mult-by -3 "c") (("2" (grind) nil nil)) nil) ("3" (mult-by -4 "c") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (both_sides_times_pos_lt1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (det const-decl "real" det_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (scal_zero formula-decl nil vectors_2D "vectors/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (scal_assoc formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil) (* const-decl "Vector" vectors_2D "vectors/")) shostak)) (repulsive_criteria_repulsive 0 (repulsive_criteria_repulsive-1 nil 3481542118 ("" (skeep) (("" (case "s*v < 0") (("1" (expand "repulsive_criteria") (("1" (assert) (("1" (flatten) (("1" (hide -3) (("1" (expand "repulsive?") (("1" (case "tca(s,v) > 0") (("1" (assert) (("1" (flatten) (("1" (name "tauv" "tca(s,v)") (("1" (replace -1) (("1" (label "tauvname" -1) (("1" (name "taunv" "tca(s,nv)") (("1" (replace -1) (("1" (label "taunvname" -1) (("1" (hide 1) (("1" (name "stau" "s + tauv*v") (("1" (replace -1) (("1" (label "stauname" -1) (("1" (case "NOT orthogonal?(v,stau)") (("1" (expand "orthogonal?") (("1" (replace "stauname" :dir rl) (("1" (rewrite "dot_add_right") (("1" (case "v*s = s*v") (("1" (replace -1 1) (("1" (hide -1) (("1" (expand "tauv" 1) (("1" (expand "tca" 1) (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "horizontal_tca") (("2" (expand "sqv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "orthogonal_basis") (("2" (inst - "v" "stau" "nv") (("2" (assert) (("2" (case "v /= zero") (("1" (assert) (("1" (label "vnz" -1) (("1" (case "norm(stau) = -(1/norm(v))*(eps*det(s,v)) AND norm(eps*(s + taunv*nv)) >= (1/norm(v))*(-e (("1" (flatten) (("1" (case "norm(eps*(s + taunv*nv)) = norm(s+taunv*nv)") (("1" (case "(1 / norm(v)) * (-eps * (det(s, v) + taunv * (det(nv, v)))) > (1 / norm(v)) * (-eps * det(s, v))") (("1" (assert) nil nil) ("2" (assert) (("2" (case "taunv/norm(v) > 0") (("1" (assert) (("1" (mult-by -13 "(1/norm(v))*taunv") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (ground) (("1" (lemma "norm_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "norm_scal") (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "norm_scal" 1) (("2" (case "abs(eps) = 1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (lemma "orthogonal_basis") (("1" (inst - "v" "perpR(v)" "stau") (("1" (assert) (("1" (case "perpR(v) /= zero AND orthogonal?(v, perpR(v))") (("1" (flatten) (("1" (assert) (("1" (case "stau*v = 0") (("1" (replace -1) (("1" (assert) (("1" (case "stau*perpR(v) = det(s,v)") (("1" (replace -1) (("1" (replace -4 2) (("1" (rewrite "norm_scal") (("1" (rewrite "abs_div") (("1" (case "abs(sqv(perpR(v))) = sqv(perpR(v))") (("1" (replace -1) (("1" (hide -1) (("1" (case "-eps*det(s,v) = abs(det(s,v))") (("1" (case "norm(perpR(v))/sqv(perpR(v)) = 1/norm(v)") (("1" (mult-by -1 "abs(det(s,v))") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (case "norm(perpR(v)) = norm(v)") (("1" (replace -1) (("1" (case "sqv(perpR(v)) = sqv(v)") (("1" (replace -1) (("1" (lemma "sqrt_sqv_norm") (("1" (inst - "v") (("1" (lemma "sq_eq") (("1" (inst - "sqrt(sqv(v))" "norm(v)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-12 1)) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "stau" 1) (("2" (rewrite "dot_add_left") (("2" (hide-all-but 1) (("2" (grind :exclude "tauv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "stau" 1) (("2" (expand "tauv" 1) (("2" (expand "tca" 1) (("2" (expand "horizontal_tca" 1) (("2" (rewrite "dot_add_left") (("2" (expand "sqv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (hide-all-but ("vnz" 1)) (("1" (flatten) (("1" (case "v = -perpR(perpR(v))") (("1" (replace -1 +) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "norm_scal") (("2" (case "abs(eps) = 1") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sq_ge") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case "sq(det(s, v) * (1 / norm(v)) * -eps + (det(nv, v)) * (1 / norm(v)) * -eps * taunv) = sq(det(s, v) * (1 / norm(v)) + (det(nv, v)) * (1 / norm(v)) * taunv)") (("1" (replace -1) (("1" (hide -1) (("1" (case "sq(det(s, v) * (1 / norm(v)) + (det(nv, v)) * (1 / norm(v)) * taunv) = (1/sqv(v))*sq(det(s + taun (("1" (case "sq(det(s, v) * (1 / norm(v)) + (det(nv, v)) * (1 / norm(v)) * taunv) = (1/sqv(v))*sq(det(s + taun (("1" (replace -1) (("1" (hide -1) (("1" (case "sq(1 * norm((s + taunv * nv))) = sqv(s+taunv*nv)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "orthogonal_basis") (("1" (inst - "perpR(v)" "v" "s + taunv*nv") (("1" (assert) (("1" (case "perpR(v) /= zero AND orthogonal?(perpR(v), v)") (("1" (flatten) (("1" (assert) (("1" (lemma "orthogonal_basis_sqv") (("1" (inst - "(((s + taunv * nv) * perpR(v)) / sqv(perpR(v)))" "(((s + taunv * nv) * v) / sqv(v))" "perpR(v)" "v" "s + taunv*nv") (("1" (assert) (("1" (replace -1 +) (("1" (case "sq((((s + taunv * nv) * perpR(v)) / sqv(perpR(v)))) * sqv(perpR(v)) >= (1 / sqv(v)) * sq(det(s + taunv * nv, v))") (("1" (assert) nil nil) ("2" (hide 3) (("2" (case "(s + taunv * nv) * perpR(v) = det(s + taunv*nv,v)") (("1" (replace -1) (("1" (case "sqv(perpR(v)) = sqv(v)") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sq_div") (("1" (expand "sq") (("1" (assert) nil nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind :exclude ("taunv")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (flatten) (("1" (hide-all-but (-1 "vnz")) (("1" (expand "zero") (("1" (decompose-equality) (("1" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqrt_sqv_norm") (("2" (inst?) (("2" (replace -1 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (case "sqv(v) = sq(norm(v))") (("1" (replace -1 1) (("1" (cross-mult 1) (("1" (hide 2) (("1" (rewrite "sq_times" :dir rl) (("1" (name "const1" "norm(v)") (("1" (replace -1) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqrt_sqv_norm") (("2" (inst - "v") (("2" (replace -1 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-1 1)) (("3" (lemma "sqv_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (expand "sq") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (mult-by -9 "eps/norm(v)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (lemma "norm_eq_0") (("3" (inst - "v") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (lemma "norm_eq_0") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (hide-all-but -10) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "tca" 1) (("2" (case "v /= zero") (("1" (assert) (("1" (expand "horizontal_tca") (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "sqv_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "repulsive?") (("2" (assert) (("2" (expand "repulsive_criteria") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((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 "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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (> const-decl "bool" reals nil) (tca const-decl "real" repulsive nil) (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (orthogonal_basis formula-decl nil basis_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (det const-decl "real" det_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (norm const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (norm_eq_0 formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (norm_scal formula-decl nil vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_gt1 formula-decl nil extra_real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_ge formula-decl nil sq "reals/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (sq const-decl "nonneg_real" sq "reals/") (times_div1 formula-decl nil real_props nil) (sq_times formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (orthogonal_basis_sqv formula-decl nil basis_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (sq_div formula-decl nil sq "reals/") (taunv skolem-const-decl "real" repulsive nil) (nv skolem-const-decl "Vect2" repulsive nil) (eps skolem-const-decl "Sign" repulsive nil) (v skolem-const-decl "Vect2" repulsive nil) (s skolem-const-decl "Vect2" repulsive nil) (perpR_eq_zero formula-decl nil perpendicular_2D "vectors/") (neg_zero formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_left formula-decl nil vectors_2D "vectors/") (stau skolem-const-decl "Vector" repulsive nil) (dot_scal_left formula-decl nil vectors_2D "vectors/") (dot_add_left formula-decl nil vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (sq_eq formula-decl nil sq "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (div_cancel4 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (abs_div formula-decl nil real_props nil) (perpR const-decl "Vect2" perpendicular_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (dot_add_right formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (tauv skolem-const-decl "real" repulsive nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (dot_zero_left formula-decl nil vectors_2D "vectors/") (orthogonal? const-decl "bool" vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (sqv_zero formula-decl nil vectors_2D "vectors/") (repulsive? const-decl "bool" repulsive nil) (repulsive_criteria const-decl "bool" repulsive nil)) shostak)) (repulsive_criteria_repulsive2 0 (repulsive_criteria_repulsive2-2 nil 3563190474 ("" (case "FORALL (eps: Sign, nv, s, v: Vect2): norm(nv)=1 AND norm(s)=1 AND norm(v)=1 AND s*v<0 AND repulsive?(s, v)(nv) AND eps * det(s, v) <= 0 AND eps * det(s, nv) < 0 AND nv /= zero AND (s * v >= 0 IMPLIES eps * det(nv, v) <= 0) IMPLIES repulsive_criteria(s, v, eps)(nv)") (("1" (skeep) (("1" (case "s*v<0") (("1" (case "s = zero OR v = zero") (("1" (split -1) (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -6) (("2" (name "ss" "^(s)") (("2" (name "vv" "^(v)") (("2" (name "nvv" "^(nv)") (("2" (lemma "norm_eq_0") (("2" (inst-cp - "s") (("2" (inst-cp - "v") (("2" (inst - "nv") (("2" (assert) (("2" (inst - "eps" "nvv" "ss" "vv") (("2" (assert) (("2" (split -) (("1" (expand "repulsive_criteria") (("1" (flatten) (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (hide-all-but (-2 9)) (("1" (mult-by 1 "(1/norm(nv))*(1/norm(v))") (("1" (expand "nvv") (("1" (expand "vv") (("1" (grind) nil nil)) nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide-all-but (-1 -10)) (("2" (mult-by -2 "(1/norm(s))*(1/norm(v))") (("1" (expand "vv") (("1" (expand "ss") (("1" (grind :exclude "norm") nil nil)) nil)) nil) ("2" (case "FORALL (aa:real): aa>0 IMPLIES (aa>=0 AND aa>0)") (("1" (rewrite -1) (("1" (cross-mult 1) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 1)) (("2" (expand "ss") (("2" (expand "vv") (("2" (mult-by -1 "(1/norm(s))*(1/norm(v))") (("1" (grind :exclude "norm") nil nil) ("2" (case "FORALL (aa:real): aa>0 IMPLIES (aa>=0 AND aa>0)") (("1" (rewrite -1) (("1" (cross-mult 1) nil nil)) nil) ("2" (grind :exclude "norm") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "repulsive?") (("3" (flatten) (("3" (hide 2) (("3" (case "NOT ss*vv<0") (("1" (hide-all-but (-4 1)) (("1" (mult-by -1 "(1/norm(s))*(1/norm(v))") (("1" (expand "ss") (("1" (expand "vv") (("1" (grind :exclude "norm") nil nil)) nil)) nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (split -) (("1" (expand "tca") (("1" (assert) (("1" (case "nvv = zero") (("1" (assert) nil nil) ("2" (assert) (("2" (hide 3) (("2" (expand "horizontal_tca") (("2" (cross-mult -1) (("2" (split -) (("1" (flatten) (("1" (cross-mult 2) (("1" (hide-all-but (-2 2)) (("1" (expand "ss") (("1" (expand "nvv") (("1" (mult-by -1 "(1/norm(s))*(1/norm(nv))") (("1" (grind :exclude "norm") nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_lt") (("2" (inst?) (("2" (assert) (("2" (rewrite "sq_norm") (("2" (rewrite "sq_norm") (("2" (lemma "sq_lt") (("2" (inst - "norm(ss + tca(ss, vv) * vv)" "norm(ss + tca(ss, nvv) * nvv)") (("2" (assert) (("2" (rewrite "sq_norm") (("2" (rewrite "sq_norm") (("2" (hide 3) (("2" (hide -2) (("2" (expand "tca") (("2" (case "vv = zero") (("1" (assert) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case "nvv = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("2" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("2" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("2" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("2" (expand "horizontal_sq_dtca") (("2" (expand "ss") (("2" (expand "vv") (("2" (expand "nvv") (("2" (expand "^" 3) (("2" (rewrite "det_scal_left") (("2" (rewrite "det_scal_left") (("2" (rewrite "det_scal_right") (("2" (rewrite "det_scal_right") (("2" (assert) (("2" (rewrite "sqv_scal") (("2" (rewrite "sqv_scal") (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (assert) (("2" (mult-by -1 "sq(1/norm(s))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "ss") (("4" (expand "vv") (("4" (mult-by -6 "(1/norm(s))*(1/norm(v))") (("1" (grind :exclude "norm") nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("5" (expand "nvv") (("5" (expand "ss") (("5" (mult-by -7 "(1/norm(s))*(1/norm(nv))") (("1" (grind :exclude "norm") nil nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("6" (flatten) (("6" (replace -1) (("6" (assert) (("6" (typepred "^(nv)") (("6" (replace -3) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("7" (hide -1) (("7" (flatten) (("7" (hide-all-but (-1 -4)) (("7" (expand "vv") (("7" (expand "ss") (("7" (mult-by -2 "(1/norm(s))*(1/norm(v))") (("1" (grind :exclude "norm") nil nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("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) ("2" (hide -1) (("2" (expand "repulsive?") (("2" (assert) (("2" (expand "repulsive_criteria") (("2" (case "s = zero") (("1" (replaces -1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "repulsive_criteria") (("2" (assert) (("2" (case "s = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (case "v = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide -8) (("2" (assert) (("2" (expand "repulsive?") (("2" (case "tca(s,v) > 0") (("1" (assert) (("1" (case "s*nv>=0") (("1" (hide -7) (("1" (lemma "wedge_containment") (("1" (inst - "-eps*perpR(v)" "s" "eps*perpR(s)" "nv" "eps*perpR(s)") (("1" (assert) (("1" (split -1) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (case "sqv(perpR(s))>0") (("1" (hide-all-but (-1 1)) (("1" (typepred "eps") (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) (("2" (case "s+zero = -perpR(perpR(s))") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (grind) nil nil) ("5" (flatten) (("5" (typepred "eps") (("5" (grind) nil nil)) nil)) nil) ("6" (typepred "eps") (("6" (grind) nil nil)) nil) ("7" (grind) nil nil) ("8" (typepred "eps") (("8" (grind) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "s+zero = -eps*(perpR(eps*perpR(s)))") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) (("2" (case "tca(s, nv) <= 0") (("1" (expand "tca" -1) (("1" (expand "horizontal_tca") (("1" (cross-mult -1) (("1" (ground) (("1" (lemma "sqv_eq_0") (("1" (inst - "nv") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst - "nv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "tca") (("2" (assert) (("2" (lemma "sq_lt") (("2" (inst - "norm(s + horizontal_tca(s, v) * v)" " norm(s + horizontal_tca(s, nv) * nv)") (("2" (assert) (("2" (rewrite "sq_norm") (("2" (rewrite "sq_norm") (("2" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("2" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("2" (expand "horizontal_sq_dtca") (("2" (lemma "sq_norm") (("2" (inst-cp - "v") (("2" (inst - "nv") (("2" (replace -5) (("2" (replace -7) (("2" (assert) (("2" (replace -2 :dir rl) (("2" (replace -1 :dir rl) (("2" (assert) (("2" (case "NOT FORALL (aaaaa:real):aaaaa/1 = aaaaa") (("1" (assert) nil nil) ("2" (rewrite -1) (("2" (rewrite -1) (("2" (hide -1) (("2" (case "NOT norm(perpR(s)) = 1") (("1" (grind) nil nil) ("2" (lemma "orthonormal_basis") (("2" (case "perpR(s) = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (name "sw" "perpR(s)") (("2" (inst - "s" "sw" _) (("2" (case "NOT orthonormal?(s,sw)") (("1" (expand "orthonormal?") (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "sw") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst-cp - "v") (("2" (inst - "nv") (("2" (lemma "basis_sqv") (("2" (inst-cp - "s" "sw" "v*s" "v*sw" "v") (("2" (inst - "s" "sw" "nv*s" "nv*sw" "nv") (("2" (assert) (("2" (replace -8 :dir rl) (("2" (replace -9 :dir rl) (("2" (case "NOT sq(s*v)>sq(s*nv)") (("1" (hide-all-but (-1 -2 -10 1)) (("1" (expand "sw") (("1" (grind) nil nil)) nil)) nil) ("2" (lemma "orthonormal_basis") (("2" (inst - "s" "sw" _) (("2" (assert) (("2" (inst - "perpR(nv)") (("2" (lemma "basis_dot") (("2" (inst - "s" "sw" "v*s" "v*sw" "perpR(nv)*s" "perpR(nv)*sw") (("2" (assert) (("2" (replace -9 :dir rl) (("2" (replace -2 :dir rl) (("2" (rewrite "det_perpR" :dir rl) (("2" (mult-by -1 "-eps") (("2" (rewrite "det_asym") (("2" (assert) (("2" (replace -1) (("2" (case "NOT perpR(nv)*sw = (s*nv)") (("1" (hide-all-but 1) (("1" (expand "sw") (("1" (grind) nil nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (case "NOT (v*sw)*-eps = eps*det(s,v)") (("1" (hide-all-but 1) (("1" (expand "sw") (("1" (grind) nil nil)) nil)) nil) ("2" (mult-by -1 "s*nv") (("2" (replaces -1) (("2" (case "NOT perpR(nv)*s = det(s,nv)") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (replaces -1) (("2" (case "FORALL (an1:negreal,an2:npreal,ap1,ap2:posreal): an1<an2 AND ap1>ap2 IMPLIES an1*ap1<an2 (("1" (inst - "eps*det(s,nv)" "eps*det(s,v)" "-(v*s)" "-(s*nv)") (("1" (assert) (("1" (hide (-1 -2)) (("1" (split +) (("1" (lemma "sqrt_lt") (("1" (inst - "sq(det(s,v))" "sq(det(s,nv))") (("1" (assert) (("1" (lemma "sqrt_sq_abs") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (hide -1) (("1" (typepred "eps") (("1" (expand "abs") (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqrt_lt") (("2" (inst - "sq(s*nv)" "sq(s*v)") (("2" (assert) (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "dot_comm") (("2" (rewrite -1 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (typepred "ap1") (("2" (hide -1) (("2" (typepred "ap2") (("2" (hide -1) (("2" (typepred "an1") (("2" (hide -1) (("2" (typepred "an2") (("2" (neg-formula -5) (("2" (mult-ineq -5 -6) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "tca" 1) (("2" (expand "horizontal_tca") (("2" (cross-mult 1) (("2" (ground) (("1" (lemma "sqv_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((wedge_containment formula-decl nil repulsive nil) (scal_zero formula-decl nil vectors_2D "vectors/") (dot_scal_right formula-decl nil vectors_2D "vectors/") (dot_scal_left formula-decl nil vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "Vector" vectors_2D "vectors/") (perpR_eq_zero formula-decl nil perpendicular_2D "vectors/") (neg_zero formula-decl nil vectors_2D "vectors/") (s skolem-const-decl "Vect2" repulsive nil) (perpR const-decl "Vect2" perpendicular_2D "vectors/") (eps skolem-const-decl "Sign" repulsive nil) (sign_neg_clos application-judgement "Sign" sign "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (orthonormal_basis formula-decl nil basis_2D "vectors/") (orthonormal? const-decl "bool" basis_2D "vectors/") (sw skolem-const-decl "Vect2" repulsive nil) (orthogonal? const-decl "bool" vectors_2D "vectors/") (basis_sqv formula-decl nil basis_2D "vectors/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (det_perpR formula-decl nil det_2D "vectors/") (det_asym formula-decl nil det_2D "vectors/") (lt_times_lt_any1 formula-decl nil extra_real_props nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (mult_neg formula-decl nil extra_tegies nil) (v skolem-const-decl "Vect2" repulsive nil) (sqrt_sq_neg formula-decl nil sqrt "reals/") (sqrt_lt formula-decl nil sqrt "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sqrt_sq_abs formula-decl nil sqrt "reals/") (dot_comm formula-decl nil vectors_2D "vectors/") (npreal type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (basis_dot formula-decl nil basis_2D "vectors/") (sq_1 formula-decl nil sq "reals/") (div_mult_pos_neg_gt1 formula-decl nil extra_real_props nil) (comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dot_zero_left formula-decl nil vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Nz_vector type-eq-decl nil vectors_2D "vectors/") (Normalized type-eq-decl nil vectors_2D "vectors/") (^ const-decl "Normalized" vectors_2D "vectors/") (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div1 formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nvv skolem-const-decl "Normalized" repulsive nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (vv skolem-const-decl "Normalized" repulsive nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nv skolem-const-decl "Vect2" repulsive nil) (v skolem-const-decl "Vect2" repulsive nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (ss skolem-const-decl "Normalized" repulsive nil) (s skolem-const-decl "Vect2" repulsive nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (sq_lt formula-decl nil sq "reals/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (horizontal_sq_dtca_eq formula-decl nil definitions nil) (horizontal_sq_dtca const-decl "real" definitions nil) (sqv_scal formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_times formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (det_scal_right formula-decl nil det_2D "vectors/") (det_scal_left formula-decl nil det_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (sq_norm formula-decl nil vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (tca const-decl "real" repulsive nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil) (minus_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/") (div_mult_pos_le1 formula-decl nil real_props nil) (horizontal_tca const-decl "real" definitions nil) (norm_zero formula-decl nil vectors_2D "vectors/") (nz_norm_gt_0 application-judgement "posreal" vectors_2D "vectors/") (norm_eq_0 formula-decl nil vectors_2D "vectors/") (real_times_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) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal 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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (< const-decl "bool" reals nil) (* const-decl "real" vectors_2D "vectors/") (repulsive? const-decl "bool" repulsive nil) (<= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (det const-decl "real" det_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil)) nil) (repulsive_criteria_repulsive2-1 nil 3563190216 ("" (skeep) (("" (case "s*v < 0") (("1" (expand "repulsive_criteria") (("1" (assert) (("1" (case "s = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "repulsive?") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil) nil nil)) (repulsive_criteria_symmetric 0 (repulsive_criteria_symmetric-1 nil 3481629993 ("" (case "FORALL (eps: Sign, nv, s, v: Vect2): repulsive_criteria(s, v, eps)(nv) IMPLIES repulsive_criteria(-s, -v, eps)(-nv)") (("1" (skeep) (("1" (inst-cp - "eps" "nv" "s" "v") (("1" (inst - "eps" "-nv" "-s" "-v") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "repulsive_criteria") (("2" (flatten) (("2" (case "s*v >= 0") (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (case "v = zero") (("1" (replace -1) (("1" (assert) (("1" (ground) (("1" (case "-(-s) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (case "-(-nv) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (hide-all-but 1) (("6" (grind) nil nil)) nil) ("7" (case "-(-s) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("8" (case "-(-nv) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("9" (hide-all-but 1) (("9" (grind) nil nil)) nil) ("10" (grind) nil nil) ("11" (grind) nil nil) ("12" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -4) (("2" (case "-s*-v>=0") (("1" (assert) (("1" (case "-v/=zero") (("1" (assert) (("1" (ground) (("1" (case "-(-s) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (case "-(-nv) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "-(-v) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 5) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "-s*-v < 0") (("1" (assert) (("1" (ground) (("1" (case "-(-s) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("2" (case "-(-nv) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil)) nil)) nil) ("2" (hide 5) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((>= const-decl "bool" reals nil) (* const-decl "real" vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (neg_zero formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (neg_neg formula-decl nil vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (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/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (repulsive_criteria const-decl "bool" repulsive nil) (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/")) shostak)) (repulsive_criteria_coordinately_repulsive 0 (repulsive_criteria_coordinately_repulsive-3 "" 3560258967 ("" (skeep) (("" (case "vo-vi = zero") (("1" (replace -1) (("1" (expand "repulsive_criteria" -2) (("1" (assert) (("1" (expand "repulsive?" +) (("1" (assert) (("1" (case "vi-vo = zero") (("1" (replace -1) (("1" (expand "repulsive_criteria") (("1" (assert) (("1" (case "vo = vi") (("1" (replace -1) (("1" (hide (-1 -2 -3)) (("1" (grind) nil nil)) nil)) nil) ("2" (case "vo+zero = vi + (vo-vi)") (("1" (replace -3) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "-zero = zero") (("1" (replace -1 1 :dir rl) (("1" (replace -2 + :dir rl) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "vovinz" 1) (("2" (name "crit" "LAMBDA (sss: Vect2,v:Vect2): (LAMBDA (nv:Vect2): sss*v<0 AND repulsive_criteria(sss,v,e (("2" (name "conf" "LAMBDA (sss:Vect2,v:Vect2): (LAMBDA (nv:Vect2): sss*v<0 AND NOT repulsive?(sss,v)(nv))" (("2" (case "s*(vo-vi)<0") (("1" (lemma "sum_indep_coordinated_2D") (("1" (inst - "conf" "crit") (("1" (split -) (("1" (expand "coordinated_2D?") (("1" (inst - "vo" "vi" "nvo" "nvi" "s") (("1" (split -) (("1" (expand "conf" +) (("1" (assert) nil nil)) nil) ("2" (expand "conf" +) (("2" (assert) (("2" (expand "repulsive?" -1) (("2" (hide-all-but (-1 -2 1)) (("2" (expand "tca") (("2" (expand "horizontal_tca") (("2" (cross-mult -1) (("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "crit" +) (("3" (assert) nil nil)) nil) ("4" (expand "crit" +) (("4" (assert) (("4" (hide-all-but (-1 1)) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "crit_symmetric_2D?") (("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "crit") (("2" (lemma "repulsive_criteria_symmetric") (("2" (inst - "eps" "nv!1" "s!1" "v!1") (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (assert) (("2" (ground) (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "sum_independent_2D?") (("3" (skosimp*) (("3" (expand "crit") (("3" (flatten) (("3" (lemma "repulsive_criteria_sum_closed") (("3" (inst - "eps" "nv!1" "nw!1" "s!1" "v!1") (("3" (assert) (("3" (expand "conf" -7) (("3" (lemma "repulsive_criteria_repulsive") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "sum_closed_2D?") (("4" (skosimp*) (("4" (expand "conf") (("4" (flatten) (("4" (assert) (("4" (lemma "not_repulsive_sum_closed") (("4" (expand "sum_closed_2D?") (("4" (inst - "s!1" "v!1" "nv!1" "nw!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2)) (("2" (expand "repulsive_criteria") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (split -) (("1" (flatten) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "repulsive?") (("2" (assert) (("2" (case "NOT vi-vo=zero") (("1" (assert) (("1" (hide -2) (("1" (grind) nil nil)) nil)) nil) ("2" (case "-(vo-vi) = zero") (("1" (assert) (("1" (case "-(-(vo-vi)) = zero") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (repulsive_criteria const-decl "bool" repulsive nil) (repulsive? const-decl "bool" repulsive nil) (/= const-decl "boolean" notequal nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (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) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (neg_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (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) (dot_zero_right formula-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) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Criter type-eq-decl nil predicate_coordination_2D nil) (Vector_Predicate nonempty-type-eq-decl nil predicate_coordination_2D nil) (set type-eq-decl nil sets nil) (not_repulsive_sum_closed formula-decl nil repulsive nil) (sum_closed_2D? const-decl "bool" predicate_coordination_2D nil) (repulsive_criteria_repulsive formula-decl nil repulsive nil) (repulsive_criteria_sum_closed formula-decl nil repulsive nil) (sum_independent_2D? const-decl "bool" predicate_coordination_2D nil) (crit_symmetric_2D? const-decl "bool" predicate_coordination_2D nil) (repulsive_criteria_symmetric formula-decl nil repulsive nil) (coordinated_2D? const-decl "bool" predicate_coordination_2D nil) (conf skolem-const-decl "[[Vect2, Vect2] -> [Vect2 -> boolean]]" repulsive nil) (horizontal_tca const-decl "real" definitions nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (tca const-decl "real" repulsive nil) (crit skolem-const-decl "[[Vect2, Vect2] -> [Vect2 -> boolean]]" repulsive nil) (sum_indep_coordinated_2D formula-decl nil predicate_coordination_2D nil) (neg_neg formula-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil)) nil) (repulsive_criteria_coordinately_repulsive-2 "" 3505031535 ("" (skeep) (("" (case "vo-vi = zero") (("1" (replace -1) (("1" (case "vo = vi") (("1" (replace -1) (("1" (assert) (("1" (expand "repulsive_criteria") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "det_zero_right") (("1" (rewrite "det_zero_right") (("1" (assert) (("1" (expand "repulsive?") (("1" (assert) (("1" (ground) (("1" (case "nvo = nvi") (("1" (replace -1) (("1" (assert) (("1" (lemma "orthogonal_basis") (("1" (inst - "s" "perpR(s)" "nvi-vi") (("1" (assert) (("1" (split -) (("1" (case "(nvi-vi)*s = 0") (("1" (replace -1) (("1" (assert) (("1" (case "(nvi-vi)*perpR(s) = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "eps") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "perpR_perpR") (("2" (inst - "s") (("2" (replace -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "nvo+zero = nvi + (nvo-nvi)") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "vo+zero = vi + (vo-vi)") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (label "vovinz" 1) (("2" (name "crit" "LAMBDA (sss: Vect2,v:Vect2): (LAMBDA (nv:Vect2): sss*v<0 AND repulsive_criteria(sss,v,e (("2" (name "conf" "LAMBDA (sss:Vect2,v:Vect2): (LAMBDA (nv:Vect2): sss*v<0 AND NOT repulsive?(sss,v)(nv))" (("2" (case "s*(vo-vi)<0") (("1" (lemma "sum_indep_coordinated_2D") (("1" (inst - "conf" "crit") (("1" (split -) (("1" (expand "coordinated_2D?") (("1" (inst - "vo" "vi" "nvo" "nvi" "s") (("1" (split -) (("1" (expand "conf" +) (("1" (assert) nil nil)) nil) ("2" (expand "conf" +) (("2" (assert) (("2" (expand "repulsive?" -1) (("2" (hide-all-but (-1 -2 1)) (("2" (expand "tca") (("2" (expand "horizontal_tca") (("2" (cross-mult -1) (("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "crit" +) (("3" (assert) nil nil)) nil) ("4" (expand "crit" +) (("4" (assert) (("4" (hide-all-but (-1 1)) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "crit_symmetric_2D?") (("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "crit") (("2" (lemma "repulsive_criteria_symmetric") (("2" (inst - "eps" "nv!1" "s!1" "v!1") (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (assert) (("2" (ground) (("1" (hide -2) (("1" (grind) nil nil)) nil) ("2" (hide -2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "sum_independent_2D?") (("3" (skosimp*) (("3" (expand "crit") (("3" (flatten) (("3" (lemma "repulsive_criteria_sum_closed") (("3" (inst - "eps" "nv!1" "nw!1" "s!1" "v!1") (("3" (assert) (("3" (expand "conf" -7) (("3" (lemma "repulsive_criteria_repulsive") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "sum_closed_2D?") (("4" (skosimp*) (("4" (expand "conf") (("4" (flatten) (("4" (assert) (("4" (lemma "not_repulsive_sum_closed") (("4" (expand "sum_closed_2D?") (("4" (inst - "s!1" "v!1" "nv!1" "nw!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "nvo = nvi") (("1" (replace -1) (("1" (hide (-2 -3)) (("1" (expand "repulsive_criteria") (("1" (flatten) (("1" (assert) (("1" (expand "repulsive?") (("1" (assert) (("1" (case "-s*(vi-vo)>=0") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (neg_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (dot_zero_right formula-decl nil vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (Criter type-eq-decl nil predicate_coordination_2D nil) (Vector_Predicate nonempty-type-eq-decl nil predicate_coordination_2D nil) (sum_closed_2D? const-decl "bool" predicate_coordination_2D nil) (sum_independent_2D? const-decl "bool" predicate_coordination_2D nil) (crit_symmetric_2D? const-decl "bool" predicate_coordination_2D nil) (coordinated_2D? const-decl "bool" predicate_coordination_2D nil) (horizontal_tca const-decl "real" definitions nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (sum_indep_coordinated_2D formula-decl nil predicate_coordination_2D nil)) shostak) (repulsive_criteria_coordinately_repulsive-1 nil 3481630204 ("" (skeep) (("" (case "vo-vi = zero") (("1" (replace -1) (("1" (expand "horizontal_conflict?") (("1" (assert) nil nil)) nil)) nil) ("2" (label "vovinz" 1) (("2" (name "crit" "LAMBDA (sss: Vect2,v:Vect2): (LAMBDA (nv:Vect2): IF sqv(sss)<sq(D) OR sss + tca(sss,v)*v = z (("1" (name "conf" "LAMBDA (sss:Vect2,v:Vect2): (LAMBDA (nv:Vect2): IF sqv(sss)<sq(D) OR sss + tca(sss,v)*v = z (("1" (lemma "sum_indep_coordinated_2D") (("1" (inst - "conf" "crit") (("1" (split -) (("1" (expand "coordinated_2D?") (("1" (inst - "vo" "vi" "nvo" "nvi" "s") (("1" (split -) (("1" (expand "conf" +) (("1" (assert) nil nil)) nil) ("2" (expand "conf" +) (("2" (assert) (("2" (expand "repulsive?" -) (("2" (expand "repulsive?" +) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "crit" +) (("3" (assert) nil nil)) nil) ("4" (expand "crit" +) (("4" (assert) (("4" (ground) (("1" (hide-all-but (-1 2)) (("1" (case "tca(-s,vi-vo) = tca(s,vo-vi)") (("1" (replace -1) (("1" (hide -1) (("1" (name "tttz" "tca(s,vo-vi)") (("1" (replace -1) (("1" (hide -1) (("1" (expand "zero") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "tca") (("2" (lift-if) (("2" (ground) (("1" (case "vo-vi=zero") (("1" (replace -1) (("1" (case "s = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "zero") (("2" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (hide -1) (("2" (expand "horizontal_tca") (("2" (name "cv1" "sqv(vi-vo)") (("2" (replace -1) (("2" (case "sqv(vo-vi) = cv1") (("1" (replace -1) (("1" (hide-all-but 3) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "horizontal_conflict?") (("2" (skosimp*) (("2" (inst + "nnt!1") (("2" (hide-all-but (-3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "crit_symmetric_2D?") (("2" (skosimp*) (("2" (expand "crit" +) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (hide-all-but (-3 2)) (("1" (expand "zero") (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (-1 3)) (("2" (expand "horizontal_conflict?") (("2" (skosimp*) (("2" (inst?) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-1 2)) (("3" (expand "zero") (("3" (expand "tca") (("3" (lift-if) (("3" (expand "zero") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-2 1)) (("4" (expand "horizontal_conflict?") (("4" (skosimp*) (("4" (inst?) (("4" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (lemma "repulsive_criteria_symmetric") (("5" (inst?) (("5" (assert) nil nil)) nil)) nil) ("6" (lemma "repulsive_criteria_symmetric") (("6" (inst?) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sum_independent_2D?") (("3" (skosimp*) (("3" (expand "crit" (-1 -2 -3 -4)) (("3" (expand "conf" (-1 -2 -3 -4)) (("3" (assert) (("3" (ground) (("3" (lemma "repulsive_criteria_sum_closed") (("3" (inst - "eps" "nv!1" "nw!1" "s!1" "v!1") (("3" (assert) (("3" (lemma "repulsive_criteria_repulsive") (("3" (inst - "eps" "nv!1+nw!1" "s!1" "v!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "sum_closed_2D?") (("4" (skosimp*) (("4" (expand "conf") (("4" (ground) (("4" (lemma "not_repulsive_sum_closed") (("4" (expand "sum_closed_2D?") (("4" (inst - "s!1" "v!1" "nv!1" "nw!1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (horizontal_conflict? const-decl "bool" horizontal nil) (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (Sign type-eq-decl nil sign "reals/") (Sp_vect2 type-eq-decl nil horizontal nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (sq const-decl "nonneg_real" sq "reals/") (sqv const-decl "nnreal" vectors_2D "vectors/") (sum_indep_coordinated_2D formula-decl nil predicate_coordination_2D nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (* const-decl "real" vectors_2D "vectors/") (scal_0 formula-decl nil vectors_2D "vectors/") (sqv_neg formula-decl nil vectors_2D "vectors/") (sq_nz_pos application-judgement "posreal" sq "reals/") (coordinated_2D? const-decl "bool" predicate_coordination_2D nil) (neg_neg formula-decl nil vectors_2D "vectors/") (crit_symmetric_2D? const-decl "bool" predicate_coordination_2D nil) (sum_independent_2D? const-decl "bool" predicate_coordination_2D nil) (sum_closed_2D? const-decl "bool" predicate_coordination_2D nil) (Vector_Predicate nonempty-type-eq-decl nil predicate_coordination_2D nil) (Criter type-eq-decl nil predicate_coordination_2D nil)) shostak)) (foo 0 (foo-2 nil 3600444212 ("" (skeep) (("" (case "vo-vi = zero") (("1" (replace -1) (("1" (expand "repulsive_criteria" -2) (("1" (assert) (("1" (expand "repulsive?" +) (("1" (assert) (("1" (case "vi-vo = zero") (("1" (replace -1) (("1" (expand "repulsive_criteria") (("1" (assert) (("1" (case "vo = vi") (("1" (replace -1) (("1" (hide (-1 -2 -3)) (("1" (grind) nil nil)) nil)) nil) ("2" (case "vo+zero = vi + (vo-vi)") (("1" (replace -3) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "-zero = zero") (("1" (replace -1 1 :dir rl) (("1" (replace -2 + :dir rl) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "vovinz" 1) (("2" (expand "repulsive?") (("2" (flatten) (("2" (case "NOT ((s * (vo - vi) < 0 AND (tca(s, nvo - nvi) <= 0 OR norm(s + tca(s, vo - vi) * (vo - vi)) < norm(s + tca(s, nvo - nvi) * (nvo - nvi)))) IFF (s * (vo - vi) < 0 AND (s*(nvo-nvi)>=0 OR sq(det(s,vo-vi))*sqv(nvo-nvi) <sq(det(s,nvo-nvi))*sqv(vo-vi) )))") (("1" (hide (3 4)) (("1" (expand "tca" 1) (("1" (assert) (("1" (case "nvo - nvi = zero") (("1" (assert) (("1" (replaces -1) (("1" (ground) nil nil)) nil)) nil) ("2" (assert) (("2" (hide -) (("2" (case "norm(s + horizontal_tca(s, vo - vi) * (vo - vi)) < norm(s + horizontal_tca(s, nvo - nvi) * (nvo - nvi)) IFF sqv(s + horizontal_tca(s, vo - vi) * (vo - sqv(s + horizontal_tca(s, nvo - nvi) * (nvo - nvi))") (("1" (replaces -1) (("1" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("1" (rewrite "horizontal_sq_dtca_eq" :dir rl) (("1" (expand "horizontal_sq_dtca") (("1" (expand "horizontal_tca") (("1" (ground) (("1" (cross-mult -1) (("1" (ground) (("1" (lemma "sqv_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult -1) (("1" (ground) (("1" (cross-mult -2) nil nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (ground) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (cross-mult 1) (("3" (ground) (("3" (lemma "sqv_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (cross-mult 2) (("4" (ground) (("4" (lemma "sqv_eq_0") (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (ground) (("1" (rewrite "sqrt_lt" 1 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil) ("2" (rewrite "sqrt_lt" -1 :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (case "FORALL (vv:Vect2): vv=zero IFF (vv`x = 0 AND vv`y=0)") (("1" (case "FORALL (vv:Vect2): vv/=zero IFF (vv`x /= 0 OR vv`y/=0)") (("1" (rewrite -1) (("1" (rewrite -2) (("1" (expand "-") (("1" (expand "*") (("1" (expand "sq") (("1" (expand "repulsive_criteria") (("1" (flatten) (("1" (rewrite -2) (("1" (rewrite -2) (("1" (rewrite -2) (("1" (rewrite -2) (("1" (rewrite -2) (("1" (rewrite -2) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (hide (-1 -2)) (("1" (expand "*") (("1" (expand "det") (("1" (expand "sqv") (("1" (assert) (("1" (expand "*") (("1" (assert) (("1" (typepred "eps") (("1" (hide -1) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (metit *) nil nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (metit *) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality 1) nil nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "zero") (("2" (skeep) (("2" (grind) (("2" (decompose-equality 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vector type-eq-decl nil vectors_2D "vectors/") (real nonempty-type-from-decl nil reals nil) (repulsive_criteria const-decl "bool" repulsive nil) (repulsive? const-decl "bool" repulsive nil) (/= const-decl "boolean" notequal nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (det const-decl "real" det_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (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) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (neg_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (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) (dot_zero_right formula-decl nil vectors_2D "vectors/") (sqv const-decl "nnreal" vectors_2D "vectors/") (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 "Vector" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (tca const-decl "real" repulsive nil) (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (scal_0 formula-decl nil vectors_2D "vectors/") (sqrt_lt formula-decl nil sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (div_mult_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_neg_lt2 formula-decl nil extra_real_props nil) (div_mult_pos_neg_lt1 formula-decl nil extra_real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (times_div2 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (real_div_nzreal_is_real application-judgement "real" reals nil) (horizontal_sq_dtca const-decl "real" definitions nil) (horizontal_sq_dtca_eq formula-decl nil definitions nil) (horizontal_tca const-decl "real" definitions nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nzint nonempty-type-eq-decl nil integers nil) (Sign type-eq-decl nil sign "reals/") (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil) (foo-1 nil 3600444200 ("" (postpone) nil nil) nil shostak)) (repulsive_increases_dist_TCC1 0 (repulsive_increases_dist_TCC1-1 nil 3575270563 ("" (subtype-tcc) nil nil) ((comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (real_lt_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/") (sqv const-decl "nnreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (repulsive? const-decl "bool" repulsive nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (repulsive_increases_dist 0 (repulsive_increases_dist-1 nil 3575270565 ("" (skeep) (("" (case "v = zero") (("1" (replace -1) (("1" (assert) (("1" (expand "repulsive?") (("1" (assert) (("1" (lemma "definitions.dot_nneg_divergent") (("1" (inst?) (("1" (assert) (("1" (expand "divergent?") (("1" (skeep 3) (("1" (case "nnt = 0") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (inst - "nnt") (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "s*v<0") (("1" (assert) (("1" (hide (3 4)) (("1" (case "NOT horizontal_tca(s,v)>0") (("1" (hide 3) (("1" (expand "horizontal_tca") (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "sqv_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep 2) (("2" (case "nnt = 0") (("1" (replaces -1) (("1" (assert) (("1" (lemma "sqv_decreasing_before_horizontal_tca") (("1" (inst - "v" "s") (("1" (assert) (("1" (inst - "0" "horizontal_tca(s,v)") (("1" (assert) (("1" (rewrite "sqrt_gt" -1 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "repulsive?") (("2" (split -) (("1" (case "NOT s*nv>=0") (("1" (expand "tca") (("1" (lift-if) (("1" (split -) (("1" (flatten) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (expand "horizontal_tca") (("2" (cross-mult -1) (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "definitions.dot_nneg_divergent") (("2" (inst - "nv" "s") (("1" (assert) (("1" (expand "divergent?") (("1" (inst - "nnt") (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (lemma "sqv_decreasing_before_horizontal_tca") (("1" (inst - "v" "s") (("1" (assert) (("1" (inst - "0" "horizontal_tca(s,v)") (("1" (assert) (("1" (rewrite "sqrt_gt" -1 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (rewrite "sqrt_sqv_norm") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) (("2" (lemma "sqv_decreasing_before_horizontal_tca") (("2" (inst - "v" "s") (("2" (assert) (("2" (inst - "0" "horizontal_tca(s,v)") (("2" (assert) (("2" (rewrite "sqrt_gt" -1 :dir rl) (("2" (rewrite "sqrt_sqv_norm") (("2" (rewrite "sqrt_sqv_norm") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "horizontal_tca_min") (("2" (case "nv = zero") (("1" (replaces -1) (("1" (assert) (("1" (expand "tca") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "nv" "s" "nnt") (("1" (rewrite "horizontal_sq_dtca_eq") (("1" (assert) (("1" (rewrite "sqrt_le" -1 :dir rl) (("1" (rewrite "sqrt_sqv_norm") (("1" (rewrite "sqrt_sqv_norm") (("1" (assert) (("1" (expand "tca") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide (3 5)) (("2" (case "NOT horizontal_tca(s,v)<=0") (("1" (hide 4) (("1" (expand "repulsive?") (("1" (expand "horizontal_tca") (("1" (cross-mult 1) (("1" (ground) (("1" (lemma "sqv_eq_0") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep 3) (("2" (expand "repulsive?") (("2" (lemma "definitions.dot_nneg_divergent") (("2" (inst - "nv" "s") (("1" (assert) (("1" (expand "divergent?") (("1" (inst - "pt") (("1" (assert) (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.1.848Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26