products/Sources/formale Sprachen/COBOL/Test-Suite/COBOL/SQ/   (NIST Cobol Test-Suite ©)  Datei vom 4.1.2008 mit Größe 47 kB image not shown  

Bilddatei

real_order.prf


products/Sources/formale Sprachen/PVS/Tarski/real_order.prf

(real_order (real_ord_ep_well_founded 0 (real_ord_ep_well_founded-1 nil 3595171480 ("" (skeep) (("" (expand "well_founded?") (("" (skeep) (("" (skolem - "a") (("" (name "Kset" "{kk:nat | EXISTS (x:(p)): kk = floor(abs(x)/epsil)}") (("" (name "mm" "min(Kset)") (("1" (typepred "mm") (("1" (copy -1) (("1" (expand "Kset" -1) (("1" (skolem - "yy") (("1" (inst + "yy") (("1" (skeep) (("1" (inst - "floor(abs(x)/epsil)") (("1" (split -) (("1" (expand "real_ord_ep") (("1" (assert) nil nil)) nil) ("2" (expand "Kset" 1) (("2" (inst + "x") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "floor(abs(a)/epsil)") (("2" (expand "Kset" 1) (("2" (inst + "a") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((well_founded? const-decl "bool" orders nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ord_ep const-decl "bool" real_order nil) (Kset skolem-const-decl "[nat -> boolean]" real_order nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (a skolem-const-decl "real" real_order nil) (p skolem-const-decl "pred[real]" real_order nil) (empty? const-decl "bool" sets nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil 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 "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil)) (real_ord_ep_decreases_halves 0 (real_ord_ep_decreases_halves-1 nil 3595172081 ("" (skeep) (("" (case "FORALL (y:real): y>=1 IMPLIES floor(y/2) < floor(y)") (("1" (inst - "abs(x)/epsil") (("1" (assert) (("1" (split -1) (("1" (expand "real_ord_ep") (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-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 "bool" reals nil) (>= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ord_ep_well_founded application-judgement "(well_founded?[real])" real_order nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ord_ep const-decl "bool" real_order nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)))