Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: linear_algebra.summary Sprache: Lisp

Original von: PVS^©

(interval_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 "interval_arith/")
    (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 "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (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 "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (numerical_soundness formula-decl nil numerical_bandb
     "interval_arith/")
    (sound? const-decl "bool" numerical_bandb "interval_arith/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (x skolem-const-decl "real" interval_examples4Q nil)
    (nml_81 skolem-const-decl "(mult?)" interval_examples4Q nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (|##| const-decl "bool" interval "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (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 "interval_arith/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (vars_in_box formula-decl nil box "interval_arith/")
    (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 "interval_arith/")
    (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 "interval_arith/")
    (list type-decl nil list_adt nil)
    (Box type-eq-decl nil box "interval_arith/")
    (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 "interval_arith/")
    (IntervalMinMax type-eq-decl nil numerical_bandb "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (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 "interval_arith/")
    (/= 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
                   "interval_arith/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (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 "interval_arith/")
    (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 "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (NEG adt-constructor-decl "[RealExpr -> (neg?)]" IntervalExpr_adt
     "interval_arith/")
    (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 "interval_arith/")
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (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
     "interval_arith/")
    (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 "interval_arith/")
    (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 "interval_arith/")
    (vars_in_box formula-decl nil box "interval_arith/")
    (^ 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 "interval_arith/")
    (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 "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (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_82 skolem-const-decl "(sub?)" interval_examples4Q nil)
    (x4 skolem-const-decl "real" interval_examples4Q nil)
    (x7 skolem-const-decl "real" interval_examples4Q nil)
    (x3 skolem-const-decl "real" interval_examples4Q nil)
    (x1 skolem-const-decl "real" interval_examples4Q nil)
    (x5 skolem-const-decl "real" interval_examples4Q nil)
    (x6 skolem-const-decl "real" interval_examples4Q nil)
    (x2 skolem-const-decl "real" interval_examples4Q nil)
    (x0 skolem-const-decl "real" interval_examples4Q nil)
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (listn_0 name-judgement "listn[real](0)" simple_bandb
     "interval_arith/")
    (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 "interval_arith/")
    (list type-decl nil list_adt nil)
    (Box type-eq-decl nil box "interval_arith/")
    (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 "interval_arith/")
    (IntervalMinMax type-eq-decl nil numerical_bandb "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (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 "interval_arith/")
    (altdir_maxvar const-decl "DirVar" numerical_bandb
                   "interval_arith/")
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (- 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 "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (interval const-decl "Output" interval_bandb "interval_arith/")
    (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 "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (IntervalOutput type-eq-decl nil interval_bandb "interval_arith/")
    (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 "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (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
     "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (x0 skolem-const-decl "real" interval_examples4Q nil)
    (x2 skolem-const-decl "real" interval_examples4Q nil)
    (x6 skolem-const-decl "real" interval_examples4Q nil)
    (x5 skolem-const-decl "real" interval_examples4Q nil)
    (x1 skolem-const-decl "real" interval_examples4Q nil)
    (x3 skolem-const-decl "real" interval_examples4Q nil)
    (x7 skolem-const-decl "real" interval_examples4Q nil)
    (x4 skolem-const-decl "real" interval_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 "interval_arith/")
    (eval def-decl "real" interval_expr "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (iar_83 skolem-const-decl "(bincludes?)" interval_examples4Q nil)
    (vars_in_box formula-decl nil box "interval_arith/")
    (vars_in_box_rec def-decl
     "{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
     box "interval_arith/")
    (lb_interval formula-decl nil interval "interval_arith/")
    (ub_interval formula-decl nil interval "interval_arith/")
    (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 "interval_arith/")
    (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
     "interval_arith/")
    (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 "interval_arith/")
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (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
     "interval_arith/")
    (MULT adt-constructor-decl "[[RealExpr, RealExpr] -> (mult?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt
     "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (>= 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 "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    (^ 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 "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (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 "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (FALSE const-decl "bool" booleans nil)
    (BNOT adt-constructor-decl "[BoolExpr -> (bnot?)]" IntervalExpr_adt
     "interval_arith/")
    (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 "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (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 "interval_arith/")
    (SUB adt-constructor-decl "[[RealExpr, RealExpr] -> (sub?)]"
     IntervalExpr_adt "interval_arith/")
    (ADD adt-constructor-decl "[[RealExpr, RealExpr] -> (add?)]"
     IntervalExpr_adt "interval_arith/")
    (< const-decl "bool" reals nil)
    (BLETIN adt-constructor-decl
     "[[IntervalExpr, BoolExpr] -> (bletin?)]" IntervalExpr_adt
     "interval_arith/")
    (BINCLUDES adt-constructor-decl
     "[[RealExpr, Interval] -> (bincludes?)]" IntervalExpr_adt
     "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (ABS adt-constructor-decl "[RealExpr -> (abs?)]" IntervalExpr_adt
     "interval_arith/")
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (RealOrder type-eq-decl nil real_orders "reals/")
    (realorder? const-decl "bool" real_orders "reals/")
    (BAND adt-constructor-decl "[[BoolExpr, BoolExpr] -> (band?)]"
     IntervalExpr_adt "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (IntervalExpr type-decl nil IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (POW adt-constructor-decl "[[RealExpr, nat] -> (pow?)]"
     IntervalExpr_adt "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (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 "interval_arith/")
    (|##| const-decl "bool" interval "interval_arith/")
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (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
     "interval_arith/")
    (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 "interval_arith/")
    (Box type-eq-decl nil box "interval_arith/")
    (ProperBox? const-decl "bool" box "interval_arith/")
    (ProperBox type-eq-decl nil box "interval_arith/")
    (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 "interval_arith/")
    (alt_max const-decl "DirVar" interval_bandb "interval_arith/")
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    ([\|\|] const-decl "Interval" interval "interval_arith/")
    (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 "interval_arith/")
    (length_singleton formula-decl nil more_list_props "structures/")
    (vars_in_box formula-decl nil box "interval_arith/")
    (iar_87 skolem-const-decl "(bimplies?)" interval_examples4Q nil)
    (eval def-decl "real" interval_expr "interval_arith/")
    (beval def-decl "bool" interval_bexpr "interval_arith/")
    (x_88 skolem-const-decl "{x: real | x ## [|0, 10|]}"
     interval_examples4Q nil)
    (|##| const-decl "bool" interval "interval_arith/")
    (list2array def-decl "T" array2list "structures/")
    (vars_in_box? const-decl "bool" box "interval_arith/")
    (Env type-eq-decl nil box "interval_arith/")
    (Eps const-decl "posreal" interval_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 "interval_arith/")
    (interval_soundness formula-decl nil interval_bandb
     "interval_arith/")
    (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 "interval_arith/")
    (/ 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 "interval_arith/")
    (SQ adt-constructor-decl "[RealExpr -> (sq?)]" IntervalExpr_adt
     "interval_arith/")
    (r2E const-decl "RealExpr" interval_expr "interval_arith/")
    (<= const-decl "bool" reals nil)
    (BREL adt-constructor-decl
     "[[RealOrder, RealExpr, RealExpr] -> (brel?)]" IntervalExpr_adt
     "interval_arith/")
    (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
     "interval_arith/")
    (X const-decl "RealExpr" interval_expr "interval_arith/")
    (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
     "interval_arith/")
    (Interval type-eq-decl nil interval "interval_arith/")
    (real nonempty-type-from-decl nil reals nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (BIMPLIES adt-constructor-decl
     "[[BoolExpr, BoolExpr] -> (bimplies?)]" IntervalExpr_adt
     "interval_arith/")
    (BoolExpr type-eq-decl nil IntervalExpr_adt "interval_arith/")
    (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bite? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (brel? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bor? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (band? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt "interval_arith/")
    (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 "interval_arith/"))
   shostak)))

¤ Dauer der Verarbeitung: 0.35 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.