| products/sources/formale sprachen/PVS/interval_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: conf Sprache: LispOriginal von: PVS© |
|
||||||
|
(numerical_bandb
(evaluate_TCC1 0 (evaluate_TCC1-1 nil 3546971207 ("" (skosimp*) (("" (lift-if -6) (("" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (Ubbox_Proper application-judgement "ProperBox" box nil) (Lbbox_Proper application-judgement "ProperBox" box nil)) nil)) (evaluate_TCC2 0 (evaluate_TCC2-1 nil 3546971207 ("" (skosimp*) (("" (lift-if -8) (("" (assert) nil nil)) nil)) nil) ((Lbbox_Proper application-judgement "ProperBox" box nil) (Ubbox_Proper application-judgement "ProperBox" box nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (mindir_maxvar_aux_TCC1 0 (mindir_maxvar_aux_TCC1-1 nil 3547134405 ("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil)) nil) ((ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Midbox_Proper application-judgement "ProperBox" box nil) (r2i_Proper application-judgement "ProperInterval" interval nil) (real_plus_real_is_real application-judgement "real" reals nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (Midbox const-decl "listn[Interval](length(box))" box nil) ([\|\|] const-decl "Interval" interval nil) (midpoint const-decl "real" interval nil) (slice const-decl "real" interval nil)) nil)) (mindir_maxvar_aux_TCC2 0 (mindir_maxvar_aux_TCC2-1 nil 3547134405 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (int_minus_int_is_int application-judgement "int" integers 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_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/") (number nonempty-type-decl nil numbers nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (slice const-decl "real" interval nil) (midpoint const-decl "real" interval nil) ([\|\|] const-decl "Interval" interval nil) (Midbox const-decl "listn[Interval](length(box))" box nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (max_rec_TCC1 0 (max_rec_TCC1-1 nil 3546365509 ("" (subtype-tcc) nil nil) nil nil)) (max_rec_TCC2 0 (max_rec_TCC2-1 nil 3546365509 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC3 0 (max_rec_TCC3-1 nil 3546365509 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC4 0 (max_rec_TCC4-1 nil 3546365509 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC5 0 (max_rec_TCC5-1 nil 3546365509 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (max_rec_TCC6 0 (max_rec_TCC6-1 nil 3546365509 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC7 0 (max_rec_TCC7-1 nil 3546365509 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC8 0 (max_rec_TCC8-1 nil 3546365509 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC9 0 (max_rec_TCC9-1 nil 3546365509 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) nil)) (max_rec_TCC10 0 (max_rec_TCC10-1 nil 3546365509 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (size const-decl "real" interval nil)) nil)) (max_rec_TCC11 0 (max_rec_TCC11-1 nil 3546365509 ("" (termination-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (> const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (max_aux_TCC1 0 (max_aux_TCC1-1 nil 3547134405 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_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/")) nil)) (max_aux_TCC2 0 (max_aux_TCC2-1 nil 3547134405 ("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil)) nil) ((ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (every adt-def-decl "boolean" list_adt nil) (length def-decl "nat" list_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (max_aux_TCC3 0 (max_aux_TCC3-1 nil 3547134405 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box 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/")) nil)) (max_aux_TCC4 0 (max_aux_TCC4-1 nil 3547134405 ("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil)) nil) ((ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (max_aux_TCC5 0 (max_aux_TCC5-1 nil 3547134405 ("" (skeep) (("" (case-replace "box=null") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (length def-decl "nat" list_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (altvar_TCC1 0 (altvar_TCC1-1 nil 3547136696 ("" (skeep :preds? t) (("" (grind) nil nil)) nil) ((ProperBox? const-decl "bool" box nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/")) nil)) (altvar_TCC2 0 (altvar_TCC2-1 nil 3547136696 ("" (skeep :preds? t) (("" (lemma "mod_pos") (("" (inst?) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (DirVarStack type-eq-decl nil branch_and_bound "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (stack type-eq-decl nil stack "structures/") (DirVar type-eq-decl nil branch_and_bound "structures/") (IntervalMinMax type-eq-decl nil numerical_bandb 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (IntervalExpr type-decl nil IntervalExpr_adt 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) (Interval type-eq-decl nil interval nil) (list type-decl nil list_adt 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) (length def-decl "nat" list_props nil) (Box type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (ProperBox type-eq-decl nil box nil) (box skolem-const-decl "ProperBox" numerical_bandb nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (interval_minmax_soundness 0 (interval_minmax_soundness-3 nil 3579703168 ("" (skeep) (("" (lemma "b_and_b_id_sound") (("" (expand "interval_minmax") (("" (inst?) (("" (assert) (("" (hide 2) (("" (split) (("1" (expand "accomodates?") (("1" (skeep) (("1" (expand "sound?") (("1" (flatten) (("1" (name-replace "ev" "evaluate(dom, obj)" :hide? nil) (("1" (copy -1) (("1" (expand "evaluate" -1 :assert? none) (("1" (skoletin* -1 :old? t) (("1" (decompose-equality -3) (("1" (case "Inclusion?(ev`lb_box, dom) AND Inclusion?(ev`ub_box, dom)") (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (skeep) (("1" (lemma "Eval_inclusion_Proper") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skeep :preds? t) (("2" (replaces -18) (("2" (hide (-3 -7 -8 -9 -10)) (("2" (case-replace "ub(P1) < ub(P2)") (("1" (lemma "Eval_inclusion_Proper") (("1" (inst -1 "Lb" "vs" "obj") (("1" (beta) (("1" (assert) (("1" (expand "##") (("1" (lemma "Proper_Inclusion") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (lemma "Eval_inclusion_Proper") (("2" (inst -1 "Ub" "vs" "obj") (("2" (beta) (("2" (expand "##") (("2" (lemma "Proper_Inclusion") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep :preds? t) (("3" (replaces -18) (("3" (hide (-2 -4 -5 -11 -12)) (("3" (case-replace "lb(P1) > lb(P2)") (("1" (lemma "Eval_inclusion_Proper") (("1" (inst -1 "Lb" "vs" "obj") (("1" (beta) (("1" (expand "##") (("1" (assert) (("1" (lemma "Proper_Inclusion") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (lemma "Eval_inclusion_Proper") (("2" (inst -1 "Ub" "vs" "obj") (("2" (expand "##") (("2" (lemma "Proper_Inclusion") (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split 1) (("1" (hide (-4 -5 -6 -7)) (("1" (case "ub(P1) < ub(P2)") (("1" (assert) (("1" (lemma "Lbbox_Inclusion") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "Ubbox_Inclusion") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 -8 -9)) (("2" (case "lb(P1) > lb(P2)") (("1" (assert) (("1" (lemma "Lbbox_Inclusion") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "Ubbox_Inclusion") (("2" (inst? -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subdiv_presound?") (("2" (skeep) (("2" (expand "denorm") (("2" (expand "branch") (("2" (expand "subdivide") (("2" (expand "sound?") (("2" (flatten) (("2" (expand "combine" -3) (("2" (use "Proper_Safe2") (("2" (assert) (("2" (flatten) (("2" (expand "combine" 1 1) (("2" (replaces -3) (("2" (assert) (("2" (flatten) (("2" (expand "combine") (("2" (expand "sound_dir") (("2" (lemma "split_Inclusion") (("2" (inst? -1) (("2" (skoletin* -1 :old? t) (("2" (lemma "split_Proper") (("2" (inst? -1) (("2" (flatten) (("2" (replace -3 :dir rl) (("2" (replace -4 :dir rl) (("2" (split 1) (("1" (skeep :preds? t) (("1" (inst - "vs") (("1" (rewrite "Union_inclusion") nil nil)) nil)) nil) ("2" (lift-if) (("2" (assert) (("2" (split 1) (("1" (flatten) (("1" (split -) (("1" (flatten) (("1" (lemma "Inclusion_trans") (("1" (inst -1 "ans1`lb_box" "bl" "dom") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "Inclusion_trans") (("2" (inst -1 "ans1`lb_box" "br" "dom") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (assert) (("3" (split 1) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.846 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
