Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: examples4Q.pvs Sprache: Lisp

Original von: PVS^©

(examples4Q
(zero_to_one_quarter 0
  (zero_to_one_quarter-1 nil 3600857764
   (""
    (then (skeep)
     (numerical (! 1 1) :precision 4 :maxdepth 20 :verbose? t))
    nil nil)
   ((IntervalExpr type-decl nil IntervalExpr_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt 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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (X const-decl "RealExpr" interval_expr nil)
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt nil)
    (r2E const-decl "RealExpr" interval_expr nil)
    (numerical_soundness formula-decl nil numerical_bandb nil)
    (sound? const-decl "bool" numerical_bandb nil)
    (listn_0 name-judgement "listn[real](0)" simple_bandb nil)
    (Env type-eq-decl nil box nil)
    (vars_in_box? const-decl "bool" box nil)
    (list2array def-decl "T" array2list "structures/")
    (x skolem-const-decl "real" examples4Q nil)
    (nml_2 skolem-const-decl "(mult?)" examples4Q nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (|##| const-decl "bool" interval nil)
    (lb_interval formula-decl nil interval nil)
    (ub_interval formula-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (eval def-decl "real" interval_expr nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (vars_in_box formula-decl nil box nil)
    (length_singleton formula-decl nil more_list_props "structures/")
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (Interval type-eq-decl nil interval nil)
    (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
    (numfield nonempty-type-eq-decl nil 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)
    (ProperBox type-eq-decl nil box nil)
    (IntervalMinMax type-eq-decl nil numerical_bandb nil)
    (ProperBox? const-decl "bool" box nil)
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (numerical const-decl "Output" numerical_bandb nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (altdir_maxvar const-decl "DirVar" numerical_bandb nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (FALSE const-decl "bool" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
(Heart_TCC1 0
  (Heart_TCC1-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(Heart_TCC2 0
  (Heart_TCC2-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm_TCC1 0
  (hdp_mm_TCC1-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm_TCC2 0
  (hdp_mm_TCC2-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm_TCC3 0
  (hdp_mm_TCC3-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm_TCC4 0
  (hdp_mm_TCC4-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm_TCC5 0
  (hdp_mm_TCC5-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm_TCC6 0
  (hdp_mm_TCC6-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(hdp_mm 0
  (hdp_mm-1 nil 3600857764
   ("" (then (skeep) (numerical (! 1 1) :verbose? t)) nil nil)
   ((IntervalExpr type-decl nil IntervalExpr_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt nil)
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt nil)
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt nil)
    (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt
     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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (X const-decl "RealExpr" interval_expr nil)
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt nil)
    (r2E const-decl "RealExpr" interval_expr nil)
    (numfield nonempty-type-eq-decl nil 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)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (numerical_soundness formula-decl nil numerical_bandb nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (sound? const-decl "bool" numerical_bandb nil)
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box nil)
    (vars_in_box formula-decl nil box nil)
    (^ const-decl "real" exponentiation 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)
    (eval def-decl "real" interval_expr nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ub_interval formula-decl nil interval nil)
    (lb_interval formula-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nml_3 skolem-const-decl "(sub?)" examples4Q nil)
    (x4 skolem-const-decl "real" examples4Q nil)
    (x7 skolem-const-decl "real" examples4Q nil)
    (x3 skolem-const-decl "real" examples4Q nil)
    (x1 skolem-const-decl "real" examples4Q nil)
    (x5 skolem-const-decl "real" examples4Q nil)
    (x6 skolem-const-decl "real" examples4Q nil)
    (x2 skolem-const-decl "real" examples4Q nil)
    (x0 skolem-const-decl "real" examples4Q nil)
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box nil)
    (Env type-eq-decl nil box nil)
    (listn_0 name-judgement "listn[real](0)" simple_bandb nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Interval type-eq-decl nil interval nil)
    (list type-decl nil list_adt nil) (Box type-eq-decl nil box 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)
    (ProperBox type-eq-decl nil box nil)
    (IntervalMinMax type-eq-decl nil numerical_bandb nil)
    (ProperBox? const-decl "bool" box nil)
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (numerical const-decl "Output" numerical_bandb nil)
    (altdir_maxvar const-decl "DirVar" numerical_bandb nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (FALSE const-decl "bool" booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil))
   shostak))
(hdp_minmax 0
  (hdp_minmax-1 nil 3600857764 ("" (then (skeep) (interval)) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (FALSE const-decl "bool" booleans nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (null adt-constructor-decl "(null?)" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    ([\|\|] const-decl "Interval" interval nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (alt_max const-decl "DirVar" interval_bandb nil)
    (interval const-decl "Output" interval_bandb nil)
    (Output type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (length def-decl "nat" list_props nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (ProperBox type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (Box type-eq-decl nil box nil)
    (IntervalOutput type-eq-decl nil interval_bandb nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (BoolExpr type-eq-decl nil IntervalExpr_adt nil)
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (every adt-def-decl "boolean" list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (list type-decl nil list_adt nil)
    (Maybe type-decl nil Maybe "structures/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb nil)
    (Env type-eq-decl nil box nil)
    (vars_in_box? const-decl "bool" box nil)
    (list2array def-decl "T" array2list "structures/")
    (x0 skolem-const-decl "real" examples4Q nil)
    (x2 skolem-const-decl "real" examples4Q nil)
    (x6 skolem-const-decl "real" examples4Q nil)
    (x5 skolem-const-decl "real" examples4Q nil)
    (x1 skolem-const-decl "real" examples4Q nil)
    (x3 skolem-const-decl "real" examples4Q nil)
    (x7 skolem-const-decl "real" examples4Q nil)
    (x4 skolem-const-decl "real" examples4Q nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (beval def-decl "bool" interval_bexpr nil)
    (eval def-decl "real" interval_expr nil)
    (|##| const-decl "bool" interval nil)
    (iar_4 skolem-const-decl "(bincludes?)" examples4Q nil)
    (vars_in_box formula-decl nil box nil)
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box nil)
    (lb_interval formula-decl nil interval nil)
    (ub_interval formula-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (sound? const-decl "bool" interval_bandb nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (interval_soundness formula-decl nil interval_bandb nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (r2E const-decl "RealExpr" interval_expr nil)
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt nil)
    (X const-decl "RealExpr" interval_expr nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt
     nil)
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt nil)
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt nil)
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt nil)
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil)
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (Interval type-eq-decl nil interval nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IntervalExpr type-decl nil IntervalExpr_adt nil)
    (>= const-decl "bool" reals 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)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
(common_point_TCC1 0
  (common_point_TCC1-1 nil 3600857764 ("" (subtype-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(common_point 0
  (common_point-1 nil 3600857764 ("" (interval :verbose? t) nil nil)
   ((minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb nil)
    (Box type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb nil)
    (alt_max const-decl "DirVar" interval_bandb nil)
    (FALSE const-decl "bool" booleans nil)
    (BNOT adt-constructor-decl "[BoolExpr -> (bnot?)]" IntervalExpr_adt
     nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (sound? const-decl "bool" interval_bandb nil)
    (interval_soundness formula-decl nil interval_bandb nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt nil)
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt nil)
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt nil)
    (< const-decl "bool" reals nil)
    (BLETIN adt-constructor-decl
     "[[IntervalExpr, BoolExpr] -> (bletin?)]" IntervalExpr_adt nil)
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil)
    (r2E const-decl "RealExpr" interval_expr nil)
    (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt
     nil)
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     nil)
    (RealOrder type-eq-decl nil real_orders "reals/")
    (realorder? const-decl "bool" real_orders "reals/")
    (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]"
     IntervalExpr_adt nil)
    (BoolExpr type-eq-decl nil IntervalExpr_adt nil)
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (IntervalExpr type-decl nil IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt nil)
    (X const-decl "RealExpr" interval_expr nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (AND const-decl "[bool, 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (Interval type-eq-decl nil interval nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (numfield nonempty-type-eq-decl nil 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)
    (<= const-decl "bool" reals nil) (>= const-decl "bool" reals 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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 "real" exponentiation nil))
   shostak))
(simple_ite 0
  (simple_ite-1 nil 3600857764 ("" (interval) nil nil)
   ((TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (listn_0 name-judgement "listn[real](0)" simple_bandb nil)
    (Maybe type-decl nil Maybe "structures/")
    (list type-decl nil list_adt nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe
     "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/")
    (IntervalOutput type-eq-decl nil interval_bandb nil)
    (Box type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (stack type-eq-decl nil stack "structures/")
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (Output type-eq-decl nil branch_and_bound "structures/")
    (interval const-decl "Output" interval_bandb nil)
    (alt_max const-decl "DirVar" interval_bandb nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (Some adt-constructor-decl "[T -> (some?)]" Maybe "structures/")
    (FALSE const-decl "bool" booleans nil)
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box nil)
    (length_singleton formula-decl nil more_list_props "structures/")
    (vars_in_box formula-decl nil box nil)
    (iar_8 skolem-const-decl "(bimplies?)" examples4Q nil)
    (eval def-decl "real" interval_expr nil)
    (beval def-decl "bool" interval_bexpr nil)
    (x_9 skolem-const-decl "{x: real | x ## [|0, 10|]}" examples4Q nil)
    (|##| const-decl "bool" interval nil)
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box nil)
    (Env type-eq-decl nil box nil)
    (Eps const-decl "posreal" examples4Q 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)
    (sound? const-decl "bool" interval_bandb nil)
    (interval_soundness formula-decl nil interval_bandb nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt nil)
    (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt
     nil)
    (r2E const-decl "RealExpr" interval_expr nil)
    (<= const-decl "bool" reals nil)
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     nil)
    (RealOrder type-eq-decl nil real_orders "reals/")
    (realorder? const-decl "bool" real_orders "reals/")
    (BITE adt-constructor-decl
     "[[BoolExpr, BoolExpr, BoolExpr] -> (bite?)]" IntervalExpr_adt
     nil)
    (X const-decl "RealExpr" interval_expr nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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_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)
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (BIMPLIES adt-constructor-decl
     "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt nil)
    (BoolExpr type-eq-decl nil IntervalExpr_adt nil)
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (IntervalExpr type-decl nil IntervalExpr_adt nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.33 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.