Quelle repulsive_iterative.prf
Sprache: Lisp
(repulsive_iterativenil 3574766784 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3574766784 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3574766784 ("" (termination-tcc) nil nil ) nil nil ))nil 3574766788 ("" (grind) nil nil )"Vect2" repulsive_iterative nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" reals nil )"real" reals nil ))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" "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 )"posreal" nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"nnreal" nil )"posreal" nil )"nat" floor_ceil nil )"{k: posint | k <= i AND k <= j}" nil )"posreal" nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"posint" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"{i | i <= x & x < i + 1}" floor_ceil nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil naturalnumbers nil )"Vect2" repulsive_iterative nil )"[numfield, numfield -> numfield]" number_fields nil )"Vect2" repulsive_iterative nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )nil repulsive_iterative nil )nil real_types nil )nil real_types nil )nil vectors_2D_def "vectors/" )nil integers nil )"bool" reals nil )nil integers nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"nnreal" nil ))nil 3575207629"" (subtype-tcc) nil nil )"boolean" notequal nil )"real" det_2D "vectors/" )"real" vectors_2D "vectors/" )"bool" repulsive nil )"real" reals nil ))nil ))nil 3575207629"" (subtype-tcc) nil nil )"boolean" notequal nil )"real" det_2D "vectors/" )"real" vectors_2D "vectors/" )"bool" repulsive nil )"real" reals nil ))nil ))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)) >= norm(man_pos_seq(s, timestep, velseq)(i))" )"1" case "FORALL (i:subrange(1,Nsteps)): norm(man_pos_seq(s, timestep, velseq)(i)) >= norm(s)" )"1" "ii" "min(floor(t/timestep)+1,Nsteps)" )"1" "ii" )"1" case "norm(maneuver_position_at(s,timestep,velseq,Nsteps)(t))>=norm(man_pos_seq(s,timestep,velseq)(ii))" )"1" (assert ) nil nil )"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" "velseq(ii)" "man_pos_seq(s,timestep,velseq)(ii)" )"1" "1" "1" expand "maneuver_position_at" "1" "1" expand "divergent?" )"1" replace -2)"1" "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" "2" case "t-ii*timestep+timestep = 0" )"1" replace "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" "pj" "1+floor(t/timestep)" )"2" case "pj>=ii AND t>=timestep*(pj-1)" )"1" "1" assert )"1" "timestep" )"1" assert )nil nil ))nil ))nil ))nil )"2" case "NOT pj>=ii" )"1" "1" expand "pj" "1" expand "ii" "1" assert )nil nil ))nil ))nil ))nil )"2" replace "2" expand "pj" "2" assert )"2" "2" "floor(t/timestep)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ii" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "floor" )nil nil ))nil ))nil ))nil )"2" case "FORALL (ii:nat): ii+1<=Nsteps IMPLIES norm(man_pos_seq(s, timestep, velseq)(ii+1)) >= norm(s)" )"1" "1" "i-1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "ii" )"1" expand "man_pos_seq" 1)"1" (propax) nil nil ))nil )"2" "2" "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" "1" (assert ) nil nil ))nil )"2" "velseq(i)" "man_pos_seq(s,timestep,velseq)(i)" )"1" "1" "1" "1" expand "divergent?" )"1" "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) * velseq(ii+1) >= 0" )"1" "1" "i-1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "ii" )"1" expand "man_pos_seq" )"1" (propax) nil nil ))nil )"2" "2" "j+1" )"1" assert )"1" case "man_pos_seq(s,timestep,velseq)(2+j)*velseq(1+j)>=0" )"1" expand "repulsive_criteria" )"1" "1" assert )"1" nil nil ))nil ))nil ))nil )"2" "2" expand "man_pos_seq" +)"2" "2" "sqv(velseq(1+j))" )"2" "timestep" )"2" "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:nnreal): norm(man_pos_seq(s, timestep, velseq)(i) + nnt*velseq(i)) >= norm(s + tca(s, v) * v)" )"1" (inst - "Nsteps-1" )"1" (assert )"1" (expand "maneuver_position_at" )"1" (skeep 2)"1" "jjp" "min(1 + floor(t / timestep), Nsteps)" )"1" replace -1)"1" "jjp" )"1" "1" assert )"1" case "floor(t/timestep)*timestep<=t" )"1" assert )"1" case "jjp-1 <= floor(t/timestep)" )"1" "timestep" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "2" "floor(t/timestep)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "jjp" )"2" "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" "2" "repulsive_criteria_repulsive" )"2" "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" "1" expand "tca" -1)"1" assert )"1" case "NOT s*velseq(1)>=0" )"1" expand "horizontal_tca" )"1" "1" "1" "sqv_eq_0" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "definitions.dot_nneg_divergent" )"2" "2" assert )"2" "2" expand "divergent?" )"2" "nnt" )"1" rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" assert )nil nil ))nil ))nil )"2" case "nnt = 0" )"1" replace "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "v = zero" )"1" "1" assert )nil nil ))nil )"2" expand "tca" )"2" assert )"2" "horizontal_tca_min" )"2" "2" "velseq(1)" "s" "nnt" )"2" rewrite "horizontal_sq_dtca_eq" )"2" assert )"2" rewrite "sqrt_le" "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" "2" expand "tca" 1)"2" assert )"2" "2" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )"2" "horizontal_tca_min" )"2" "v" "s" "0" )"2" assert )"2" rewrite "horizontal_sq_dtca_eq" )"2" rewrite "sqrt_le" "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" "i-1" )"1" assert )"1" "i" )"1" case "NOT i=2+j" )"1" "i" )"1" (assert ) nil nil ))nil )"2" "2" assert )"2" "1+j" )"2" assert )"2" replace -1)"2" assert )"2" "2" "repulsive_criteria_repulsive" )"2" "2" assert )"2" "repulsive_increases_dist" )"2" "2" assert )"2" "1" "1" "1" "nnt" )"1" assert )"1" "ttca" "%1" )"1" replace "1" "timestep +ttca" )"1" expand "man_pos_seq" "1" assert )"1" "repulsive_criteria" "norm" "man_pos_seq" "horizontal_tca" ))nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "nnt = 0" )"1" replace "1" assert )"1" "1" "timestep" )"1" expand "man_pos_seq" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT nnt>0" )"1" assert )nil nil )"2" "nnt" )"2" expand "man_pos_seq" "2" "timestep" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" assert )"3" "3" "nnt" )"3" assert )"3" expand "man_pos_seq" "3" replace "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" "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 )"bool" repulsive_iterative nil )"bool" repulsive_iterativenil )nil vectors_2D_def "vectors/" )"real" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nat" repulsive_iterative nil )"nnreal" vectors_2D "vectors/" )"bool" repulsive nil )nil definitions nil )"int" integers nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"nat" repulsive_iterative nil )"nat" floor_ceil nil )"posreal" nil )"posint" nil )"{k: posint | k <= i AND k <= j}" nil )"[T, T -> boolean]" equalities nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil integers nil )"bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil integers nil )"Vect2" repulsive_iterative nil )"Vector" vectors_2D "vectors/" )"real" reals nil )"posint" nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" reals nil )"posreal" nil )"bool" closest_approach_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil distance_2D "vectors/" )nil vectors_2D "vectors/" )nil sqrt "reals/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" distance_2D "vectors/" )"odd_int" integers nil )nil vectors_2D "vectors/" )"nnreal" nil )NOT const-decl "[bool -> bool]" booleans nil )nil extra_real_propsnil )nil real_props nil )"posint" repulsive_iterative nil )nil vectors_2D "vectors/" )"VelSeq" repulsive_iterative nil )"{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" nil )"posnat" repulsive_iterative nil )"posreal" repulsive_iterative nil )"posreal" repulsive_iterative nil )"(total_order?[real])" nil )"subrange(1, Nsteps - 1)" repulsive_iterativenil )nil distance_2D "vectors/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil real_types nil )nil real_types nil )nil repulsive_iterative nil )"Vect2" repulsive_iterative nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"even_int" integersnil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" repulsive_iterative nil )"nnreal" repulsive_iterative nil )nil repulsive nil )"subrange(1, 2 + j)" repulsive_iterative nil )"nat" repulsive_iterative nil )"odd_int" integers nil )nil repulsive nil )"bool" repulsive nil )nil vectors_2D "vectors/" )nil definitions nil )nil sqrt "reals/" )nil vectors_2D "vectors/" )nil definitions nil )"real" reals nil )nil extra_real_props nil )nil reals nil )"real" reals nil )nil vectors_2D "vectors/" )"real" definitions nil )"nnreal" repulsive_iterative nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"posreal" repulsive_iterative nil )"{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" nil )nil extra_real_propsnil )"real" repulsive nil ))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" "mps" "man_pos_seq(s, timestep, velseq)(k)" )"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" "eps" )"1" "1" rewrite "vx_distr_add" )"1" rewrite "vy_distr_add" )"1" rewrite "vx_scal" )"1" rewrite "vy_scal" )"1" expand "*" )"1" expand "+" )"1" "rd" "velseq(k)" )"1" "1" "dv" "velseq(1+k)" )"1" "1" assert )"1" "1" assert )"1" rewrite "vx_distr_sub" )"1" rewrite "vy_distr_sub" )"1" assert )"1" "1" "1" assert )"1" "timestep" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "timestep" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "mps" "man_pos_seq(s, timestep, velseq)(1+k)" )"2" (replace -1)"2" (expand "man_pos_seq" +)"2" "2" "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" expand "det" )"1" "eps" )"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" "rd" "velseq(k)" )"1" "1" "dv" "velseq(1+k)" )"1" "1" assert )"1" "1" assert )"1" "1" "1" assert )"1" "timestep" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "timestep" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil 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" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil defined_types nil )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" repulsive nil )nil repulsive_iterative nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil real_types nil )nil real_types nil )"Vect2" repulsive_iterative nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil subrange_inductions nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" repulsive_iterativenil )nil repulsive nil )nil vectors_2D "vectors/" )"int" integers nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )"real" reals nil )"real" det_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )"odd_int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"real" reals nil )nil vectors_2D "vectors/" )"real" reals nil )nil vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" ))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" "vv" "(man_pos_seq(s, timestep, velseq)(mm) ") "2" "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" "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" "repulsive_criteria_sum_closed" )"2" "2" assert )"2" "repulsive_criteria_scal_nv" )"2" expand "ww" 1)"2" "1" assert )"1" "repulsive_criteria_iterative_reduces_seq" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "(t - mm * timestep + timestep) = 0" )"1" expand "ww" 3)"1" "1" (assert ) nil nil ))nil ))nil )"2" assert )"2" case "(t - mm * timestep + timestep) >= 0" )"1" (assert ) nil nil )"2" "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" "1" nil nil ))nil ))nil )"2" "2" "2" "1/timestep" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "mm" )"2" expand "min" )"2" "2" "2" "2" assert )"2" "1" "timestep" )"1" assert )nil nil ))nil )"2" "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" "repulsive_criteria_iterative_reduces_seq" )"2" (inst?)"2" assert )"2" "mm-1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" floor_ceil nil )"{k: posint | k <= i AND k <= j}" nil )"posreal" nil )"Vect2" repulsive_iterative nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"bool" repulsive nil )"Vector" vectors_2D "vectors/" )"Vector" repulsive_iterative nil )"real" reals nil )"Vector" repulsive_iterative nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil repulsive nil )"odd_int" integers nil )nil vectors_2D "vectors/" )nil extra_real_propsnil )nil real_props nil )nil real_props nil )"nnreal" nil )"(total_order?[real])" nil )nil integers nil )nil nil )"posnat" repulsive_iterative nil )"posreal" repulsive_iterative nil )"posreal" repulsive_iterative nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )"Vect2" repulsive_iterative nil )nil repulsive nil )"bool" repulsive_iterativenil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )nil vectors_2D_def "vectors/" )nil repulsive_iterative nil )nil vectors_2D "vectors/" )"even_int" integersnil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"posreal" nil )"posint" nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil integers nil )nil integers nil )nil integers nil )nil integers nil ))nil "" (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" "1" expand "man_pos_seq" )"1" assert )"1" "mps" "man_pos_seq(s, 1, velseq)(k)" )"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" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" expand "det" )"1" "eps" )"1" "1" rewrite "vx_distr_add" )"1" rewrite "vy_distr_add" )"1" rewrite "vx_scal" )"1" rewrite "vy_scal" )"1" expand "*" )"1" expand "+" )"1" "rd" "velseq(k)" )"1" "1" "dv" "velseq(1+k)" )"1" "1" assert )"1" "1" assert )"1" rewrite "vx_distr_sub" )"1" rewrite "vy_distr_sub" )"1" assert )"1" "sname" )"1" "1" assert )"1" "k" )"1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mps" "man_pos_seq(s, 1, velseq)(1+k)" )"2" replace -1)"2" expand "man_pos_seq" +)"2" "2" "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" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" rewrite "1" expand "det" )"1" "eps" )"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" "rd" "velseq(k)" )"1" "1" "dv" "velseq(1+k)" )"1" "1" assert )"1" "1" assert )"1" "sname" )"1" "1" assert )"1" case "NOT (v`x/=0 OR v`y/=0)" )"1" "1" "1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" case "v`x = 0 AND v`y = 0" )"1" "1" nil nil ))nil )"2" replace "2" case "(2 * v`x = 0 AND 2 * v`y = 0)" )"1" "1" assert )nil nil ))nil )"2" case "NOT (NOT k * v`x = 0 OR NOT k * v`y = 0)" )"1" "1" nil nil ))nil )"2" replace "2" assert )"2" "2" case "NOT (NOT (k+1) * v`x = 0 OR NOT (k+1) * v`y = 0)" )"1" "1" nil nil ))nil )"2" replace "2" "2" case "((k+1) * v`x = 0 AND (k+1) * v`y = 0)" )"1" "1" nil nil ))nil )"2" "2" "2" "1" "1" assert )"1" "k" )"1" "1" assert )"1" "1" nil nil )"2" nil nil )"3" nil nil )"4" nil nil )"5" nil nil )"6" nil nil )"7" nil nil )"8" nil nil )"9" nil nil )"10" nil nil )"11" nil nil )"12" nil nil )"13" nil nil )"14" nil nil )"15" nil nil )"16" nil nil )"17" nil nil )"18" nil nil )"19" nil nil )"20" nil nil )"21" nil nil )"22" nil nil )"23" nil nil )"24" nil nil )"25" nil nil )"26" nil nil )"27" nil nil )"28" nil nil )"29" nil nil )"30" nil nil )"31" nil nil )"32" nil nil )"33" nil nil )"34" nil nil )"35" nil nil )"36" nil nil )"37" nil nil )"38" nil nil )"39" nil nil )"40" nil nil )"41" nil nil )"42" nil nil )"43" nil nil )"44" nil nil )"45" nil nil )"46" nil nil )"47" nil nil )"48" nil nil )"49" nil nil )"50" nil nil )"51" nil nil )"52" nil nil )"53" nil nil )"54" nil nil )"55" nil nil )"56" nil nil )"57" nil nil )"58" nil nil )"59" nil nil )"60" nil nil )"61" nil nil )"62" nil nil )"63" nil nil )"64" nil nil )"65" nil nil )"66" nil nil )"67" nil nil )"68" nil nil )"69" nil nil )"70" nil nil )"71" nil nil )"72" nil nil )"73" nil nil )"74" nil nil )"75" nil nil )"76" nil nil )"77" nil nil )"78" nil nil )"79" nil nil )"80" nil nil )"81" nil nil )"82" nil nil )"83" nil nil )"84" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "k" )"2" "2" assert )"2" "1" nil nil )"2" nil nil )"3" nil nil )"4" nil nil )"5" nil nil )"6" nil nil )"7" nil nil )"8" nil nil )"9" nil nil )"10" nil nil )"11" nil nil )"12" nil nil )"13" nil nil )"14" nil nil )"15" nil nil )"16" nil nil )"17" nil nil )"18" nil nil )"19" nil nil )"20" nil nil )"21" nil nil )"22" nil nil )"23" nil nil )"24" nil nil )"25" nil nil )"26" nil nil )"27" nil nil )"28" nil nil )"29" nil nil )"30" nil nil )"31" nil nil )"32" nil nil )"33" nil nil )"34" nil nil )"35" nil nil )"36" nil nil )"37" nil nil )"38" nil nil )"39" nil nil )"40" nil nil )"41" nil nil )"42" nil nil )"43" nil nil )"44" nil nil )"45" nil nil )"46" nil nil )"47" nil nil )"48" nil nil )"49" nil nil )"50" nil nil )"51" nil nil )"52" nil nil )"53" nil nil )"54" nil nil )"55" nil nil )"56" nil nil )"57" nil nil )"58" nil nil )"59" nil nil )"60" nil nil )"61" nil nil )"62" nil nil )"63" nil nil )"64" nil nil )"65" nil nil )"66" nil nil )"67" nil nil )"68" nil nil )"69" nil nil )"70" nil nil )"71" nil nil )"72" nil nil )"73" nil nil )"74" nil nil )"75" nil nil )"76" nil nil )"77" nil nil )"78" nil nil )"79" nil nil )"80" nil nil )"81" nil nil )"82" nil nil )"83" nil nil )"84" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" expand "zero" )"1" nil nil ))nil )"2" expand "zero" )"2" nil nil ))nil )"3" expand "zero" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))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" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil defined_types nil )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"bool" repulsive nil )nil repulsive_iterative nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil real_types nil )nil real_types nil )"Vect2" repulsive_iterative nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil subrange_inductions nil )"bool" repulsive_iterativenil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D "vectors/" )"real" reals nil )"real" det_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"real" reals nil )nil vectors_2D "vectors/" )"real" reals nil )nil vectors_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"Vector" vectors_2D "vectors/" )"[bool, bool -> bool]" booleans nil )nil vectors_2D "vectors/" )"even_int" integersnil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"even_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(total_order?[real])" nil ))nil ))nil 3581432581"" "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" "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" "1" assert )"1" "((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" "1" expand "DF" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" case "perpR(zero) = s-s" )"1" "1" "1" case "s+zero = perpR(-perpR(s))" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "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" "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(ss,vv,epsi)(ww) IFF repulsive_criteria(DF(ss),tp*DF(vv),epsi)(tp*DF(ww)))" )"1" "1" "1" case "NOT (repulsive_criteria(DF(ss), tp * DF(vv), epsi) ") "1" "1" "repulsive_criteria_scal_nv" )"1" case "DF(ss)*DF(vv)>=0" )"1" "tp" "epsi" "DF(ww)" "DF(ss)" "(tp)*DF(vv)" )"1" assert )"1" "1" "1" "tp" )"1" assert )nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" "2" "2" expand "repulsive_criteria" )"2" assert )"2" "1" "1" assert )"1" "1" "1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil )"2" "tp" )"2" nil nil ))nil )"3" "tp" )"3" nil nil ))nil )"4" "tp" )"4" "tp" )"4" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "tp" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" case "DF(ww) = (1/tp)*(tp*DF(ww))" )"1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "1/tp" )"2" nil nil ))nil )"3" "1/tp" )"3" nil nil ))nil )"4" "4" "1" "1/tp" )"1" nil nil ))nil )"2" "1/tp" )"2" "1/tp" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "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" "1" "1" assert )"1" "1" assert )"1" "sqv(s)" )"1" assert )nil nil ))nil ))nil )"2" "sqv(s)" )"2" assert )nil nil ))nil )"3" "3" "1" "1" "1" "sqv(s)" )"1" assert )nil nil ))nil )"2" "sqv(s)" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "1" "sqv(s)" )"1" assert )nil nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" "sqv(s)" )"3" assert )nil nil ))nil ))nil )"4" "sqv(s)" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1/sqv(s)" )"1" assert )nil nil )"2" "1" nil nil )"2" nil nil ))nil ))nil )"2" "1/sqv(s)" )"1" assert )nil nil )"2" nil nil ))nil )"3" "3" "1" "1" assert )"1" "1" "1/sqv(s)" )"1" assert )nil nil )"2" nil nil ))nil )"2" "1/sqv(s)" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "1" assert )nil nil ))nil )"2" "2" "2" assert )"2" case "DF(zero) = zero" )"1" assert )"1" "1/sqv(s)" )"1" assert )nil nil )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "DF" )"2" expand "zero" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "vv" )"3" assert )"3" "1/sqv(s)" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"4" "1/sqv(s)" )"1" assert )nil nil )"2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "det_perpR" "2" case "perpR(DF(w2)) = DF(perpR(w2))" )"1" "1" rewrite "Hlem" "1" rewrite "det_perpR" nil nil ))nil ))nil )"2" "2" expand "DF" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1" "1" "1" expand "DF" )"1" expand "zero" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "sqv_eq_0" )"2" "DF(Wp)" )"2" assert )"2" expand "sqv" )"2" rewrite "Hlem" )"2" "2" "sqv_eq_0" )"2" "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" "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" "1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" assert )"2" case "NOT timestep * (DF(s) * DF(v)) >= 0" )"1" "1/timestep" )"1" assert )"1" rewrite "Hlem" -1)"1" assert )"1" case "FORALL (egv:real): 0*egv=0" )"1" rewrite -1)"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):") "1" "1" "1" expand "repulsive_criteria_iterative" )"1" rewrite "1" "1" assert )"1" "1" "m" )"1" assert )"1" case "man_pos_seq(DF(s), LAMBDA ") "1" "1" rewrite nil nil ))nil )"2" "2" case "FORALL (mm:nat): man_pos_seq(DF(s), 1, LAMBDA (ii: posnat): timestep * DF(velseq(ii)))") "1" "m" )nil nil )"2" "2" "mm" )"1" assert )"1" expand "man_pos_seq" )"1" nil nil ))nil ))nil )"2" "2" assert )"2" expand "man_pos_seq" "2" "2" "2" expand "DF" )"2" "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" "2" "m" )"2" "2" assert )"2" rewrite "2" assert )"2" "2" assert )"2" case "man_pos_seq(DF(s), LAMBDA ") "1" "1" case "FORALL (ww1,ww2:Vect2): DF(ww1-ww2)=DF(ww1)-DF(ww2)" )"1" rewrite "1" case "(m*timestep)*DF(v) = DF((m*timestep)*v)" )"1" "1" assert )"1" "1" "1" assert )"1" rewrite nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "DF" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "DF" )"2" 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" "m" )nil nil )"2" "2" "mm" )"1" assert )"1" expand "man_pos_seq" )"1" nil nil ))nil ))nil )"2" "2" assert )"2" expand "man_pos_seq" "2" "2" "2" expand "DF" )"2" "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 )nil vectors_2D "vectors/" )nil basis_2D "vectors/" )nil real_types nil )nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"[bool, bool -> bool]" booleans nil )"bool" repulsive nil )"Vector" vectors_2D "vectors/" )nil extra_real_props nil )"Vect2" repulsive_iterative nil )nil vectors_2D "vectors/" )nil extra_real_propsnil )nil real_props nil )nil det_2D "vectors/" )nil vectors_2D "vectors/" )nil real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nnreal" nil )nil extra_real_propsnil )"(total_order?[real])" nil )"posreal" nil )"bool" reals nil )nil real_props nil )"real" det_2D "vectors/" )nil vectors_2D "vectors/" )nil real_props nil )nil repulsive nil )"bool" repulsive_iterativenil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"Vect2" repulsive_iterative nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil naturalnumbers nil )nil defined_types nil )nil naturalnumbers nil )"odd_int" integers nil )"posint" nil )"int" integers nil )"int" integers nil )nil integers nil )nil integers nil )nil repulsive_iterative nil )nil real_props nil )nil reals nil )nil real_props nil )"bool" vectors_2D "vectors/" )"[Vect2 -> [# x: real, y: real #]]" nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil basis_2D "vectors/" )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" perpendicular_2D "vectors/" )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil repulsive_iterative nil ))nil ))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" "newv" "LAMBDA (n:nat): eps*perpR(s) - (1/(n+1))*s" )"2" case "FORALL (n:nat): repulsive_criteria_iterative(s, newv(n), timestep, velseq, Nsteps, eps)" )"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 ") "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" "n" )"1" "m" )"1" assert )"1" "1" "1" expand "repulsive_criteria" "1" case "s*newv(n)<0" )"1" (assert ) nil nil )"2" case "s = zero" )"1" "1" assert )nil nil ))nil )"2" "2" expand "newv" )"2" case "sqv(s)>0" )"1" "1/(1+n)" )"1" nil nil ))nil )"2" "sqv_eq_0" )"2" "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" "1" expand "V" )"1" "eps" )"1" (grind) nil nil ))nil ))nil ))nil )"2" expand "newv" -2)"2" "2" case "s = zero" )"1" "1" (assert ) nil nil ))nil )"2" "2" case "EXISTS (n:nat): (1/(1+n)) *(eps*det(vv,s)) <= eps*det(vv,V)" )"1" "1" "n" )"1" (grind) nil nil ))nil ))nil )"2" "2" case "FORALL (aa:real,bb:posreal): EXISTS (n:nat): (1/(1+n))*aa<=bb" )"1" "1" assert )nil nil ))nil )"2" "2" "2" case "aa<=0" )"1" "1" )"1" assert )nil nil ))nil )"2" "archimedean" )"2" "bb/aa" )"1" "1" "n-1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "1" nil nil )"2" 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)): ") "1" (hide (-2 -3))"1" "1" expand "repulsive_criteria" )"1" case "NOT FORALL (n:nat): (s * newv(n) < 0 AND eps * det(velseq(m), newv(n)) < 0)" )"1" "1" "n!1" )"1" "m" )"1" assert )"1" "1" assert )"1" replace 1)"1" "1" "1" case "sqv(s)>0" )"1" "(1/(1+n!1))" )"1" expand "newv" )"1" nil nil ))nil ))nil )"2" "sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "newv" -1)"2" "2" case "EXISTS (n:nat): (1/(1+n))*(eps*det(velseq(m),s)) <= -(s*velseq(m))" )"1" "1" "n!1" )"1" "1" "eps" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (aa:real,bb:posreal): EXISTS (n:nat): (1/(1+n))*aa<=bb" )"1" "1" assert )nil nil ))nil )"2" "2" "2" case "aa<=0" )"1" "1" )"1" assert )nil nil ))nil )"2" "archimedean" )"2" "bb/aa" )"1" "1" "n!1-1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "1" nil nil )"2" nil nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "Nsteps" "eps" "s" "timestep" "newv(n!1)" "velseq" )"2" assert )"2" "n!1" )"2" assert )"2" "1" "m!1" )"1" (assert ) nil nil ))nil )"2" "szero" )"2" "2" expand "newv" )"2" case "sqv(s)>0" )"1" "1/(1+n!1)" )"1" nil nil ))nil )"2" "sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "Nsteps" "eps" "s" "timestep" "newv(n)" "velseq" )"2" assert )"2" "1" "m" )"1" (assert ) nil nil ))nil )"2" "2" "2" expand "newv" )"2" case "sqv(s)>0" )"1" "1/(1+n)" )"1" (grind) nil nil ))nil )"2" "szero" )"2" "sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "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" "1" assert )"1" "1" case "sqv(s)>0" )"1" "1/(1+n)" )"1" "1" expand "newv" )"1" (grind) nil nil ))nil ))nil ))nil )"2" "sqv_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" assert )"2" "2" case "NOT s*newv(n)<0" )"1" "1" expand "newv" 1)"1" case "sqv(s)>0" )"1" "1/(1+n)" )"1" nil nil ))nil )"2" "sqv_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "newv" )"2" "eps" )"2" "1/(1+n)" )"2" 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 )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil integers nil )nil integers nil )nil repulsive_iterative nil )"bool" repulsive_iterativenil )"posint" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"real" vectors_2D "vectors/" )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" repulsive nil )"Vect2" repulsive_iterative nil )"[bool, bool -> bool]" booleans nil )"Vector" repulsive_iterative nil )"Sign" repulsive_iterative nil )nil real_props nil )nil real_props nil )nil extra_real_props nil )"int" integers nil )"nzrat" rationalsnil )"real" reals nil )nil real_props nil )nil real_props nil )nil reals nil )nil real_props nil )"posreal" nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"posreal" repulsive_iterative nil )"real" repulsive_iterative nil )"nzreal" nil )"even_int" integersnil )"odd_int" integers nil )"(total_order?[real])" nil )"Vector" repulsive_iterative nil )"[nat -> Vector]" repulsive_iterative nil )nil vectors_2D "vectors/" )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"real" reals nil )"nonneg_rat" nil )"real" reals nil )"real" reals nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"(strict_total_order?[real])" real_props nil )"real" det_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"subrange(1, Nsteps)" repulsive_iterative nil )"posnat" repulsive_iterative nil )"VelSeq" repulsive_iterative nil )"Vect2" repulsive_iterative nil )"posreal" repulsive_iterative nil )"real" repulsive_iterative nil )nil nil )nil real_props nil )"posint" nil )"posrat" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil sign "reals/" )"Vect2" perpendicular_2D "vectors/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))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" "1" assert )"1" case "NOT s*velseq(1)>=0" )"1" (ground) nil nil )"2" "t" )"2" assert )"2" case "v = zero" )"1" "1" (assert ) nil nil ))nil )"2" assert )"2" "t" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "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" "2" "DV" "man_pos_seq(s, timestep, velseq)(mm) - s" )"2" replace -1)"2" "mm" )"2" "2" "2" assert )"2" "2" "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" "(t - mm * timestep + timestep)" )"1" "1" expand "DV" )"1" "man_pos_seq" ))nil nil ))nil ))nil ))nil )"2" "2" expand "repulsive_criteria" "2" "2" case "v = zero" )"1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "repulsive_criteria" "2" case "(mm * timestep - timestep) * v = zero" )"1" replace "1" assert )nil nil ))nil )"2" "2" "1" "1" "(mm-1)*timestep" )"1" assert )nil nil )"2" "nnreal_times_nnreal_is_nnreal" )"2" "mm-1" "timestep" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "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" "1" nil nil ))nil ))nil )"2" "2" "2" "1/timestep" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "mm" )"2" expand "min" )"2" "2" "2" "2" assert )"2" "1" "timestep" )"1" assert )nil nil ))nil )"2" "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 )"nat" floor_ceil nil )"{k: posint | k <= i AND k <= j}" nil )"posreal" nil )"Vect2" repulsive_iterative nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{k: posint | k <= 1 + floor(t / timestep) AND k <= Nsteps}" nil )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )nil real_props nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"posnat" repulsive_iterative nil )"posreal" repulsive_iterative nil )"posreal" repulsive_iterative nil )"Vector" repulsive_iterative nil )"Vector" vectors_2D "vectors/" )nil real_types nil )"Vector" vectors_2D "vectors/" )nil repulsive_iterative nil )"Vect2" repulsive_iterative nil )"bool" repulsive_iterativenil )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil repulsive_iterative nil )"nnreal" nil )nil real_props nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil extra_real_propsnil )"(total_order?[real])" nil )"bool" repulsive nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"even_int" integersnil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"posreal" nil )"posint" nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil integers nil )nil integers nil )nil integers nil )nil integers nil ))nil )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" "mps" "man_pos_seq(s, timestep, velseq)(k)" )"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" "eps" )"1" "1" rewrite "vx_distr_add" )"1" rewrite "vy_distr_add" )"1" rewrite "vx_scal" )"1" rewrite "vy_scal" )"1" expand "*" )"1" expand "+" )"1" "rd" "velseq(k)" )"1" "1" "dv" "velseq(1+k)" )"1" "1" assert )"1" "1" assert )"1" rewrite "vx_distr_sub" )"1" rewrite "vy_distr_sub" )"1" assert )"1" "1" "1" assert )"1" "timestep" )"1" "1" nil )))))))))"2"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.754 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
2026-05-26
