Quelle vz_criteria.prf
Sprache: unbekannt
|
|
(vz_criteria
(vertical_exit_independence 0
(vertical_exit_independence-1 nil 3431703025
("" (skeep)
(("" (expand "vertical_exit_criterion?")
(("" (lemma "vertical_sep_dir")
(("" (inst?)
(("" (replaces -1)
(("" (expand "vertical_conflict?")
(("" (ground)
(("1" (skeep -2)
(("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil)
("2" (skeep 2)
(("2" (inst? 1)
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(vertical_exit_criterion? const-decl "bool" vz_criteria 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 "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(Spz type-eq-decl nil vertical nil)
(vertical_conflict? const-decl "bool" vertical nil)
(t skolem-const-decl "real" vz_criteria nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(nnreal type-eq-decl nil real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(vertical_sep_dir formula-decl nil 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)
(bool nonempty-type-eq-decl nil booleans 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)
(H formal-const-decl "posreal" vz_criteria nil))
nil))
(vertical_exit_coordination 0
(vertical_exit_coordination-2 nil 3451903387
("" (skeep)
(("" (lemma "vertical_exit_independence")
(("" (inst -1 "spz" "vz")
(("" (assert)
(("" (hide -1)
(("" (expand "vertical_exit_criterion?")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((vertical_exit_independence formula-decl nil vz_criteria nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(neg_spz application-judgement "Spz" vz_criteria nil)
(vertical_exit_criterion? const-decl "bool" vz_criteria nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(Spz type-eq-decl nil vertical nil)
(H formal-const-decl "posreal" vz_criteria nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil)
(vertical_exit_coordination-1 nil 3431792967
("" (skeep)
(("" (lemma "vertical_exit_independence")
(("" (inst -1 "spz" "voz-viz")
(("" (assert)
(("" (hide -1)
(("" (expand "vertical_exit_criterion?")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((Spz type-eq-decl nil vertical nil)) nil))
(vertical_sep_dir_at 0
(vertical_sep_dir_at-2 "" 3565298982
("" (skeep)
(("" (name-replace "s" "sz+nnt*vz" :hide? nil)
(("" (name-replace "ns" "sz+nnt*nvz" :hide? nil)
(("" (beta)
(("" (flatten)
(("" (rewrite "sign_abs")
(("" (rewrite "sign_abs")
(("" (typepred "dir")
(("" (hide -1)
(("" (split)
(("1" (replaces -1)
(("1" (hide -5)
(("1" (case "s>=0")
(("1" (rewrite "sign_eq_1")
(("1"
(real-props :simple? t)
(("1"
(cancel-by -5 "s")
(("1"
(case "ns >= s")
(("1"
(rewrite "sign_eq_1" 2)
(("1"
(assert)
(("1" (grind-reals) nil nil))
nil))
nil)
("2"
(hide 3)
(("2"
(replaces (-4 -5) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sign_eq_neg1")
(("2"
(real-props :simple? t)
(("2"
(cancel-by -4 "s")
(("2"
(case "ns <= s")
(("1"
(rewrite "sign_eq_neg1" 4)
(("1"
(assert)
(("1" (grind-reals) nil nil))
nil))
nil)
("2"
(hide 5)
(("2"
(replaces (-2 -3) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replaces -1)
(("2" (case "s>=0")
(("1" (rewrite "sign_eq_1")
(("1" (real-props :simple? t)
(("1"
(cancel-by -5 "s")
(("1"
(case "ns >= s")
(("1"
(rewrite "sign_eq_1" 2)
(("1"
(assert)
(("1"
(neg-formula 2)
(("1" (grind-reals) nil nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(replaces (-4 -5) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sign_eq_neg1")
(("2" (real-props :simple? t)
(("2"
(cancel-by -4 "s")
(("2"
(case "ns <= s")
(("1"
(rewrite "sign_eq_neg1" 4)
(("1"
(assert)
(("1"
(neg-formula 4)
(("1" (grind-reals) nil nil))
nil))
nil))
nil)
("2"
(hide 5)
(("2"
(replaces (-2 -3) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sign_abs formula-decl nil sign "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Sign type-eq-decl nil sign "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(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)
(/= const-decl "boolean" notequal nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(sign_eq_neg1 formula-decl nil sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(CBD_57 skolem-const-decl "real" vz_criteria nil)
(both_sides_times_neg_ge1_imp formula-decl nil extra_real_props
nil)
(div_mult_neg_le1 formula-decl nil real_props nil)
(both_sides_plus_le1 formula-decl nil real_props nil)
(both_sides_times_pos_le2 formula-decl nil real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(neg_one_times formula-decl nil extra_tegies nil)
(sign_eq_1 formula-decl nil sign "reals/")
(> const-decl "bool" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(CBD_56 skolem-const-decl "real" vz_criteria 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)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_le_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)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(zero_div formula-decl nil extra_tegies nil)
(ge_times_ge_pos formula-decl nil real_props nil)
(ge_plus_ge formula-decl nil real_props nil)
(pos_times_ge formula-decl nil real_props nil)
(one_times formula-decl nil extra_tegies nil)
(neg_times_ge formula-decl nil real_props nil)
(both_sides_times_neg_ge1 formula-decl nil real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_neg formula-decl nil extra_tegies nil)
(neg_neg formula-decl nil extra_tegies nil)
(both_sides_times_pos_ge2 formula-decl nil real_props nil)
(both_sides_plus_ge1 formula-decl nil real_props nil)
(CBD_58 skolem-const-decl "real" vz_criteria nil)
(neg_ge formula-decl nil real_props nil)
(le_plus_le formula-decl nil real_props nil)
(le_times_le_pos formula-decl nil real_props nil)
(CBD_59 skolem-const-decl "real" vz_criteria nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak)
(vertical_sep_dir_at-1 nil 3432124634
("" (skeep)
(("" (name-replace "s" "sz+nnt*vz" :hide? nil)
(("" (name-replace "ns" "sz+nnt*nvz" :hide? nil)
(("" (beta)
(("" (flatten)
(("" (rewrite "sign_abs")
(("" (rewrite "sign_abs")
(("" (typepred "dir")
(("" (hide -1)
(("" (split)
(("1" (replaces -1)
(("1" (hide -5)
(("1" (case "s>=0")
(("1" (rewrite "sign_eq_1")
(("1"
(cancel-by -5 "s")
(("1"
(case "ns >= s")
(("1"
(rewrite "sign_eq_1" 2)
(("1"
(assert)
(("1" (grind-reals) nil nil))
nil))
nil)
("2"
(hide 3)
(("2"
(replaces (-4 -5) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sign_eq_neg1")
(("2"
(cancel-by -4 "s")
(("2"
(case "ns <= s")
(("1"
(rewrite "sign_eq_neg1" 4)
(("1"
(assert)
(("1" (grind-reals) nil nil))
nil))
nil)
("2"
(hide 5)
(("2"
(replaces (-2 -3) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replaces -1)
(("2" (case "s>=0")
(("1" (rewrite "sign_eq_1")
(("1" (cancel-by -5 "s")
(("1"
(case "ns >= s")
(("1"
(rewrite "sign_eq_1" 2)
(("1"
(assert)
(("1" (neg-formula 2) nil nil))
nil))
nil)
("2"
(hide 3)
(("2"
(replaces (-4 -5) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sign_eq_neg1")
(("2" (cancel-by -4 "s")
(("2"
(case "ns <= s")
(("1"
(rewrite "sign_eq_neg1" 4)
(("1"
(assert)
(("1" (neg-formula 4) nil nil))
nil))
nil)
("2"
(hide 5)
(("2"
(replaces (-2 -3) :dir rl)
(("2" (grind-reals) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sign_abs formula-decl nil sign "reals/")
(Sign type-eq-decl nil sign "reals/")
(sign_eq_neg1 formula-decl nil sign "reals/")
(sign_eq_1 formula-decl nil sign "reals/"))
nil)))
[ zur Elbe Produktseite wechseln0.16Quellennavigators
Analyse erneut starten
]
|
2026-03-28
|
