|
(cd_vertical
(cd_vertical_rewrite 0
(cd_vertical_rewrite-2 nil 3477047766
("" (skeep)
(("" (expand "cd_vertical?")
((""
(case "vz/=0 IMPLIES (min(max(-H - sign(vz) * sz, B * abs(vz)), T * abs(vz))>=0 AND min(max(Theta_H(sz,vz, -1), B), T)>=0)")
(("1"
(case "vz /= 0 IMPLIES (min(max(Theta_H(sz, vz, -1), B), T)*abs(vz) = min(max(-H - sign(vz) * sz, B * abs(vz)), T * abs(vz)) AND
max(min(Theta_H(sz, vz, 1), T), B)*abs(vz) = max(min(H - sign(vz) * sz, T * abs(vz)), B * abs(vz)))")
(("1" (split +)
(("1" (flatten)
(("1" (split -1)
(("1" (propax) nil nil)
("2" (flatten)
(("2" (assert)
(("2" (flatten)
(("2" (mult-by 3 "abs(vz)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split -)
(("1" (propax) nil nil)
("2" (flatten)
(("2" (assert)
(("2" (flatten)
(("2" (mult-by -1 "abs(vz)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (flatten)
(("2" (lemma "nneg_mult_min")
(("2"
(inst - "abs(vz)" "max(Theta_H(sz, vz, -1), B)" "T")
(("1" (replace -1)
(("1" (hide -1)
(("1" (lemma "nneg_mult_max")
(("1"
(inst - "abs(vz)"
"min(Theta_H(sz, vz, 1), T)" "B")
(("1" (replace -1)
(("1" (hide -1)
(("1"
(rewrite "nneg_mult_min")
(("1"
(rewrite "nneg_mult_max")
(("1"
(case "vz>0")
(("1"
(expand "abs")
(("1"
(expand "sign")
(("1"
(assert)
(("1" (grind) nil nil))
nil))
nil))
nil)
("2"
(expand "abs")
(("2"
(expand "sign")
(("2"
(assert)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (flatten)
(("2" (lemma "nnreal_times_nnreal_is_nnreal")
(("2" (inst - "B" "abs(vz)")
(("2" (lemma "nnreal_times_nnreal_is_nnreal")
(("2" (inst - "T" "abs(vz)")
(("2" (grind :exclude ("Theta_H" "sign" "abs")) nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(cd_vertical? const-decl "bool" cd_vertical nil)
(nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vz skolem-const-decl "real" cd_vertical nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(< const-decl "bool" reals nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nneg_mult_max formula-decl nil min_max "reals/")
(nneg_mult_min formula-decl nil min_max "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(max 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)
(- const-decl "[numfield -> numfield]" number_fields 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)
(H formal-const-decl "posreal" cd_vertical 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)
(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 "[T, T -> boolean]" equalities nil)
(Sign type-eq-decl nil sign "reals/")
(sign const-decl "Sign" sign "reals/")
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" cd_vertical nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(T formal-const-decl "{AB: posreal | AB > B}" cd_vertical nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Theta_H const-decl "real" vertical nil))
nil)
(cd_vertical_rewrite-1 nil 3477047745 ("" (postpone) nil nil) nil
shostak))
(cd_vertical_correct 0
(cd_vertical_correct-2 "" 3504842549
("" (skeep)
(("" (rewrite "cd_vertical_rewrite")
(("" (split -)
(("1" (expand "conflict_vertical?")
(("1" (flatten)
(("1" (inst + "B") (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (flatten)
(("2" (expand "max")
(("2" (expand "min")
(("2" (lemma "Theta_H_lt")
(("2" (inst?)
(("1" (lemma "vertical_los_inside_Theta")
(("1" (expand "conflict_vertical?")
(("1" (lift-if)
(("1" (case "Theta_H(sz, vz, 1) > T")
(("1" (assert)
(("1" (ground)
(("1"
(inst + "B")
(("1"
(inst - "vz" "sz" "B")
(("1" (assert) nil nil))
nil))
nil)
("2"
(lift-if)
(("2"
(assert)
(("2"
(ground)
(("2"
(inst + "T")
(("2"
(inst - "vz" "sz" "T")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lift-if)
(("2"
(assert)
(("2"
(ground)
(("1"
(inst + "B")
(("1"
(inst - "vz" "sz" "B")
(("1" (assert) nil nil))
nil))
nil)
("2"
(inst
+
"Theta_H(sz,vz,-1)/2 + Theta_H(sz,vz,1)/2")
(("2"
(inst
-
"vz"
"sz"
"Theta_H(sz,vz,-1)/2 + Theta_H(sz,vz,1)/2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cd_vertical_rewrite formula-decl nil cd_vertical nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(/= const-decl "boolean" notequal nil)
(vz skolem-const-decl "real" cd_vertical nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(Theta_H const-decl "real" vertical nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(vertical_los_inside_Theta formula-decl nil vertical nil)
(Theta_H_lt formula-decl nil vertical nil)
(H formal-const-decl "posreal" cd_vertical nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(conflict_vertical? const-decl "bool" cd_vertical nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(B formal-const-decl "nnreal" cd_vertical 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)
(T formal-const-decl "{AB: posreal | AB > B}" cd_vertical nil)
(Lookahead type-eq-decl nil Lookahead nil))
shostak)
(cd_vertical_correct-1 nil 3477048337
("" (skeep)
(("" (rewrite "cd_vertical_rewrite")
(("" (split -)
(("1" (expand "conflict_vertical?")
(("1" (flatten)
(("1" (inst + "B") (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (flatten)
(("2" (expand "max")
(("2" (expand "min")
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (assert)
(("2" (lemma "Theta_H_lt")
(("2"
(inst?)
(("2"
(lemma "vertical_los_inside_Theta")
(("2"
(expand "conflict_vertical?")
(("2"
(ground)
(("1"
(inst + "B")
(("1"
(inst - "vz" "sz" "B")
(("1" (assert) nil nil))
nil))
nil)
("2"
(inst + "T")
(("2"
(inst - "vz" "sz" "T")
(("2" (assert) nil nil))
nil))
nil)
("3"
(inst + "B")
(("3"
(inst - "vz" "sz" "B")
(("3" (assert) nil nil))
nil))
nil)
("4"
(inst
+
"Theta_H(sz,vz,-1)/2 + Theta_H(sz,vz,1)/2")
(("4"
(inst
-
"vz"
"sz"
"Theta_H(sz,vz,-1)/2 + Theta_H(sz,vz,1)/2")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Theta_H const-decl "real" vertical nil)
(Sign type-eq-decl nil sign "reals/")
(vertical_los_inside_Theta formula-decl nil vertical nil)
(Theta_H_lt formula-decl nil vertical nil)
(Lookahead type-eq-decl nil Lookahead nil))
shostak))
(cd_vertical_complete 0
(cd_vertical_complete-1 nil 3477048596
("" (skeep)
(("" (rewrite "cd_vertical_rewrite")
(("" (flatten)
(("" (expand "conflict_vertical?")
(("" (skosimp*)
(("" (case "vz = 0")
(("1" (replace -1) (("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (assert)
(("2" (lemma "vertical_los_inside_Theta")
(("2" (inst - "vz" "sz" "t!1")
(("2" (assert)
(("2" (flatten)
(("2" (typepred "t!1")
(("2" (grind :exclude "Theta_H") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cd_vertical_rewrite formula-decl nil cd_vertical nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(conflict_vertical? const-decl "bool" cd_vertical nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(Lookahead type-eq-decl nil Lookahead nil)
(T formal-const-decl "{AB: posreal | AB > B}" cd_vertical nil)
(B formal-const-decl "nnreal" cd_vertical nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(minus_real_is_real application-judgement "real" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(H formal-const-decl "posreal" cd_vertical 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)
(bool nonempty-type-eq-decl nil booleans nil)
(vertical_los_inside_Theta formula-decl nil vertical nil))
shostak))
(cd_vertical 0
(cd_vertical-1 nil 3477048859
("" (skeep)
(("" (split)
(("1" (flatten) (("1" (rewrite "cd_vertical_complete") nil nil))
nil)
("2" (flatten) (("2" (rewrite "cd_vertical_correct") nil nil))
nil))
nil))
nil)
((cd_vertical_complete formula-decl nil cd_vertical nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(cd_vertical_correct formula-decl nil cd_vertical nil))
shostak))
(conflict_vertical_on_open_interval 0
(conflict_vertical_on_open_interval-1 nil 3477048939
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (rewrite "cd_vertical")
(("1" (lemma "cd_vertical_rewrite")
(("1" (inst?)
(("1" (replace -1)
(("1" (hide -1)
(("1" (split)
(("1" (flatten)
(("1" (inst + "B/2 + T/2")
(("1" (assert)
(("1" (hide -) (("1" (grind-reals) nil nil))
nil))
nil)
("2" (assert)
(("2" (split)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(name "newt"
"(min(max(Theta_H(sz, vz, -1), B), T) +
max(min(Theta_H(sz, vz, 1), T), B))/2")
(("2" (lemma "Theta_H_lt")
(("2" (inst?)
(("2" (lemma "vertical_los_inside_Theta")
(("2"
(inst - "vz" "sz" "newt")
(("2"
(inst + "newt")
(("1"
(grind :exclude "Theta_H")
nil
nil)
("2"
(replace -3 :dir rl)
(("2"
(hide -)
(("2"
(grind :exclude "Theta_H")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (skosimp*)
(("2" (expand "conflict_vertical?")
(("2" (inst + "topen!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((cd_vertical formula-decl nil cd_vertical nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Theta_H_lt formula-decl nil vertical nil)
(vertical_los_inside_Theta formula-decl nil vertical nil)
(newt skolem-const-decl "real" cd_vertical nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(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/")
(H formal-const-decl "posreal" cd_vertical nil)
(Theta_H const-decl "real" vertical 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)
(Lookahead type-eq-decl nil Lookahead nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(B formal-const-decl "nnreal" cd_vertical nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
(T formal-const-decl "{AB: posreal | AB > B}" cd_vertical nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cd_vertical_rewrite formula-decl nil cd_vertical nil)
(conflict_vertical? const-decl "bool" cd_vertical nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak)))
¤ Dauer der Verarbeitung: 0.36 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.
|
