|
(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)) >= 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"
(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,timestep,velseq)(ii))")
(("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)) >= norm(s)")
(("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) * velseq(ii+1) >= 0")
(("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: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"
(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"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.112 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
