|
(vs_bands
(vs_bands_vertical_dir_exclusive 0
(vs_bands_vertical_dir_exclusive-1 nil 3477244353
("" (skeep)
(("" (split +)
(("1" (flatten)
(("1" (split -)
(("1" (flatten)
(("1" (replace -1)
(("1" (hide -1)
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "abs")
(("1" (lift-if)
(("1" (split -2)
(("1" (flatten)
(("1" (neg-formula -2)
(("1"
(replace -1)
(("1"
(case "vsp - viz < 0")
(("1"
(case "sz + B*(vsp-viz) > -H")
(("1"
(copy 2)
(("1"
(expand "conflict_vertical?")
(("1"
(inst + "B")
(("1"
(case
"sz + B*(vsp-viz) >= H")
(("1"
(name
"newt"
"-sz/(vsp-viz)")
(("1"
(case
"B <= newt and newt <= T")
(("1"
(flatten)
(("1"
(inst + "newt")
(("1"
(case
"sz + newt*(vsp-viz) = 0")
(("1"
(assert)
nil)
("2"
(replace
-3
:dir
rl)
(("2"
(name
"const3"
"vsp-viz")
(("2"
(replace
-1)
(("2"
(both-sides
"-"
"sz"
1)
(("1"
(assert)
(("1"
(cross-mult
1)
nil)))
("2"
(assert)
nil)))))))))))
("2"
(assert)
nil)))))
("2"
(replace -1 :dir rl)
(("2"
(split 1)
(("1"
(cross-mult 1)
(("1"
(typepred "T")
(("1"
(mult-by
-3
"viz-vsp")
(("1"
(assert)
nil)))))))
("2"
(cross-mult 1)
(("2"
(typepred "T")
(("2"
(mult-by
-3
"viz-vsp")
(("2"
(assert)
nil)))))))))))))
("2" (assert) nil)))
("2"
(expand "abs" 2)
(("2"
(lift-if)
(("2"
(ground)
nil)))))))))))))
("2"
(mult-by -1 "T-B")
(("2" (assert) nil)))))
("2"
(mult-by 2 "H")
(("2"
(mult-by 1 "H")
(("2" (assert) nil)))))))))))))
("2" (flatten)
(("2" (replace -1)
(("2"
(case "vsp > viz")
(("1"
(case "sz + B*(vsp-viz) < H")
(("1"
(hide 1)
(("1"
(copy 2)
(("1"
(expand "conflict_vertical?")
(("1"
(inst + "B")
(("1"
(case
"sz + B*(vsp-viz) <= -H")
(("1"
(name
"newt"
"-sz/(vsp-viz)")
(("1"
(case
"B <= newt and newt <= T")
(("1"
(flatten)
(("1"
(inst + "newt")
(("1"
(case
"sz + newt*(vsp-viz) = 0")
(("1"
(assert)
nil)
("2"
(replace
-3
:dir
rl)
(("2"
(name
"const3"
"vsp-viz")
(("2"
(replace
-1)
(("2"
(both-sides
"-"
"sz"
1)
(("1"
(assert)
(("1"
(cross-mult
1)
nil)))
("2"
(assert)
nil)))))))))))
("2"
(assert)
nil)))))
("2"
(replace -1 :dir rl)
(("2"
(split 1)
(("1"
(cross-mult 1)
(("1"
(typepred "T")
(("1"
(mult-by
-3
"vsp-viz")
(("1"
(assert)
nil)))))))
("2"
(cross-mult 1)
(("2"
(typepred "T")
(("2"
(mult-by
-3
"vsp-viz")
(("2"
(assert)
nil)))))))))))))
("2" (assert) nil)))
("2"
(expand "abs" 2)
(("2"
(lift-if)
(("2"
(ground)
nil)))))))
("2" (assert) nil)))))))))
("2"
(typepred "T")
(("2"
(mult-by -3 "vsp-viz")
(("2" (assert) nil)))))))
("2"
(mult-by 1 "H")
(("2"
(mult-by 3 "H")
(("2"
(assert)
nil)))))))))))))))))))))))))))
("2" (flatten)
(("2" (replace -1)
(("2" (hide -1)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "abs")
(("2" (lift-if)
(("2" (split -)
(("1" (flatten)
(("1" (neg-formula -2)
(("1"
(replace -1)
(("1"
(case "vsp>viz")
(("1"
(case "sz + T*(vsp-viz) > -H")
(("1"
(copy 2)
(("1"
(expand "conflict_vertical?")
(("1"
(inst + "T")
(("1"
(case
"sz + T*(vsp-viz) >= H")
(("1"
(name
"newt"
"-sz/(vsp-viz)")
(("1"
(case
"B <= newt and newt <= T")
(("1"
(flatten)
(("1"
(case
"sz + newt*(vsp-viz) = 0")
(("1"
(inst + "newt")
(("1"
(assert)
nil)
("2"
(assert)
nil)))
("2"
(replace
-3
:dir
rl)
(("2"
(name
"const3"
"vsp-viz")
(("2"
(replace -1)
(("2"
(both-sides
"-"
"sz"
1)
(("1"
(assert)
(("1"
(cross-mult
1)
nil)))
("2"
(assert)
nil)))))))))))))
("2"
(replace -1 :dir rl)
(("2"
(split +)
(("1"
(cross-mult 1)
(("1"
(typepred "T")
(("1"
(mult-by
-2
"vsp-viz")
(("1"
(assert)
nil)))))))
("2"
(cross-mult 1)
(("2"
(typepred "T")
(("2"
(mult-by
-3
"vsp-viz")
(("2"
(assert)
nil)))))))))))))
("2" (assert) nil)))
("2"
(expand "abs" 2)
(("2"
(lift-if)
(("2"
(ground)
nil)))))))
("2" (assert) nil)))))))
("2"
(typepred "T")
(("2"
(mult-by -3 "vsp-viz")
(("2" (assert) nil)))))))
("2"
(mult-by 1 "H")
(("2"
(mult-by 2 "H")
(("2" (assert) nil)))))))))))))
("2" (flatten)
(("2" (replace -1)
(("2"
(hide 1)
(("2"
(case "vsp < viz")
(("1"
(case "sz + T*(vsp-viz) < H")
(("1"
(copy 2)
(("1"
(expand "conflict_vertical?")
(("1"
(inst + "T")
(("1"
(case
"sz + T*(vsp-viz) <= -H")
(("1"
(name
"newt"
"-sz/(vsp-viz)")
(("1"
(case
"B <= newt and newt <= T")
(("1"
(flatten)
(("1"
(case
"sz + newt*(vsp-viz) = 0")
(("1"
(inst + "newt")
(("1"
(assert)
nil)
("2"
(assert)
nil)))
("2"
(replace
-3
:dir
rl)
(("2"
(name
"const3"
"vsp-viz")
(("2"
(replace -1)
(("2"
(both-sides
"-"
"sz"
1)
(("1"
(assert)
(("1"
(cross-mult
1)
nil)))
("2"
(assert)
nil)))))))))))))
("2"
(replace -1 :dir rl)
(("2"
(split +)
(("1"
(cross-mult 1)
(("1"
(typepred "T")
(("1"
(mult-by
-3
"viz-vsp")
(("1"
(assert)
nil)))))))
("2"
(cross-mult 1)
(("2"
(typepred "T")
(("2"
(mult-by
-3
"viz-vsp")
(("2"
(assert)
nil)))))))))))))
("2" (assert) nil)))
("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil)))))))
("2" (assert) nil)))))))
("2"
(typepred "T")
(("2"
(mult-by -3 "viz-vsp")
(("2" (assert) nil)))))))
("2"
(mult-by 1 "H")
(("2"
(mult-by 2 "H")
(("2"
(assert)
nil)))))))))))))))))))))))))))))))))
("2" (flatten)
(("2" (case "vsp - viz = 0")
(("1" (replace -1) (("1" (assert) nil)))
("2" (replace 1)
(("2" (split -)
(("1" (flatten)
(("1" (replace -1)
(("1" (hide -1)
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "abs")
(("1" (lift-if)
(("1" (split -)
(("1"
(flatten)
(("1"
(expand "conflict_vertical?")
(("1"
(skosimp*)
(("1"
(neg-formula -2)
(("1"
(replace -1)
(("1"
(case "vsp < viz")
(("1"
(mult-by -1 "H")
(("1" (assert) nil)))
("2"
(mult-by 1 "T-t!1")
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil)))))))))))))))))))
("2"
(flatten)
(("2"
(replace -1)
(("2"
(case "vsp > viz")
(("1"
(mult-by -1 "H")
(("1" (assert) nil)))
("2"
(expand "conflict_vertical?")
(("2"
(skosimp*)
(("2"
(mult-by 1 "T-t!1")
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil)))))))))))))))))))))))))))))))))
("2" (flatten)
(("2" (replace -1)
(("2" (hide -1)
(("2" (replace -1)
(("2" (hide -1)
(("2" (expand "abs")
(("2" (lift-if)
(("2" (split -)
(("1"
(flatten)
(("1"
(neg-formula -2)
(("1"
(replace -1)
(("1"
(case "vsp > viz")
(("1"
(mult-by -1 "H")
(("1" (assert) nil)))
("2"
(expand "conflict_vertical?")
(("2"
(skosimp*)
(("2"
(mult-by 1 "t!1-B")
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil)))))))))))))))))))
("2"
(flatten)
(("2"
(replace -1)
(("2"
(case "vsp < viz")
(("1"
(mult-by -1 "H")
(("1" (assert) nil)))
("2"
(expand "conflict_vertical?")
(("2"
(skosimp*)
(("2"
(mult-by 1 "t!1-B")
(("2"
(expand "abs")
(("2"
(lift-if)
(("2"
(ground)
nil))))))))))))))))))))))))))))))))))))))))))))
nil)
((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(mult_neg formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(H formal-const-decl "posreal" vs_bands nil)
(T formal-const-decl "{AB: posreal | AB > B}" vs_bands nil)
(B formal-const-decl "nnreal" vs_bands nil)
(nnreal type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(number nonempty-type-decl nil numbers nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(< const-decl "bool" reals nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Lookahead type-eq-decl nil Lookahead nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(div_mult_neg_le1 formula-decl nil real_props nil)
(div_mult_neg_le2 formula-decl nil real_props nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(viz skolem-const-decl "real" vs_bands nil)
(vsp skolem-const-decl "real" vs_bands nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs_nat formula-decl nil abs_lems "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(newt skolem-const-decl "real" vs_bands nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(conflict_vertical? const-decl "bool" cd_vertical nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(both_sides_times1 formula-decl nil real_props nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(div_cancel2 formula-decl nil real_props nil)
(newt skolem-const-decl "real" vs_bands nil)
(newt skolem-const-decl "real" vs_bands nil)
(newt skolem-const-decl "real" vs_bands nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(band_critical_on_H 0
(band_critical_on_H-3 "stop infinite loop on mult-by -1" 3508591107
("" (skeep)
(("" (case "B = 0")
(("1" (replace -1)
(("1" (assert)
(("1" (hide -1)
(("1" (expand "sign" -3)
(("1" (case "T * vsp1 - T * viz + sz >= 0")
(("1" (assert)
(("1" (lift-if)
(("1" (ground)
(("1" (expand "abs" (-1 -2 -3 -4))
(("1" (hide -1)
(("1" (hide -1)
(("1" (case "sz + tlh*(vsp2-viz) < H")
(("1"
(hide -4)
(("1"
(name "newt" "(H-sz+T*viz)/T")
(("1"
(case "sz + T*(newt-viz) = H")
(("1"
(inst + "newt")
(("1"
(expand "abs" +)
(("1"
(assert)
(("1"
(lemma
"vs_bands_vertical_dir_exclusive")
(("1"
(inst
-
"T"
"1"
"sz"
"viz"
"newt")
(("1"
(expand "abs" -1)
(("1"
(expand
"conflict_vertical?")
(("1"
(skosimp*)
(("1"
(case
"newt-viz = (H-sz)/T")
(("1"
(mult-by
-1
"t!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(case
"sz + ((H-sz)/T)*t!1)
(("1"
(hide
-2)
(("1"
(mult-by
-1
"T")
(("1"
(mult-by
-5
"T-t!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand
"abs"
-1)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-3
:dir
rl)
(("2"
(mult-by
1
"T")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "vsp2 < viz")
(("1"
(case
"sz + T*(vsp2-viz) < H")
(("1"
(typepred "band")
(("1"
(inst
-
"vsp2"
"vsp1"
"newt")
(("1"
(assert)
(("1"
(replace -4 :dir rl)
(("1"
(split 1)
(("1"
(cross-mult 1)
nil
nil)
("2"
(cross-mult 1)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(mult-by -1 "T-tlh")
(("2" (assert) nil nil))
nil))
nil)
("2"
(mult-by 1 "tlh")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(replace -1 :dir rl)
(("2"
(mult-by 1 "T")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "abs")
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (ground)
(("2" (expand "abs" (-1 -2))
(("2" (neg-formula -1)
(("2" (neg-formula -2)
(("2" (case "sz + tlh*(vsp2-viz) > -H")
(("1" (assert)
(("1" (case "sz >= 0")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(hide -4)
(("2"
(name "newt" "(-H-sz+T*viz)/T")
(("2"
(case "sz + T*(newt-viz) = -H")
(("1"
(inst + "newt")
(("1"
(expand "abs" +)
(("1"
(assert)
(("1"
(lemma
"vs_bands_vertical_dir_exclusive")
(("1"
(inst
-
"T"
"1"
"sz"
"viz"
"newt")
(("1"
(expand "abs" -1)
(("1"
(expand
"conflict_vertical?")
(("1"
(skosimp*)
(("1"
(case
"newt-viz = (-H-sz)/T")
(("1"
(case
"newt*t!1 - viz*t!1 = (-H - sz) / T*t!1")
(("1"
(hide -2)
(("1"
(hide -1)
(("1"
(case
"sz + ((-H-sz)/T)*t!1>-H")
(("1"
(hide
-2)
(("1"
(case
" sz*T + ((-H - sz)) * t!1 > -H*T")
(("1"
(hide
-2)
(("1"
(mult-by
-6
"T-t!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide-all-but
(-1
1))
(("2"
(name-replace
"div_T"
"(-H - sz) / T")
(("2"
(mult-by
-1
"T")
(("2"
(expand
"div_T")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3
4)
(("2"
(replace
-3
:dir
rl
:hide?
t)
(("2"
(grind-reals)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(ground)
nil
nil))
nil)
("2"
(hide-all-but
(-1 1))
(("2"
(cross-mult
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case "vsp2 > viz")
(("1"
(case
"sz + T*(vsp2-viz) > -H")
(("1"
(typepred "band")
(("1"
(inst
-
"vsp1"
"vsp2"
"newt")
(("1"
(assert)
(("1"
(replace
-4
:dir
rl)
(("1"
(split 1)
(("1"
(cross-mult 1)
nil
nil)
("2"
(cross-mult 1)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(mult-by -1 "T-tlh")
(("2" (assert) nil nil))
nil))
nil)
("2"
(mult-by 1 "tlh")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(replace -1 :dir rl)
(("2"
(mult-by 1 "T")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "abs" -)
(("2" (lift-if) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "sign" -)
(("2" (lift-if)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "abs" (-1 -2 -3 -4))
(("1" (hide -1)
(("1" (hide -1)
(("1" (case "sz + tlh*(vsp2-viz) < H")
(("1" (hide -4)
(("1" (name "newtb" "(H-sz+B*viz)/B")
(("1" (label "newtbname" -1)
(("1"
(case "sz + B*(newtb-viz) = H")
(("1"
(name "newtt" "(H-sz+T*viz)/T")
(("1"
(label "newttname" -1)
(("1"
(case "sz + T*(newtt-viz) = H")
(("1"
(case "vsp2 >= viz")
(("1"
(case
"sz + B*(vsp2-viz) < H")
(("1"
(inst + "newtb")
(("1"
(flatten)
(("1"
(hide 3)
(("1"
(expand "abs" +)
(("1"
(assert)
(("1"
(lemma
"vs_bands_vertical_dir_exclusive")
(("1"
(inst
-
"B"
"-1"
"sz"
"viz"
"newtb")
(("1"
(expand
"abs"
-1)
(("1"
(expand
"conflict_vertical?")
(("1"
(skosimp*)
(("1"
(case
"sz + t!1*(newtb - viz) < H")
(("1"
(hide
-2)
(("1"
(case
"newtb - viz = (H-sz)/B")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(both-sides
"-"
"sz"
-1)
(("1"
(assert)
(("1"
(cross-mult
-1)
(("1"
(case
"H < sz")
(("1"
(mult-by
-4
"B")
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.46 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.
|
