| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 684 kB |
|
Quelle repulsive_iterative.prfSprache: Lisp |
|||||||||||||||
|
(repulsive_iterative (man_pos_seq_TCC1 0 (man_pos_seq_TCC1-1 nil 3574766784 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers 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) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (man_pos_seq_TCC2 0 (man_pos_seq_TCC2-1 nil 3574766784 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" 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 "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (man_pos_seq_TCC3 0 (man_pos_seq_TCC3-1 nil 3574766784 ("" (termination-tcc) nil nil) nil nil)) (man_pos_seq_test 0 (man_pos_seq_test-1 nil 3574766788 ("" (grind) nil nil) ((man_pos_seq def-decl "Vect2" repulsive_iterative nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (manuever_position_at_def 0 (manuever_position_at_def-1 nil 3575022941 ("" (induct "m") (("1" (assert) (("1" (skeep) (("1" (expand "maneuver_position_at") (("1" (name "iz" "floor(0)") (("1" (case "NOT iz = 0") (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (replaces -2) (("2" (replace -1) (("2" (grind) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst?) (("2" (expand "man_pos_seq" +) (("2" (assert) (("2" (replace -1 :dir rl) (("2" (hide -1) (("2" (assert) (("2" (expand "maneuver_position_at") (("2" (case "floor((j * timestep + timestep) / timestep) = floor(j * timestep / timestep)+1") (("1" (replaces -1) (("1" (assert) (("1" (expand "man_pos_seq" + 1) (("1" (grind :exclude ("man_pos_seq" "floor")) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posint_min application-judgement "{k: posint | k <= i AND k <= j}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (* const-decl "Vector" vectors_2D "vectors/") (+ const-decl "Vector" vectors_2D "vectors/") (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (maneuver_position_at const-decl "Vect2" repulsive_iterative nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (VelSeq type-eq-decl nil repulsive_iterative nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (repulsive_criteria_iterative_TCC1 0 (repulsive_criteria_iterative_TCC1-1 nil 3575207629 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (det const-decl "real" det_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (repulsive_criteria_iterative_TCC2 0 (repulsive_criteria_iterative_TCC2-1 nil 3575207629 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (det const-decl "real" det_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (repulsive_criteria_iterative_repulsive 0 (repulsive_criteria_iterative_repulsive-1 nil 3575046820 ("" (skeep) (("" (expand "repulsive_iterative?") (("" (flatten) (("" (expand "repulsive_criteria_iterative") (("" (flatten) (("" (case "s*v>=0") (("1" (assert) (("1" (hide 1) (("1" (case "FORALL (i:subrange(1,Nsteps)): man_pos_seq(s,timestep,velseq)(i)*velseq(i)>=0 (("1" (lemma "definitions.dot_nneg_divergent") (("1" (skeep) (("1" (case "FORALL (i:subrange(1,Nsteps-1)): norm(man_pos_seq(s, timestep, velseq)(1 + i)) >= n (("1" (case "FORALL (i:subrange(1,Nsteps)): norm(man_pos_seq(s, timestep, velseq)(i)) >= norm( (("1" (name "ii" "min(floor(t/timestep)+1,Nsteps)") (("1" (inst - "ii") (("1" (case "norm(maneuver_position_at(s,timestep,velseq,Nsteps)(t))>=norm(man_pos_seq(s,time (("1" (assert) nil nil) ("2" (hide (-2 2)) (("2" (case "velseq(ii)=zero") (("1" (expand "maneuver_position_at") (("1" (replace -2) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "velseq(ii)" "man_pos_seq(s,timestep,velseq)(ii)") (("1" (flatten) (("1" (hide -4) (("1" (expand "maneuver_position_at" +) (("1" (split -) (("1" (expand "divergent?") (("1" (replace -2) (("1" (inst - "t-timestep*(ii-1)") (("1" (expand "dist") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sq_dist_norm") (("1" (rewrite "sqrt_sq") (("1" (rewrite "sqrt_sq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "t = timestep*(ii-1)") (("1" (case "NOT t - timestep * floor(t / timestep) = 0") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (case "t-ii*timestep+timestep = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "t>=timestep*(ii-1)") (("1" (assert) nil nil) ("2" (name "pj" "1+floor(t/timestep)") (("2" (case "pj>=ii AND t>=timestep*(pj-1)") (("1" (flatten) (("1" (assert) (("1" (mult-by -1 "timestep") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "NOT pj>=ii") (("1" (hide 2) (("1" (expand "pj" 1) (("1" (expand "ii" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "pj" 1) (("2" (assert) (("2" (hide-all-but 1) (("2" (typepred "floor(t/timestep)") (("2" (cross-mult -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -3 "ii") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind :exclude "floor") nil nil)) nil)) nil)) nil) ("2" (case "FORALL (ii:nat): ii+1<=Nsteps IMPLIES norm(man_pos_seq(s, timestep, velseq)(ii+1) (("1" (skeep) (("1" (inst - "i-1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "ii") (("1" (expand "man_pos_seq" 1) (("1" (propax) nil nil)) nil) ("2" (skeep) (("2" (inst - "j+1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "man_pos_seq" + 1) (("2" (case "velseq(i) = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (inst - "velseq(i)" "man_pos_seq(s,timestep,velseq)(i)") (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (expand "divergent?") (("1" (inst - "timestep") (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "repulsive_criteria" - 1) (("2" (case "NOT s*velseq(1)>=0") (("1" (ground) nil nil) ("2" (hide -3) (("2" (case "FORALL (ii:nat): ii<=Nsteps-1 IMPLIES man_pos_seq(s, timestep, velseq)(ii+1) * vels (("1" (skeep) (("1" (inst - "i-1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "ii") (("1" (expand "man_pos_seq") (("1" (propax) nil nil)) nil) ("2" (skeep) (("2" (inst - "j+1") (("1" (assert) (("1" (case "man_pos_seq(s,timestep,velseq)(2+j)*velseq(1+j)>=0") (("1" (expand "repulsive_criteria") (("1" (flatten) (("1" (assert) (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "man_pos_seq" +) (("2" (hide (-2 -3 -4 -5 -6 -7 -8 -9)) (("2" (typepred "sqv(velseq(1+j))") (("2" (mult-by -1 "timestep") (("2" (grind :exclude "man_pos_seq") 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) (("2" (case "FORALL (dd:nat): dd+1<=Nsteps IMPLIES FORALL (i:subrange(1,dd+1)): FORALL (nnt:nnr (("1" (inst - "Nsteps-1") (("1" (assert) (("1" (expand "maneuver_position_at") (("1" (skeep 2) (("1" (name "jjp" "min(1 + floor(t / timestep), Nsteps)") (("1" (replace -1) (("1" (inst - "jjp") (("1" (inst?) (("1" (assert) (("1" (case "floor(t/timestep)*timestep<=t") (("1" (assert) (("1" (case "jjp-1 <= floor(t/timestep)") (("1" (mult-by -1 "timestep") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (cross-mult 1) (("2" (typepred "floor(t/timestep)") (("2" (cross-mult -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but 1) (("2" (expand "jjp") (("2" (grind :exclude "floor") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (induct "dd") (("1" (assert) (("1" (skosimp 1) (("1" (case "NOT i!1=1") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (hide -3) (("2" (lemma "repulsive_criteria_repulsive") (("2" (inst?) (("2" (assert) (("2" (expand "man_pos_seq") (("2" (expand "repulsive?") (("2" (case "norm(s)>=norm(s+tca(s,v)*v)") (("1" (case "velseq(1) = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (split -) (("1" (expand "tca" -1) (("1" (assert) (("1" (case "NOT s*velseq(1)>=0") (("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) ("2" (lemma "definitions.dot_nneg_divergent") (("2" (inst?) (("2" (assert) (("2" (skeep 2) (("2" (expand "divergent?") (("2" (inst - "nnt") (("1" (rewrite "dist_norm") (("1" (rewrite "dist_norm") (("1" (assert) nil nil)) nil)) nil) ("2" (case "nnt = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "v = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (expand "tca") (("2" (assert) (("2" (lemma "horizontal_tca_min") (("2" (skeep 3) (("2" (inst - "velseq(1)" "s" "nnt") (("2" (rewrite "horizontal_sq_dtca_eq") (("2" (assert) (("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) ("2" (hide -1) (("2" (expand "tca" 1) (("2" (assert) (("2" (lift-if) (("2" (split) (("1" (flatten) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (lemma "horizontal_tca_min") (("2" (inst - "v" "s" "0") (("2" (assert) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (skeep) (("2" (inst -4 "i-1") (("1" (assert) (("1" (typepred "i") (("1" (case "NOT i=2+j") (("1" (inst - "i") (("1" (assert) nil nil)) nil) ("2" (hide (-2 -3)) (("2" (assert) (("2" (inst - "1+j") (("2" (assert) (("2" (replace -1) (("2" (assert) (("2" (hide -4) (("2" (lemma "repulsive_criteria_repulsive") (("2" (inst?) (("2" (assert) (("2" (lemma "repulsive_increases_dist") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (flatten) (("1" (skeep 2) (("1" (inst - "nnt") (("1" (assert) (("1" (invoke (name "ttca" "%1") (! -2 1)) (("1" (replace -1) (("1" (inst - "timestep +ttca") (("1" (expand "man_pos_seq" -4 2) (("1" (assert) (("1" (grind :exclude ("repulsive_criteria" "norm" "man_pos_seq" "horizontal_tca")) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skeep 2) (("2" (case "nnt = 0") (("1" (replace -1) (("1" (assert) (("1" (hide -4) (("1" (inst - "timestep") (("1" (expand "man_pos_seq" +) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT nnt>0") (("1" (assert) nil nil) ("2" (inst - "nnt") (("2" (expand "man_pos_seq" -4 2) (("2" (inst - "timestep") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (replace -1) (("3" (assert) (("3" (skeep) (("3" (inst - "nnt") (("3" (assert) (("3" (expand "man_pos_seq" -2 2) (("3" (replace -1) (("3" (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) ("2" (assert) (("2" (case "NOT i=1") (("1" (assert) nil nil) ("2" (replaces -1) (("2" (assert) (("2" (inst - "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((repulsive_iterative? const-decl "bool" repulsive_iterative nil) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative 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) (j skolem-const-decl "nat" repulsive_iterative nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil) (dot_nneg_divergent formula-decl nil definitions nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (norm const-decl "nnreal" vectors_2D "vectors/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (j skolem-const-decl "nat" repulsive_iterative nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_min application-judgement "{k: posint | k <= i AND k <= j}" real_defs nil) (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posint nonempty-type-eq-decl nil integers nil) (maneuver_position_at const-decl "Vect2" repulsive_iterative nil) (zero const-decl "Vector" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (scal_zero formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (divergent? const-decl "bool" closest_approach_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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq_dist_norm formula-decl nil distance_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (sqrt_sq formula-decl nil sqrt "reals/") (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (dist const-decl "nnreal" distance_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (scal_0 formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (pj skolem-const-decl "posint" repulsive_iterative nil) (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") (velseq skolem-const-decl "VelSeq" repulsive_iterative nil) (ii skolem-const-decl "{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" repulsive_iterative nil) (Nsteps skolem-const-decl "posnat" repulsive_iterative nil) (timestep skolem-const-decl "posreal" repulsive_iterative nil) (t skolem-const-decl "posreal" repulsive_iterative nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (i skolem-const-decl "subrange(1, Nsteps - 1)" repulsive_iterative nil) (dist_norm formula-decl nil distance_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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (subrange type-eq-decl nil integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (VelSeq type-eq-decl nil repulsive_iterative nil) (man_pos_seq def-decl "Vect2" repulsive_iterative 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) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (comp_zero_y formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (ttca skolem-const-decl "real" repulsive_iterative nil) (nnt skolem-const-decl "nnreal" repulsive_iterative nil) (repulsive_increases_dist formula-decl nil repulsive nil) (i skolem-const-decl "subrange(1, 2 + j)" repulsive_iterative nil) (j skolem-const-decl "nat" repulsive_iterative nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (repulsive_criteria_repulsive formula-decl nil repulsive nil) (repulsive? const-decl "bool" repulsive nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (horizontal_sq_dtca_eq formula-decl nil definitions nil) (sqrt_le formula-decl nil sqrt "reals/") (sqrt_sqv_norm formula-decl nil vectors_2D "vectors/") (horizontal_tca_min formula-decl nil definitions nil) (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) (minus_real_is_real application-judgement "real" reals nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (horizontal_tca const-decl "real" definitions nil) (nnt skolem-const-decl "nnreal" repulsive_iterative nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (t skolem-const-decl "posreal" repulsive_iterative nil) (jjp skolem-const-decl "{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" repulsive_iterative nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (tca const-decl "real" repulsive nil)) shostak)) (repulsive_criteria_iterative_reduces_seq 0 (repulsive_criteria_iterative_reduces_seq-1 nil 3576335586 ("" (skeep) (("" (induct "m") (("1" (expand "repulsive_criteria_iterative") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (expand "man_pos_seq") (("2" (expand "man_pos_seq") (("2" (assert) (("2" (lemma "repulsive_criteria_scal_nv") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (expand "repulsive_criteria_iterative") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (assert) (("3" (assert) (("3" (expand "repulsive_criteria_iterative") (("3" (flatten) (("3" (inst - "k") (("3" (assert) (("3" (split +) (("1" (assert) (("1" (hide -5) (("1" (expand "man_pos_seq") (("1" (assert) (("1" (name "mps" "man_pos_seq(s, timestep, velseq)(k)") (("1" (replaces -1) (("1" (expand "repulsive_criteria") (("1" (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 -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (expand "det") (("1" (typepred "eps") (("1" (hide -1) (("1" (rewrite "vx_distr_add") (("1" (rewrite "vy_distr_add") (("1" (rewrite "vx_scal") (("1" (rewrite "vy_scal") (("1" (expand "*") (("1" (expand "+") (("1" (name "rd" "velseq(k)") (("1" (replaces -1) (("1" (name "dv" "velseq(1+k)") (("1" (replaces -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (assert) (("1" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (typepred "timestep") (("1" (hide -1) (("1" (metit *) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (typepred "timestep") (("2" (hide -1) (("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)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality +) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality -) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality -) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (name "mps" "man_pos_seq(s, timestep, velseq)(1+k)") (("2" (replace -1) (("2" (expand "man_pos_seq" +) (("2" (replaces -1) (("2" (hide -6) (("2" (hide (-1 -2)) (("2" (expand "repulsive_criteria") (("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 -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (expand "det") (("1" (typepred "eps") (("1" (hide -1) (("1" (expand "*") (("1" (expand "+") (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (assert) (("1" (name "rd" "velseq(k)") (("1" (replaces -1) (("1" (name "dv" "velseq(1+k)") (("1" (replaces -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (typepred "timestep") (("1" (hide -1) (("1" (metit *) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (typepred "timestep") (("2" (hide -1) (("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)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality +) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality -) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality -) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality +) 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) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= 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/") (repulsive_criteria const-decl "bool" repulsive nil) (VelSeq type-eq-decl nil repulsive_iterative nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (subrange_induction formula-decl nil subrange_inductions 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) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative nil) (repulsive_criteria_scal_nv formula-decl nil repulsive nil) (add_cancel formula-decl nil vectors_2D "vectors/") (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (zero const-decl "Vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D "vectors/") (vy_distr_add formula-decl nil vectors_2D "vectors/") (vy_scal formula-decl nil vectors_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (vx_distr_sub formula-decl nil vectors_2D "vectors/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (vy_distr_sub formula-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (vx_scal formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (vx_distr_add formula-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/")) shostak)) (repulsive_criteria_iterative_reduces 0 (repulsive_criteria_iterative_reduces-1 nil 3581327910 ("" (skeep) (("" (expand "maneuver_position_at") (("" (name "mm" "min(1 + floor(t / timestep), Nsteps)") (("" (replaces -1) (("" (case "NOT mm-1<Nsteps") (("1" (assert) nil nil) ("2" (case "mm = 0") (("1" (expand "mm" -1) (("1" (hide-all-but (-1)) (("1" (grind) nil nil)) nil)) nil) ("2" (case "mm = 1") (("1" (replaces -1) (("1" (assert) (("1" (expand "man_pos_seq") (("1" (assert) (("1" (lemma "repulsive_criteria_scal_nv") (("1" (inst?) (("1" (assert) (("1" (expand "repulsive_criteria_iterative") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "vv" "(man_pos_seq(s, timestep, velseq)(mm) - s)") (("2" (name "ww" "(t - mm * timestep + timestep) * velseq(mm)") (("2" (case "repulsive_criteria(s,v,eps)(vv+ww)") (("1" (hide-all-but (-1 3)) (("1" (expand "vv") (("1" (expand "ww") (("1" (grind :exclude ("repulsive_criteria" "man_pos_seq")) nil nil)) nil)) nil)) nil) ("2" (case "repulsive_criteria(s,v,eps)(vv)") (("1" (case "ww = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (hide 5) (("2" (lemma "repulsive_criteria_sum_closed") (("2" (inst?) (("2" (assert) (("2" (lemma "repulsive_criteria_scal_nv") (("2" (expand "ww" 1) (("2" (inst?) (("1" (assert) (("1" (lemma "repulsive_criteria_iterative_reduces_seq") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(t - mm * timestep + timestep) = 0") (("1" (expand "ww" 3) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "(t - mm * timestep + timestep) >= 0") (("1" (assert) nil nil) ("2" (hide (2 3)) (("2" (case "(mm-1)*timestep <= t") (("1" (assert) nil nil) ("2" (case "(mm-1)*timestep = min(floor(t/timestep)*timestep,(Nsteps-1)*timestep)") (("1" (case "t>=floor(t / timestep) * timestep") (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (mult-by 1 "1/timestep") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "mm") (("2" (expand "min") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (mult-by -1 "timestep") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "timestep") (("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) ("2" (expand "vv" 1) (("2" (lemma "repulsive_criteria_iterative_reduces_seq") (("2" (inst?) (("2" (assert) (("2" (inst - "mm-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posint_min application-judgement "{k: posint | k <= i AND k <= j}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (maneuver_position_at const-decl "Vect2" repulsive_iterative nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mm skolem-const-decl "{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" repulsive_iterative nil) (Vector type-eq-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (repulsive_criteria const-decl "bool" repulsive nil) (+ const-decl "Vector" vectors_2D "vectors/") (vv skolem-const-decl "Vector" repulsive_iterative nil) (real_times_real_is_real application-judgement "real" reals nil) (ww skolem-const-decl "Vector" repulsive_iterative nil) (zero const-decl "Vector" vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (repulsive_criteria_sum_closed formula-decl nil repulsive nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (scal_0 formula-decl nil vectors_2D "vectors/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subrange type-eq-decl nil integers nil) (repulsive_criteria_iterative_reduces_seq formula-decl nil repulsive_iterative nil) (Nsteps skolem-const-decl "posnat" repulsive_iterative nil) (timestep skolem-const-decl "posreal" repulsive_iterative nil) (t skolem-const-decl "posreal" repulsive_iterative nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "Vector" vectors_2D "vectors/") (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (repulsive_criteria_scal_nv formula-decl nil repulsive nil) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (VelSeq type-eq-decl nil repulsive_iterative nil) (add_cancel formula-decl nil vectors_2D "vectors/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_plus_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 "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ 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) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (>= const-decl "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) (int nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil)) shostak)) (repulsive_criteria_iterative_reduces_seq_divergent_special 0 (repulsive_criteria_iterative_reduces_seq_divergent_special-1 nil 3581701564 ("" (skeep) (("" (replaces -1) (("" (label "sname" -1) (("" (hide "sname") (("" (assert) (("" (induct "m") (("1" (expand "repulsive_criteria_iterative") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (expand "man_pos_seq") (("2" (expand "man_pos_seq") (("2" (assert) (("2" (expand "repulsive_criteria_iterative") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skeep) (("3" (assert) (("3" (expand "repulsive_criteria_iterative") (("3" (flatten) (("3" (inst - "k") (("3" (assert) (("3" (split +) (("1" (assert) (("1" (hide -5) (("1" (expand "man_pos_seq") (("1" (assert) (("1" (name "mps" "man_pos_seq(s, 1, velseq)(k)") (("1" (replaces -1) (("1" (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" (expand "repulsive_criteria") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (expand "det") (("1" (typepred "eps") (("1" (hide -1) (("1" (rewrite "vx_distr_add") (("1" (rewrite "vy_distr_add") (("1" (rewrite "vx_scal") (("1" (rewrite "vy_scal") (("1" (expand "*") (("1" (expand "+") (("1" (name "rd" "velseq(k)") (("1" (replaces -1) (("1" (name "dv" "velseq(1+k)") (("1" (replaces -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (assert) (("1" (reveal "sname") (("1" (replaces -1) (("1" (assert) (("1" (typepred "k") (("1" (hide (-4 -12 -18)) (("1" (hide (-4 -5 -11)) (("1" (assert) (("1" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality +) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality -) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality -) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality +) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (name "mps" "man_pos_seq(s, 1, velseq)(1+k)") (("2" (replace -1) (("2" (expand "man_pos_seq" +) (("2" (replaces -1) (("2" (hide -6) (("2" (hide (-1 -2)) (("2" (rewrite "scal_add_left") (("2" (assert) (("2" (expand "repulsive_criteria") (("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 -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (expand "det") (("1" (typepred "eps") (("1" (hide -1) (("1" (expand "*") (("1" (expand "+") (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (assert) (("1" (name "rd" "velseq(k)") (("1" (replaces -1) (("1" (name "dv" "velseq(1+k)") (("1" (replaces -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (reveal "sname") (("1" (replaces -1) (("1" (assert) (("1" (case "NOT (v`x/=0 OR v`y/=0)") (("1" (flatten) (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) (("1" (hide -5) (("1" (metit *) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (case "v`x = 0 AND v`y = 0") (("1" (flatten) (("1" (metit *) nil nil)) nil) ("2" (replace 1) (("2" (case "(2 * v`x = 0 AND 2 * v`y = 0)") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (case "NOT (NOT k * v`x = 0 OR NOT k * v`y = 0)") (("1" (hide-all-but (-1 1)) (("1" (ground) nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (hide (-1 -2 1)) (("2" (case "NOT (NOT (k+1) * v`x = 0 OR NOT (k+1) * v`y = 0)") (("1" (hide-all-but (1 2)) (("1" (ground) nil nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (case "((k+1) * v`x = 0 AND (k+1) * v`y = 0)") (("1" (hide-all-but (-1 1)) (("1" (ground) nil nil)) nil) ("2" (replaces 1) (("2" (hide 1) (("2" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (typepred "k") (("1" (hide -2) (("1" (assert) (("1" (ground) (("1" (metit *) nil nil) ("2" (metit *) nil nil) ("3" (metit *) nil nil) ("4" (metit *) nil nil) ("5" (metit *) nil nil) ("6" (metit *) nil nil) ("7" (metit *) nil nil) ("8" (metit *) nil nil) ("9" (metit *) nil nil) ("10" (metit *) nil nil) ("11" (metit *) nil nil) ("12" (metit *) nil nil) ("13" (metit *) nil nil) ("14" (metit *) nil nil) ("15" (metit *) nil nil) ("16" (metit *) nil nil) ("17" (metit *) nil nil) ("18" (metit *) nil nil) ("19" (metit *) nil nil) ("20" (metit *) nil nil) ("21" (metit *) nil nil) ("22" (metit *) nil nil) ("23" (metit *) nil nil) ("24" (metit *) nil nil) ("25" (metit *) nil nil) ("26" (metit *) nil nil) ("27" (metit *) nil nil) ("28" (metit *) nil nil) ("29" (metit *) nil nil) ("30" (metit *) nil nil) ("31" (metit *) nil nil) ("32" (metit *) nil nil) ("33" (metit *) nil nil) ("34" (metit *) nil nil) ("35" (metit *) nil nil) ("36" (metit *) nil nil) ("37" (metit *) nil nil) ("38" (metit *) nil nil) ("39" (metit *) nil nil) ("40" (metit *) nil nil) ("41" (metit *) nil nil) ("42" (metit *) nil nil) ("43" (metit *) nil nil) ("44" (metit *) nil nil) ("45" (metit *) nil nil) ("46" (metit *) nil nil) ("47" (metit *) nil nil) ("48" (metit *) nil nil) ("49" (metit *) nil nil) ("50" (metit *) nil nil) ("51" (metit *) nil nil) ("52" (metit *) nil nil) ("53" (metit *) nil nil) ("54" (metit *) nil nil) ("55" (metit *) nil nil) ("56" (metit *) nil nil) ("57" (metit *) nil nil) ("58" (metit *) nil nil) ("59" (metit *) nil nil) ("60" (metit *) nil nil) ("61" (metit *) nil nil) ("62" (metit *) nil nil) ("63" (metit *) nil nil) ("64" (metit *) nil nil) ("65" (metit *) nil nil) ("66" (metit *) nil nil) ("67" (metit *) nil nil) ("68" (metit *) nil nil) ("69" (metit *) nil nil) ("70" (metit *) nil nil) ("71" (metit *) nil nil) ("72" (metit *) nil nil) ("73" (metit *) nil nil) ("74" (metit *) nil nil) ("75" (metit *) nil nil) ("76" (metit *) nil nil) ("77" (metit *) nil nil) ("78" (metit *) nil nil) ("79" (metit *) nil nil) ("80" (metit *) nil nil) ("81" (metit *) nil nil) ("82" (metit *) nil nil) ("83" (metit *) nil nil) ("84" (metit *) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (typepred "k") (("2" (hide -2) (("2" (assert) (("2" (ground) (("1" (metit *) nil nil) ("2" (metit *) nil nil) ("3" (metit *) nil nil) ("4" (metit *) nil nil) ("5" (metit *) nil nil) ("6" (metit *) nil nil) ("7" (metit *) nil nil) ("8" (metit *) nil nil) ("9" (metit *) nil nil) ("10" (metit *) nil nil) ("11" (metit *) nil nil) ("12" (metit *) nil nil) ("13" (metit *) nil nil) ("14" (metit *) nil nil) ("15" (metit *) nil nil) ("16" (metit *) nil nil) ("17" (metit *) nil nil) ("18" (metit *) nil nil) ("19" (metit *) nil nil) ("20" (metit *) nil nil) ("21" (metit *) nil nil) ("22" (metit *) nil nil) ("23" (metit *) nil nil) ("24" (metit *) nil nil) ("25" (metit *) nil nil) ("26" (metit *) nil nil) ("27" (metit *) nil nil) ("28" (metit *) nil nil) ("29" (metit *) nil nil) ("30" (metit *) nil nil) ("31" (metit *) nil nil) ("32" (metit *) nil nil) ("33" (metit *) nil nil) ("34" (metit *) nil nil) ("35" (metit *) nil nil) ("36" (metit *) nil nil) ("37" (metit *) nil nil) ("38" (metit *) nil nil) ("39" (metit *) nil nil) ("40" (metit *) nil nil) ("41" (metit *) nil nil) ("42" (metit *) nil nil) ("43" (metit *) nil nil) ("44" (metit *) nil nil) ("45" (metit *) nil nil) ("46" (metit *) nil nil) ("47" (metit *) nil nil) ("48" (metit *) nil nil) ("49" (metit *) nil nil) ("50" (metit *) nil nil) ("51" (metit *) nil nil) ("52" (metit *) nil nil) ("53" (metit *) nil nil) ("54" (metit *) nil nil) ("55" (metit *) nil nil) ("56" (metit *) nil nil) ("57" (metit *) nil nil) ("58" (metit *) nil nil) ("59" (metit *) nil nil) ("60" (metit *) nil nil) ("61" (metit *) nil nil) ("62" (metit *) nil nil) ("63" (metit *) nil nil) ("64" (metit *) nil nil) ("65" (metit *) nil nil) ("66" (metit *) nil nil) ("67" (metit *) nil nil) ("68" (metit *) nil nil) ("69" (metit *) nil nil) ("70" (metit *) nil nil) ("71" (metit *) nil nil) ("72" (metit *) nil nil) ("73" (metit *) nil nil) ("74" (metit *) nil nil) ("75" (metit *) nil nil) ("76" (metit *) nil nil) ("77" (metit *) nil nil) ("78" (metit *) nil nil) ("79" (metit *) nil nil) ("80" (metit *) nil nil) ("81" (metit *) nil nil) ("82" (metit *) nil nil) ("83" (metit *) nil nil) ("84" (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)) 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" (hide-all-but 1) (("2" (skosimp*) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality +) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality -) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) (("1" (expand "zero") (("1" (decompose-equality -) nil nil)) nil) ("2" (expand "zero") (("2" (decompose-equality -) nil nil)) nil) ("3" (expand "zero") (("3" (decompose-equality +) 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) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= 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/") (repulsive_criteria const-decl "bool" repulsive nil) (VelSeq type-eq-decl nil repulsive_iterative nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (subrange_induction formula-decl nil subrange_inductions nil) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative nil) (add_cancel formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "Vector" vectors_2D "vectors/") (real_times_real_is_real application-judgement "real" reals nil) (det const-decl "real" det_2D "vectors/") (vy_distr_add formula-decl nil vectors_2D "vectors/") (vy_scal formula-decl nil vectors_2D "vectors/") (vx_distr_sub formula-decl nil vectors_2D "vectors/") (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (vy_distr_sub formula-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (real_minus_real_is_real application-judgement "real" reals nil) (vx_scal formula-decl nil vectors_2D "vectors/") (real_plus_real_is_real application-judgement "real" reals nil) (vx_distr_add formula-decl nil vectors_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (zero const-decl "Vector" vectors_2D "vectors/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (scal_add_left formula-decl nil vectors_2D "vectors/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (repulsive_criteria_iterative_reduces_seq_divergent 0 (repulsive_criteria_iterative_reduces_seq_divergent-1 nil 3581432581 ("" (lemma "repulsive_criteria_iterative_reduces_seq_divergent_special") (("" (skeep) (("" (label "szero" 1) (("" (hide "szero") (("" (case "s/=zero AND sqv(s)>0 AND norm(s)>0") (("1" (flatten) (("1" (name "DF" "LAMBDA (ww:Vect2): (# x:= (1/sqv(s))*(ww*s),y:=(1/sqv(s))*(ww*-perpR(s)) #)") (("1" (lemma "orthogonal_basis_dot") (("1" (case "NOT FORALL (w1,w2:Vect2): sqv(s)*(DF(w1)*DF(w2))=w1*w2") (("1" (skeep) (("1" (lemma "orthogonal_basis") (("1" (inst - "s" "-perpR(s)" _) (("1" (inst-cp - "w1") (("1" (inst - "w2") (("1" (assert) (("1" (case "-perpR(s) /= zero AND orthogonal?(s, -perpR(s))") (("1" (flatten) (("1" (assert) (("1" (inst - "((w1 * s) / sqv(s))" "((w1 * -perpR(s)) / sqv(perpR(s)))" "((w2 * s) / sqv(s))" "((w2 * -perpR(s)) / sqv(perpR(s)))" "s" "-perpR(s)" "w1" "w2") (("1" (assert) (("1" (replaces -4) (("1" (expand "DF") (("1" (hide-all-but 2) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (flatten) (("1" (case "perpR(zero) = s-s") (("1" (replaces -2 -1 :dir rl) (("1" (hide-all-but (-1 2)) (("1" (case "s+zero = perpR(-perpR(s))") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) 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)) nil)) nil)) nil)) nil)) nil) ("2" (label "Dlem" -1) (("2" (case "NOT FORALL (w1,w2:Vect2): DF(w1)*DF(w2)=(1/sqv(s))*(w1*w2)") (("1" (skeep) (("1" (cross-mult 1) (("1" (assert) (("1" (inst - "w1" "w2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (label "Hlem" -1) (("2" (assert) (("2" (case "NOT FORALL (tp:posreal,ss:Vect2,vv,ww:Vect2,epsi:Sign): (repulsive_criteria(s (("1" (hide (-7 3)) (("1" (skeep) (("1" (case "NOT (repulsive_criteria(DF(ss), tp * DF(vv), epsi) (tp * DF(ww)) IFF repulsive_criteria(DF(ss),DF(vv), epsi) (DF(ww)))") (("1" (hide 2) (("1" (lemma "repulsive_criteria_scal_nv") (("1" (case "DF(ss)*DF(vv)>=0") (("1" (inst - "tp" "epsi" "DF(ww)" "DF(ss)" "(tp)*DF(vv)") (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (mult-by -4 "tp") (("1" (assert) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (hide -) (("2" (expand "repulsive_criteria") (("2" (assert) (("2" (split) (("1" (flatten) (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (mult-by 1 "tp") (("2" (grind) nil nil)) nil) ("3" (mult-by 1 "tp") (("3" (grind) nil nil)) nil) ("4" (mult-by 1 "tp") (("4" (mult-by 1 "tp") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (mult-by 4 "tp") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (case "DF(ww) = (1/tp)*(tp*DF(ww))") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (mult-by 1 "1/tp") (("2" (grind) nil nil)) nil) ("3" (mult-by 1 "1/tp") (("3" (grind) nil nil)) nil) ("4" (flatten) (("4" (split +) (("1" (mult-by 1 "1/tp") (("1" (grind) nil nil)) nil) ("2" (mult-by 1 "1/tp") (("2" (mult-by 1 "1/tp") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (expand "repulsive_criteria" 1) (("2" (case "FORALL (Wp:Vect2): DF(Wp)/=zero IFF Wp/=zero") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (case "FORALL (w1,w2:Vect2): det(DF(w1),DF(w2))=(1/sqv(s))*det(w1,w2)") (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite "Hlem") (("1" (rewrite "Hlem") (("1" (assert) (("1" (split +) (("1" (flatten) (("1" (assert) (("1" (split 3) (("1" (assert) (("1" (mult-by 1 "sqv(s)") (("1" (assert) nil nil)) nil)) nil) ("2" (mult-by 1 "sqv(s)") (("2" (assert) nil nil)) nil) ("3" (flatten) (("3" (split -) (("1" (flatten) (("1" (split 1) (("1" (mult-by 1 "sqv(s)") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "sqv(s)") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (split +) (("1" (mult-by 1 "sqv(s)") (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil) ("3" (flatten) (("3" (mult-by 2 "sqv(s)") (("3" (assert) nil nil)) nil)) nil) ("4" (mult-by 1 "sqv(s)") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (mult-by 1 "1/sqv(s)") (("1" (assert) nil nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil) ("2" (mult-by 1 "1/sqv(s)") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil) ("3" (flatten) (("3" (split -) (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (mult-by 1 "1/sqv(s)") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil) ("2" (mult-by 1 "1/sqv(s)") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (split +) (("1" (cross-mult -1) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (replaces -1) (("2" (assert) (("2" (case "DF(zero) = zero") (("1" (assert) (("1" (mult-by 1 "1/sqv(s)") (("1" (assert) nil nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "DF") (("2" (expand "zero") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (inst -8 "vv") (("3" (assert) (("3" (mult-by 2 "1/sqv(s)") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil) ("4" (mult-by 1 "1/sqv(s)") (("1" (assert) 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) ("2" (hide 2) (("2" (skeep) (("2" (rewrite "det_perpR" +) (("2" (case "perpR(DF(w2)) = DF(perpR(w2))") (("1" (replaces -1) (("1" (rewrite "Hlem" +) (("1" (rewrite "det_perpR" +) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "DF") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (ground) (("1" (replaces -1) (("1" (hide -) (("1" (expand "DF") (("1" (expand "zero") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst - "DF(Wp)") (("2" (assert) (("2" (expand "sqv") (("2" (rewrite "Hlem") (("2" (cross-mult -1) (("2" (lemma "sqv_eq_0") (("2" (inst - "Wp") (("2" (assert) (("2" (expand "sqv") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "Nsteps" "eps" "DF(s)" "1" "timestep*DF(v)" "LAMBDA (ii:posnat): timestep*DF(velseq(ii))") (("2" (assert) (("2" (case "NOT DF(s) = (# x := 1, y := 0 #)") (("1" (expand "DF" 1) (("1" (split 1) (("1" (cross-mult 1) (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "NOT timestep * (DF(s) * DF(v)) >= 0") (("1" (mult-by 1 "1/timestep") (("1" (assert) (("1" (rewrite "Hlem" -1) (("1" (assert) (("1" (case "FORALL (egv:real): 0*egv=0") (("1" (rewrite -1) (("1" (cross-mult 1) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -2 :dir rl) (("2" (case "NOT repulsive_criteria_iterative(DF(s), timestep* DF(v), 1, LAMBDA (ii: posnat): timestep* DF(velseq(ii)), Nsteps, eps)") (("1" (hide -10) (("1" (hide 3) (("1" (expand "repulsive_criteria_iterative") (("1" (rewrite -3 + :dir rl) (("1" (flatten) (("1" (assert) (("1" (skeep) (("1" (inst - "m") (("1" (assert) (("1" (case "man_pos_seq(DF(s), 1, LAMBDA (ii: posnat): (timestep) * DF(velseq(ii))) (1 + m) = DF(man_pos_seq(s, timestep, velseq)(1 + m))") (("1" (replaces -1) (("1" (rewrite -3 + :dir rl) nil nil)) nil) ("2" (hide 2) (("2" (case "FORALL (mm:nat): man_pos_seq(DF(s), 1, LAMBDA (ii: posnat): timestep * DF(velseq(ii))) (1 + mm) = DF(man_pos_seq(s, timestep, velseq)(1 + mm))") (("1" (inst - "m") nil nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "man_pos_seq") (("1" (propax) nil nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "man_pos_seq" +) (("2" (replaces -1) (("2" (hide -) (("2" (expand "DF") (("2" (grind :exclude ("sqv" "man_pos_seq")) 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" (skeep 2) (("2" (inst - "m") (("2" (flatten) (("2" (assert) (("2" (rewrite -4 :dir rl) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (case "man_pos_seq(DF(s), 1, LAMBDA (ii: posnat): (timestep) * DF(velseq(ii))) (1 + m) = DF(man_pos_seq(s, timestep, velseq)(1 + m))") (("1" (replaces -1) (("1" (case "FORALL (ww1,ww2:Vect2): DF(ww1-ww2)=DF(ww1)-DF(ww2)") (("1" (rewrite -1 :dir rl) (("1" (case "(m*timestep)*DF(v) = DF((m*timestep)*v)") (("1" (replaces -1) (("1" (assert) (("1" (inst -5 "1" _ _ _ _) (("1" (assert) (("1" (rewrite -5 :dir rl) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "DF") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "DF") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (mm:nat): man_pos_seq(DF(s), 1, LAMBDA (ii: posnat): timestep * DF(velseq(ii))) (1 + mm) = DF(man_pos_seq(s, timestep, velseq)(1 + mm))") (("1" (inst - "m") nil nil) ("2" (hide 2) (("2" (induct "mm") (("1" (assert) (("1" (expand "man_pos_seq") (("1" (propax) nil nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (expand "man_pos_seq" +) (("2" (replaces -1) (("2" (hide -) (("2" (expand "DF") (("2" (grind :exclude ("sqv" "man_pos_seq")) 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" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (reveal "szero") (("2" (assert) (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) (("2" (lemma "norm_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((norm_eq_0 formula-decl nil vectors_2D "vectors/") (orthogonal_basis_dot formula-decl nil basis_2D "vectors/") (nonneg_real nonempty-type-eq-decl nil real_types 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) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (IFF const-decl "[bool, bool -> bool]" booleans nil) (repulsive_criteria const-decl "bool" repulsive nil) (* const-decl "Vector" vectors_2D "vectors/") (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (s skolem-const-decl "Vect2" repulsive_iterative nil) (dot_zero_right formula-decl nil vectors_2D "vectors/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (det_perpR formula-decl nil det_2D "vectors/") (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (div_cancel3 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (scal_1 formula-decl nil vectors_2D "vectors/") (scal_assoc formula-decl nil vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (< const-decl "bool" reals nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (det const-decl "real" det_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (both_sides_times_pos_ge1 formula-decl nil real_props nil) (repulsive_criteria_scal_nv formula-decl nil repulsive nil) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative nil) (subrange type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (VelSeq type-eq-decl nil repulsive_iterative nil) (div_cancel4 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (orthogonal? const-decl "bool" vectors_2D "vectors/") (DF skolem-const-decl "[Vect2 -> [# x: real, y: real #]]" repulsive_iterative nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (+ const-decl "Vector" vectors_2D "vectors/") (sub_eq_args formula-decl nil vectors_2D "vectors/") (add_zero_right formula-decl nil vectors_2D "vectors/") (comp_zero_x formula-decl nil vectors_2D "vectors/") (comp_zero_y formula-decl nil vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (sqv_neg formula-decl nil vectors_2D "vectors/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (orthogonal_basis formula-decl nil basis_2D "vectors/") (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "real" vectors_2D "vectors/") (- const-decl "Vector" vectors_2D "vectors/") (perpR const-decl "Vect2" perpendicular_2D "vectors/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (/= const-decl "boolean" notequal nil) (Vector type-eq-decl nil vectors_2D "vectors/") (zero const-decl "Vector" vectors_2D "vectors/") (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (norm const-decl "nnreal" vectors_2D "vectors/") (repulsive_criteria_iterative_reduces_seq_divergent_special formula-decl nil repulsive_iterative nil)) nil)) (repulsive_criteria_iterative_reduces_seq_div 0 (repulsive_criteria_iterative_reduces_seq_div-1 nil 3581429161 ("" (skeep) (("" (case "s = zero") (("1" (assert) (("1" (replaces -1) (("1" (assert) nil nil)) nil)) nil) ("2" (label "szero" 1) (("2" (hide "szero") (("2" (name "newv" "LAMBDA (n:nat): eps*perpR(s) - (1/(n+1))*s") (("2" (case "FORALL (n:nat): repulsive_criteria_iterative(s, newv(n), timestep, velseq, Nstep (("1" (lemma "repulsive_criteria_iterative_reduces_seq") (("1" (case "FORALL (n:nat): FORALL (m:subrange(1,Nsteps)): s*velseq(m)>=0 AND (m < Nsteps IMPLIES repulsive_criteria(s, newv(n), eps) (man_pos_seq(s, timestep, velseq)(m + 1) - s))") (("1" (skeep) (("1" (split +) (("1" (inst - "1") (("1" (inst - "m") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (skoletin 1) (("2" (case "NOT FORALL (n:nat): eps*det(vv,newv(n)) < 0") (("1" (skeep) (("1" (inst - "n") (("1" (inst - "m") (("1" (assert) (("1" (flatten) (("1" (hide -3) (("1" (expand "repulsive_criteria" -3) (("1" (case "s*newv(n)<0") (("1" (assert) nil nil) ("2" (case "s = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (1 2)) (("2" (expand "newv") (("2" (case "sqv(s)>0") (("1" (mult-by -1 "1/(1+n)") (("1" (grind) 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) ("2" (name "V" "(eps*perpR(s))") (("2" (case "eps*det(vv,V)<=0") (("1" (hide-all-but (-1 1)) (("1" (expand "V") (("1" (typepred "eps") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand "newv" -2) (("2" (replaces -1) (("2" (case "s = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (hide-all-but (-1 1 2)) (("2" (case "EXISTS (n:nat): (1/(1+n)) *(eps*det(vv,s)) <= eps*det(vv,V)") (("1" (skeep -1) (("1" (inst - "n") (("1" (grind) nil nil)) nil)) nil) ("2" (hide -1) (("2" (case "FORALL (aa:real,bb:posreal): EXISTS (n:nat): (1/(1+n))*aa<=bb") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (case "aa<=0") (("1" (inst + "1") (("1" (assert) nil nil)) nil) ("2" (lemma "archimedean") (("2" (inst - "bb/aa") (("1" (skeep -1) (("1" (inst + "n-1") (("1" (assert) (("1" (cross-mult -1) (("1" (cross-mult 2) nil nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil) ("3" (assert) 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" (skeep) (("2" (split +) (("1" (case "FORALL (n:nat): FORALL (m: subrange(1, Nsteps)): repulsive_criteria(s, newv(n), eps)(velseq(m))") (("1" (hide (-2 -3)) (("1" (hide -4) (("1" (expand "repulsive_criteria") (("1" (case "NOT FORALL (n:nat): (s * newv(n) < 0 AND eps * det(velseq(m), newv(n)) < 0)") (("1" (skeep) (("1" (inst - "n!1") (("1" (inst - "m") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (replace 1) (("1" (flatten) (("1" (hide-all-but (-3 2)) (("1" (case "sqv(s)>0") (("1" (mult-by -1 "(1/(1+n!1))") (("1" (expand "newv") (("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)) nil)) nil) ("2" (expand "newv" -1) (("2" (hide -2) (("2" (case "EXISTS (n:nat): (1/(1+n))*(eps*det(velseq(m),s)) <= -(s*velseq(m))") (("1" (skosimp*) (("1" (inst - "n!1") (("1" (flatten) (("1" (typepred "eps") (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -) (("2" (case "FORALL (aa:real,bb:posreal): EXISTS (n:nat): (1/(1+n))*aa<=bb") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (case "aa<=0") (("1" (inst + "1") (("1" (assert) nil nil)) nil) ("2" (lemma "archimedean") (("2" (inst - "bb/aa") (("1" (skosimp*) (("1" (inst + "n!1-1") (("1" (assert) (("1" (cross-mult -1) (("1" (cross-mult 2) nil nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (cross-mult 1) nil nil) ("2" (cross-mult 1) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "Nsteps" "eps" "s" "timestep" "newv(n!1)" "velseq") (("2" (assert) (("2" (inst - "n!1") (("2" (assert) (("2" (split -) (("1" (inst - "m!1") (("1" (assert) nil nil)) nil) ("2" (reveal "szero") (("2" (hide-all-but (1 2)) (("2" (expand "newv") (("2" (case "sqv(s)>0") (("1" (mult-by -1 "1/(1+n!1)") (("1" (grind) 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) ("2" (flatten) (("2" (inst - "Nsteps" "eps" "s" "timestep" "newv(n)" "velseq") (("2" (assert) (("2" (split -) (("1" (inst - "m") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (expand "newv") (("2" (case "sqv(s)>0") (("1" (mult-by -1 "1/(1+n)") (("1" (grind) nil nil)) nil) ("2" (reveal "szero") (("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "repulsive_criteria_iterative") (("2" (flatten) (("2" (name "V" "(eps*perpR(s))") (("2" (hide -2) (("2" (split +) (("1" (hide -4) (("1" (expand "repulsive_criteria") (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (case "sqv(s)>0") (("1" (mult-by -1 "1/(1+n)") (("1" (hide-all-but (-1 -2 1 2)) (("1" (expand "newv") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case "NOT s*newv(n)<0") (("1" (hide (2 3)) (("1" (expand "newv" 1) (("1" (case "sqv(s)>0") (("1" (mult-by -1 "1/(1+n)") (("1" (grind) nil nil)) nil) ("2" (lemma "sqv_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "newv") (("2" (typepred "eps") (("2" (mult-by -7 "1/(1+n)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((zero const-decl "Vector" vectors_2D "vectors/") (Vector type-eq-decl nil vectors_2D "vectors/") (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (real nonempty-type-from-decl nil reals nil) (sub_zero_right formula-decl nil vectors_2D "vectors/") (dot_zero_left formula-decl nil vectors_2D "vectors/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (VelSeq type-eq-decl nil repulsive_iterative nil) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (* const-decl "real" vectors_2D "vectors/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (repulsive_criteria const-decl "bool" repulsive nil) (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (vv skolem-const-decl "Vector" repulsive_iterative nil) (eps skolem-const-decl "Sign" repulsive_iterative nil) (archimedean formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (bb skolem-const-decl "posreal" repulsive_iterative nil) (aa skolem-const-decl "real" repulsive_iterative nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (V skolem-const-decl "Vector" repulsive_iterative nil) (newv skolem-const-decl "[nat -> Vector]" repulsive_iterative nil) (sqv_eq_0 formula-decl nil vectors_2D "vectors/") (both_sides_times_pos_gt1 formula-decl nil real_props 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) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqv const-decl "nnreal" vectors_2D "vectors/") (nnreal type-eq-decl nil real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (det const-decl "real" det_2D "vectors/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (m skolem-const-decl "subrange(1, Nsteps)" repulsive_iterative nil) (Nsteps skolem-const-decl "posnat" repulsive_iterative nil) (velseq skolem-const-decl "VelSeq" repulsive_iterative nil) (s skolem-const-decl "Vect2" repulsive_iterative nil) (bb skolem-const-decl "posreal" repulsive_iterative nil) (aa skolem-const-decl "real" repulsive_iterative nil) (repulsive_criteria_iterative_reduces_seq formula-decl nil repulsive_iterative nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "Vector" vectors_2D "vectors/") (* const-decl "Vector" vectors_2D "vectors/") (/= const-decl "boolean" notequal nil) (nzint nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Sign type-eq-decl nil sign "reals/") (perpR const-decl "Vect2" perpendicular_2D "vectors/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (repulsive_criteria_iterative_reduces_div 0 (repulsive_criteria_iterative_reduces_div-2 nil 3581415074 ("" (skeep) (("" (expand "maneuver_position_at") (("" (name "mm" "min(1 + floor(t / timestep), Nsteps)") (("" (replaces -1) (("" (case "NOT mm-1<Nsteps") (("1" (assert) nil nil) ("2" (case "mm = 0") (("1" (expand "mm" -1) (("1" (hide-all-but (-1)) (("1" (grind) nil nil)) nil)) nil) ("2" (case "mm = 1") (("1" (replaces -1) (("1" (assert) (("1" (expand "man_pos_seq") (("1" (assert) (("1" (expand "repulsive_criteria_iterative") (("1" (flatten) (("1" (hide -4) (("1" (expand "repulsive_criteria") (("1" (flatten) (("1" (assert) (("1" (case "NOT s*velseq(1)>=0") (("1" (ground) nil nil) ("2" (mult-by -1 "t") (("2" (assert) (("2" (case "v = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (mult-by -7 "t") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "repulsive_criteria_iterative_reduces_seq_divergent") (("2" (inst?) (("2" (assert) (("2" (case "s = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst-cp - "mm-1") (("2" (assert) (("2" (flatten) (("2" (name "DV" "man_pos_seq(s, timestep, velseq)(mm) - s") (("2" (replace -1) (("2" (inst - "mm") (("2" (flatten) (("2" (hide -3) (("2" (assert) (("2" (hide -3) (("2" (name "tc" "(t - mm * timestep + timestep)") (("2" (case "tc>=0") (("1" (case "s*DV>=s*((mm * timestep - timestep) * v)") (("1" (case "s*velseq(mm)>=s*v") (("1" (mult-by -1 "(t - mm * timestep + timestep)") (("1" (hide-all-but (-1 -2 +)) (("1" (expand "DV") (("1" (grind :exclude ("man_pos_seq")) nil nil)) nil)) nil)) nil) ("2" (hide 5) (("2" (expand "repulsive_criteria" -5) (("2" (flatten) (("2" (case "v = zero") (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "repulsive_criteria" -5) (("2" (case "(mm * timestep - timestep) * v = zero") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (split -7) (("1" (flatten) (("1" (mult-by -10 "(mm-1)*timestep") (("1" (assert) nil nil) ("2" (lemma "nnreal_times_nnreal_is_nnreal") (("2" (inst - "mm-1" "timestep") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(mm-1)*timestep <= t") (("1" (assert) nil nil) ("2" (case "(mm-1)*timestep = min(floor(t/timestep)*timestep,(Nsteps-1)*timestep)") (("1" (case "t>=floor(t / timestep) * timestep") (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) (("2" (mult-by 1 "1/timestep") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "mm") (("2" (expand "min") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (mult-by -1 "timestep") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "timestep") (("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) ((nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posint_min application-judgement "{k: posint | k <= i AND k <= j}" real_defs nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (maneuver_position_at const-decl "Vect2" repulsive_iterative nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mm skolem-const-decl "{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" repulsive_iterative nil) (Sign type-eq-decl nil sign "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nzint nonempty-type-eq-decl nil integers nil) (dot_zero_left formula-decl nil vectors_2D "vectors/") (sub_zero_right formula-decl nil vectors_2D "vectors/") (subrange type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (* const-decl "Vector" vectors_2D "vectors/") (scal_zero formula-decl nil vectors_2D "vectors/") (Nsteps skolem-const-decl "posnat" repulsive_iterative nil) (timestep skolem-const-decl "posreal" repulsive_iterative nil) (t skolem-const-decl "posreal" repulsive_iterative nil) (DV skolem-const-decl "Vector" repulsive_iterative nil) (+ const-decl "Vector" vectors_2D "vectors/") (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (- const-decl "Vector" vectors_2D "vectors/") (repulsive_criteria_iterative_reduces_seq_divergent formula-decl nil repulsive_iterative nil) (man_pos_seq def-decl "Vect2" repulsive_iterative nil) (repulsive_criteria_iterative const-decl "bool" repulsive_iterative nil) (Vector type-eq-decl nil vectors_2D "vectors/") (* const-decl "real" vectors_2D "vectors/") (Vect2 type-eq-decl nil vectors_2D_def "vectors/") (VelSeq type-eq-decl nil repulsive_iterative nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (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) (repulsive_criteria const-decl "bool" repulsive nil) (dot_scal_right formula-decl nil vectors_2D "vectors/") (add_cancel formula-decl nil vectors_2D "vectors/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals 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 "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ 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) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (>= const-decl "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) (int nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil)) nil) (repulsive_criteria_iterative_reduces_div-1 nil 3581330688 ("" (skeep) (("" (induct "m") (("1" (expand "repulsive_criteria_iterative") (("1" (assert) nil))) ("2" (assert) (("2" (flatten) (("2" (expand "man_pos_seq") (("2" (expand "man_pos_seq") (("2" (assert) (("2" (lemma "repulsive_criteria_scal_nv") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (expand "repulsive_criteria_iterative") (("2" (propax) nil))))))))))))))))))))) ("3" (skeep) (("3" (assert) (("3" (assert) (("3" (expand "repulsive_criteria_iterative") (("3" (flatten) (("3" (inst - "k") (("3" (assert) (("3" (split +) (("1" (assert) (("1" (hide -5) (("1" (expand "man_pos_seq") (("1" (assert) (("1" (name "mps" "man_pos_seq(s, timestep, velseq)(k)") (("1" (replaces -1) (("1" (expand "repulsive_criteria") (("1" (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 -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (rewrite -1) (("1" (expand "det") (("1" (typepred "eps") (("1" (hide -1) (("1" (rewrite "vx_distr_add") (("1" (rewrite "vy_distr_add") (("1" (rewrite "vx_scal") (("1" (rewrite "vy_scal") (("1" (expand "*") (("1" (expand "+") (("1" (name "rd" "velseq(k)") (("1" (replaces -1) (("1" (name "dv" "velseq(1+k)") (("1" (replaces -1) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (rewrite "vx_distr_sub") (("1" (rewrite "vy_distr_sub") (("1" (assert) (("1" (split -1) (("1" (replaces -1) (("1" (assert) (("1" (typepred "timestep") (("1" (hide -1) (("1" (metit *) nil))))))))) ("2" (replaces --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.815 Sekunden (vorverarbeitet am 2026-04-29) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26