| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/interval_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 281 kB |
|
Impressum interval.prf Sprache: Lisp |
|||||||||
|
(interval
(Member_Proper 0 (Member_Proper-1 nil 3545739152 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (Proper? const-decl "bool" interval nil)) nil)) (Proper_Member 0 (Proper_Member-1 nil 3545739170 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (Proper? const-decl "bool" interval nil) (|##| const-decl "bool" interval nil)) nil)) (r2i_Proper 0 (r2i_Proper-1 nil 3549199013 ("" (judgement-tcc) nil nil) (([\|\|] const-decl "Interval" interval nil) (Proper? const-decl "bool" interval nil)) nil)) (Proper_eq_NonEmpty 0 (Proper_eq_NonEmpty-1 nil 3546812344 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Proper? const-decl "bool" interval nil) (EmptyInterval? const-decl "bool" interval nil)) shostak)) (Proper_NonEmpty 0 (Proper_NonEmpty-1 nil 3577002288 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil) (EmptyInterval const-decl "Interval" interval nil) (Proper? const-decl "bool" interval nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (eq_Incl 0 (eq_Incl-1 nil 3545738788 ("" (grind) (("" (decompose-equality) nil nil)) nil) ((Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<< const-decl "bool" interval nil)) shostak)) (Incl_Member 0 (Incl_Member-1 nil 3545739626 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (<< const-decl "bool" interval nil) (|##| const-decl "bool" interval nil)) shostak)) (Member_Incl 0 (Member_Incl-1 nil 3545739631 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (Interval type-eq-decl nil interval nil) (Proper? const-decl "bool" interval nil) (|##| const-decl "bool" interval nil) (<< const-decl "bool" interval nil)) shostak)) (Incl_Proper 0 (Incl_Proper-1 nil 3546770863 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<< const-decl "bool" interval nil) (Proper? const-decl "bool" interval nil)) shostak)) (midpoint_inclusion 0 (midpoint_inclusion-1 nil 3546711487 ("" (grind) nil nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Proper? const-decl "bool" interval nil) (slice const-decl "real" interval nil) (midpoint const-decl "real" interval nil) (|##| const-decl "bool" interval nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (Lt_Ge 0 (Lt_Ge-1 nil 3318335123 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Lt const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (EmptyInterval? const-decl "bool" interval nil)) shostak)) (Le_Gt 0 (Le_Gt-1 nil 3318335128 ("" (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Le const-decl "bool" interval nil) (Gt const-decl "bool" interval nil) (EmptyInterval? const-decl "bool" interval nil)) shostak)) (Trichotomy 0 (Trichotomy-1 nil 3545736267 ("" (grind) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Proper? const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (Le const-decl "bool" interval nil) (Zeroin? const-decl "bool" interval nil)) shostak)) (Abs_TCC1 0 (Abs_TCC1-1 nil 3579649336 ("" (subtype-tcc) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (Zeroin? const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Ge const-decl "bool" interval nil) (NonNeg? const-decl "bool" interval nil)) nil)) (Abs_TCC2 0 (Abs_TCC2-1 nil 3579649336 ("" (grind) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Zeroin? const-decl "bool" interval nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Ge const-decl "bool" interval nil) (NonNeg? const-decl "bool" interval nil)) nil)) (Sq_TCC1 0 (Sq_TCC1-1 nil 3318333335 ("" (subtype-tcc) nil nil) ((Ge const-decl "bool" interval nil) (sq const-decl "nonneg_real" sq "reals/") ([\|\|] const-decl "Interval" interval nil) (NonNeg? const-decl "bool" interval nil)) nil)) (Sq_TCC2 0 (Sq_TCC2-1 nil 3579649506 ("" (subtype-tcc) nil nil) ((Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (sq const-decl "nonneg_real" sq "reals/") ([\|\|] const-decl "Interval" interval nil) (NonNeg? const-decl "bool" interval nil)) nil)) (Sq_TCC3 0 (Sq_TCC3-1 nil 3579649506 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (sq const-decl "nonneg_real" sq "reals/") ([\|\|] const-decl "Interval" interval nil) (NonNeg? const-decl "bool" interval nil)) nil)) (Pow_TCC1 0 (Pow_TCC1-1 nil 3350326108 ("" (subtype-tcc) nil nil) ((Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (Pow_TCC2 0 (Pow_TCC2-1 nil 3350326108 ("" (subtype-tcc) nil nil) ((Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (Pow_TCC3 0 (Pow_TCC3-1 nil 3350326108 ("" (subtype-tcc) nil nil) ((Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (Pow_TCC4 0 (Pow_TCC4-1 nil 3350326108 ("" (subtype-tcc) nil nil) ((Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (Pow_TCC5 0 (Pow_TCC5-1 nil 3350326108 ("" (subtype-tcc) nil nil) ((Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (Pow_TCC6 0 (Pow_TCC6-1 nil 3350326108 ("" (subtype-tcc) nil nil) ((Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (/= const-decl "boolean" notequal nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) nil)) (Intersection_inclusion 0 (Intersection_inclusion-1 nil 3577002526 ("" (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Intersection const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil)) nil)) (Intersection_left_Empty 0 (Intersection_left_Empty-1 nil 3579697131 ("" (grind) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (EmptyInterval? const-decl "bool" interval nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Intersection const-decl "Interval" interval nil)) shostak)) (Intersection_right_Empty 0 (Intersection_right_Empty-1 nil 3579697162 ("" (grind) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (EmptyInterval? const-decl "bool" interval nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Intersection const-decl "Interval" interval nil)) shostak)) (Add_comm 0 (Add_comm-1 nil 3318335139 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil) (Add const-decl "Interval" interval nil)) shostak)) (Mult_comm 0 (Mult_comm-1 nil 3318334112 ("" (grind) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Ge const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (pXp const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (Neg const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (pXn const-decl "Interval" interval nil) (pXm const-decl "Interval" interval nil) (nXn const-decl "Interval" interval nil) (nXm const-decl "Interval" interval nil) (mXp const-decl "Interval" interval nil) (mXn const-decl "Interval" interval nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (mXm const-decl "Interval" interval nil) (Mult const-decl "Interval" interval nil)) shostak)) (Neg_Incl 0 (Neg_Incl-1 nil 3545739708 ("" (grind) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<< const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil)) nil)) (Zeroless0 0 (Zeroless0-1 nil 3318335234 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (Zeroless? const-decl "bool" interval nil) (/= const-decl "boolean" notequal nil)) shostak)) (Neg_Ge_0 0 (Neg_Ge_0-1 nil 3318335239 ("" (grind) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Le const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil) (Ge const-decl "bool" interval nil)) shostak)) (Strict_Lt 0 (Strict_Lt-1 nil 3320961671 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (StrictInterval? const-decl "bool" interval nil)) shostak)) (Halves 0 (Halves-1 nil 3321035367 ("" (skeep) (("" (grind) nil nil)) nil) ((slice const-decl "real" interval nil) (midpoint const-decl "real" interval nil) ([\|\|] const-decl "Interval" interval nil) (HalfRight const-decl "Interval" interval nil) (size const-decl "real" interval nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (HalfLeft const-decl "Interval" interval nil)) shostak)) (Halves_Incl 0 (Halves_Incl-1 nil 3321095140 ("" (grind) nil nil) ((real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Proper? const-decl "bool" interval nil) (slice const-decl "real" interval nil) (midpoint const-decl "real" interval nil) ([\|\|] const-decl "Interval" interval nil) (HalfLeft const-decl "Interval" interval nil) (<< const-decl "bool" interval nil) (HalfRight const-decl "Interval" interval nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (Halves_inclusion 0 (Halves_inclusion-1 nil 3546810076 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (|##| const-decl "bool" interval nil) (slice const-decl "real" interval nil) (midpoint const-decl "real" interval nil) ([\|\|] const-decl "Interval" interval nil) (HalfLeft const-decl "Interval" interval nil) (HalfRight const-decl "Interval" interval nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (Incl_trans 0 (Incl_trans-1 nil 3321095152 ("" (grind) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (<< const-decl "bool" interval nil)) shostak)) (Pow2_Sq 0 (Pow2_Sq-1 nil 3321310186 ("" (grind) nil nil) ((Ge const-decl "bool" interval nil) (odd? const-decl "bool" integers nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) ([\|\|] const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (Pow const-decl "Interval" interval nil) (sq const-decl "nonneg_real" sq "reals/") (Sq const-decl "(NonNeg?)" interval nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil)) shostak)) (Mult_Neg_Neg 0 (Mult_Neg_Neg-1 nil 3545736683 ("" (grind) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (Ge const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (pXp const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (Neg const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (pXn const-decl "Interval" interval nil) (pXm const-decl "Interval" interval nil) (nXn const-decl "Interval" interval nil) (nXm const-decl "Interval" interval nil) (mXp const-decl "Interval" interval nil) (mXn const-decl "Interval" interval nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (mXm const-decl "Interval" interval nil) (Mult const-decl "Interval" interval nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (Mult_Neg_left 0 (Mult_Neg_left-1 nil 3545736690 ("" (grind) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Ge const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (pXp const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (Neg const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (pXn const-decl "Interval" interval nil) (pXm const-decl "Interval" interval nil) (nXn const-decl "Interval" interval nil) (nXm const-decl "Interval" interval nil) (mXp const-decl "Interval" interval nil) (mXn const-decl "Interval" interval nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (mXm const-decl "Interval" interval nil) (Mult const-decl "Interval" interval nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (Mult_Neg_right 0 (Mult_Neg_right-1 nil 3545736695 ("" (grind) nil nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Ge const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (pXp const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (Neg const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (pXn const-decl "Interval" interval nil) (pXm const-decl "Interval" interval nil) (nXn const-decl "Interval" interval nil) (nXm const-decl "Interval" interval nil) (mXp const-decl "Interval" interval nil) (mXn const-decl "Interval" interval nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (mXm const-decl "Interval" interval nil) (Mult const-decl "Interval" interval nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (Sq_Neg_eq 0 (Sq_Neg_eq-1 nil 3545818757 ("" (grind) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Ge const-decl "bool" interval nil) (sq const-decl "nonneg_real" sq "reals/") ([\|\|] const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (Sq const-decl "(NonNeg?)" interval nil) (Neg const-decl "Interval" interval nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (Union_id 0 (Union_id-1 nil 3546381093 ("" (skeep) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((Union const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil)) shostak)) (Union_symm 0 (Union_symm-1 nil 3546381143 ("" (grind) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Union const-decl "Interval" interval nil)) shostak)) (Union_Incl_left 0 (Union_Incl_left-1 nil 3546812242 ("" (grind) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Union const-decl "Interval" interval nil) (<< const-decl "bool" interval nil)) shostak)) (Union_Incl_right 0 (Union_Incl_right-1 nil 3546812266 ("" (grind) nil nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) ([\|\|] const-decl "Interval" interval nil) (Union const-decl "Interval" interval nil) (<< const-decl "bool" interval nil)) shostak)) (Add_0_r 0 (Add_0_r-1 nil 3320066346 ("" (skeep) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((r2i_Proper application-judgement "ProperInterval" interval nil) (Add const-decl "Interval" interval 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) ([\|\|] const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_plus_real_is_real application-judgement "real" reals nil) ([\|\|] const-decl "Interval" interval nil)) shostak)) (Add_0_l 0 (Add_0_l-1 nil 3320066375 ("" (skeep) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((r2i_Proper application-judgement "ProperInterval" interval nil) (Add const-decl "Interval" interval 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) ([\|\|] const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_plus_real_is_real application-judgement "real" reals nil) ([\|\|] const-decl "Interval" interval nil)) nil)) (Mult_1_r 0 (Mult_1_r-1 nil 3320066384 ("" (skeep) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((r2i_Proper application-judgement "ProperInterval" interval nil) (Mult const-decl "Interval" interval 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) ([\|\|] const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (Ge const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (pXp const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (pXm const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (nXm const-decl "Interval" interval nil) (mXp const-decl "Interval" interval nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (Mult_1_l 0 (Mult_1_l-1 nil 3320066393 ("" (skeep) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((r2i_Proper application-judgement "ProperInterval" interval nil) (Mult const-decl "Interval" interval 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) ([\|\|] const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (pXm const-decl "Interval" interval nil) (pXn const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (pXp const-decl "Interval" interval nil) ([\|\|] const-decl "Interval" interval nil) (Ge const-decl "bool" interval nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (Div_1 0 (Div_1-1 nil 3318335177 ("" (skosimp) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((r2i_Proper application-judgement "ProperInterval" interval nil) (Div const-decl "Interval" interval 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) ([\|\|] const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) ([\|\|] const-decl "Interval" interval nil) (Ge const-decl "bool" interval nil) (pXp const-decl "Interval" interval nil) (Le const-decl "bool" interval nil) (pXm const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil) (nXp const-decl "Interval" interval nil) (nXm const-decl "Interval" interval nil) (mXp const-decl "Interval" interval nil) (Mult const-decl "Interval" interval nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (Pow_0 0 (Pow_0-1 nil 3318335195 ("" (skosimp) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((r2i_Proper application-judgement "ProperInterval" interval 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Pow const-decl "Interval" interval nil) ([\|\|] const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (Pow_1 0 (Pow_1-1 nil 3318335202 ("" (skosimp) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Pow const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) ([\|\|] const-decl "Interval" interval nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (Ge const-decl "bool" interval nil)) shostak)) (lb_interval 0 (lb_interval-1 nil 3318621128 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil)) shostak)) (lb_r2i 0 (lb_r2i-1 nil 3319735236 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil)) shostak)) (ub_interval 0 (ub_interval-1 nil 3318621141 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil)) shostak)) (ub_r2i 0 (ub_r2i-1 nil 3319735241 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil)) shostak)) (Incl_reflx 0 (Incl_reflx-1 nil 3549125759 ("" (grind) nil nil) ((<< const-decl "bool" interval nil)) shostak)) (Incl_r2i 0 (Incl_r2i-1 nil 3549125766 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil) (<< const-decl "bool" interval nil) (|##| const-decl "bool" interval nil)) shostak)) (Neg_Neg 0 (Neg_Neg-1 nil 3318335220 ("" (skosimp) (("" (decompose-equality) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((Neg const-decl "Interval" interval nil) (Interval type-eq-decl nil interval nil) (real nonempty-type-from-decl nil reals nil) (minus_real_is_real application-judgement "real" reals nil) ([\|\|] const-decl "Interval" interval nil)) shostak)) (ub_inclusion 0 (ub_inclusion-1 nil 3545739421 ("" (grind) nil nil) ((Proper? const-decl "bool" interval nil) (|##| const-decl "bool" interval nil)) shostak)) (lb_inclusion 0 (lb_inclusion-1 nil 3545739427 ("" (grind) nil nil) ((Proper? const-decl "bool" interval nil) (|##| const-decl "bool" interval nil)) shostak)) (Neg_interval 0 (Neg_interval-1 nil 3318621148 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil)) shostak)) (Pos_Gt_0 0 (Pos_Gt_0-1 nil 3318335249 ("" (grind) nil nil) ((Gt const-decl "bool" interval nil) (Pos? const-decl "bool" interval nil)) shostak)) (NonNeg_Ge_0 0 (NonNeg_Ge_0-1 nil 3318335254 ("" (grind) nil nil) ((Ge const-decl "bool" interval nil) (NonNeg? const-decl "bool" interval nil)) shostak)) (Pos_Neg_Lt_0 0 (Pos_Neg_Lt_0-1 nil 3318335259 ("" (grind) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Gt const-decl "bool" interval nil) (Pos? const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil) (Lt const-decl "bool" interval nil)) shostak)) (NonNeg_Neg_Le_0 0 (NonNeg_Neg_Le_0-1 nil 3318335264 ("" (grind) nil nil) ((minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Ge const-decl "bool" interval nil) (NonNeg? const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil) (Le const-decl "bool" interval nil)) shostak)) (r2i_sharp_eq 0 (r2i_sharp_eq-1 nil 3567640507 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) ([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil)) shostak)) (r2i_Le 0 (r2i_Le-1 nil 3319587327 ("" (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 "Interval" interval nil) (Le const-decl "bool" interval nil)) shostak)) (r2i_Lt 0 (r2i_Lt-1 nil 3319587332 ("" (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 "Interval" interval nil) (Lt const-decl "bool" interval nil)) shostak)) (r2i_Ge 0 (r2i_Ge-1 nil 3319587338 ("" (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 "Interval" interval nil) (Ge const-decl "bool" interval nil)) shostak)) (r2i_Gt 0 (r2i_Gt-1 nil 3319587343 ("" (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 "Interval" interval nil) (Gt const-decl "bool" interval nil)) shostak)) (Lt_Le 0 (Lt_Le-1 nil 3318335287 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Lt const-decl "bool" interval nil) (Le const-decl "bool" interval nil)) shostak)) (Gt_Ge 0 (Gt_Ge-1 nil 3318335291 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Gt const-decl "bool" interval nil) (Ge const-decl "bool" interval nil)) shostak)) (inclusion_Gt 0 (inclusion_Gt-1 nil 3318335303 ("" (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (Gt const-decl "bool" interval nil)) shostak)) (inclusion_Ge 0 (inclusion_Ge-1 nil 3318335308 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (Ge const-decl "bool" interval nil)) shostak)) (inclusion_Lt 0 (inclusion_Lt-1 nil 3318335312 ("" (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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (Lt const-decl "bool" interval nil)) shostak)) (inclusion_Le 0 (inclusion_Le-1 nil 3318335316 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (Le const-decl "bool" interval nil)) shostak)) (r2i_trans 0 (r2i_trans-1 nil 3303814164 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (<< const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil)) shostak)) (add2sub 0 (add2sub-1 nil 3350326109 ("" (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) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Sub const-decl "Interval" interval nil)) shostak)) (sub2add 0 (sub2add-1 nil 3350326116 ("" (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) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Add const-decl "Interval" interval nil)) shostak)) (Member_trans 0 (Member_trans-1 nil 3318335334 ("" (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) (<< const-decl "bool" interval nil)) shostak)) (r2i_inclusion 0 (r2i_inclusion-1 nil 3302519809 ("" (grind) nil nil) (([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil)) shostak)) (Add_inclusion 0 (Add_inclusion-1 nil 3318335347 ("" (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) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Add const-decl "Interval" interval nil)) shostak)) (Sub_inclusion 0 (Sub_inclusion-1 nil 3318335352 ("" (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) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Sub const-decl "Interval" interval nil)) shostak)) (Neg_inclusion 0 (Neg_inclusion-1 nil 3318335356 ("" (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) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (Neg const-decl "Interval" interval nil)) shostak)) (pXp 0 (pXp-1 nil 3278260700 ("" (grind :theories "real_props") nil nil) ((pXp const-decl "Interval" interval nil) ([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (le_times_le_pos formula-decl nil real_props 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (nXp 0 (nXp-1 nil 3278260739 ("" (skeep) (("" (expand "nXp") (("" (lemma "Neg_inclusion") (("" (inst -1 "X" "x") (("" (assert) (("" (lemma "pXp") (("" (inst -1 "Neg(X)" "Y" "-x" "y") (("" (assert) (("" (split -1) (("1" (lemma "Neg_inclusion") (("1" (inst -1 "pXp(Neg(X),Y)" "-x*y") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nXp const-decl "Interval" interval nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval 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) (pXp formula-decl nil interval nil) (Le const-decl "bool" interval nil) (Ge const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pXp const-decl "Interval" interval nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Neg const-decl "Interval" interval nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (Neg_inclusion formula-decl nil interval nil)) nil)) (pXn 0 (pXn-1 nil 3278260788 ("" (skeep) (("" (expand "pXn") (("" (lemma "nXp") (("" (inst -1 "Y" "X" "y" "x") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((pXn const-decl "Interval" interval nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval 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_times_real_is_real application-judgement "real" reals nil) (nXp formula-decl nil interval nil)) nil)) (nXn 0 (nXn-2 nil 3278261218 ("" (grind :theories "real_props") nil nil) ((nXn const-decl "Interval" interval nil) (pXp const-decl "Interval" interval nil) (neg_times_neg formula-decl nil real_props nil) (Neg const-decl "Interval" interval nil) ([\|\|] const-decl "Interval" interval nil) (|##| const-decl "bool" interval nil) (Le const-decl "bool" interval nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (le_times_le_neg formula-decl nil real_props 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (pXm 0 (pXm-1 nil 3301392992 ("" (skeep) (("" (case "y >= 0") (("1" (grind :theories "real_props") (("1" (case "x * y >= 0") (("1" (case "ub(X) * lb(Y) <= 0") (("1" (assert) nil nil) ("2" (grind-reals) nil nil)) nil) ("2" (grind-reals) nil nil)) nil)) nil) ("2" (grind :theories "real_props") (("1" (case "x*y <= 0") (("1" (case "ub(X) * ub(Y) >= 0") (("1" (assert) nil nil) ("2" (grind-reals) nil nil)) nil) ("2" (grind-reals) nil nil)) nil) ("2" (mult-ineq -6 -7 (+ -)) nil nil)) nil)) nil)) nil) ((>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (neg_times_le formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (Interval type-eq-decl nil interval nil) (<= const-decl "bool" reals nil) (le_times_le_pos formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Ge const-decl "bool" interval nil) (Zeroin? const-decl "bool" interval nil) (|##| const-decl "bool" interval nil) ([\|\|] const-decl "Interval" interval nil) (pXm const-decl "Interval" interval nil) (le_times_le_any1 formula-decl nil extra_real_props nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (mXp 0 (mXp-1 nil 3301397382 ("" (skeep) (("" (expand "mXp") (("" (lemma "pXm") (("" (inst -1 "Y" "X" "y" "x") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((mXp const-decl "Interval" interval nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval 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_times_real_is_real application-judgement "real" reals nil) (pXm formula-decl nil interval nil)) shostak)) (nXm 0 (nXm-2 nil 3579693670 ("" (skeep) (("" (expand "nXm") (("" (lemma "pXm") (("" (inst -1 "Neg(X)" "Y" "-x" "y") (("" (assert) (("" (split) (("1" (lemma "Neg_inclusion") (("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "Neg_Ge_0") nil nil) ("3" (rewrite "Neg_inclusion") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nXm const-decl "Interval" interval nil) (minus_real_is_real application-judgement "real" reals nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval nil) (Neg const-decl "Interval" interval 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (pXm const-decl "Interval" interval nil) (Neg_inclusion formula-decl nil interval nil) (Neg_Ge_0 formula-decl nil interval nil) (real_times_real_is_real application-judgement "real" reals nil) (pXm formula-decl nil interval nil)) nil)) (mXn 0 (mXn-1 nil 3301399245 ("" (skeep) (("" (expand "mXn") (("" (lemma "nXm") (("" (inst -1 "Y" "X" "y" "x") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((mXn const-decl "Interval" interval nil) (real nonempty-type-from-decl nil reals nil) (Interval type-eq-decl nil interval 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_times_real_is_real application-judgement "real" reals nil) (nXm formula-decl nil interval nil)) shostak)) (mXm 0 (mXm-1 nil 3301399821 ("" (skeep) (("" (expand "mXm") (("" (expand "Zeroin?") (("" (case "ub(X) * ub(Y) >=0" "lb(X) * lb(Y) >= 0" "ub(X) * lb(Y) <= 0" "lb(X) * ub(Y) <= 0") (("1" (label "H" (-1 -2 -3 -4)) (("1" (hide "H") (("1" (grind :theories "real_props") (("1" (case "x*y >= 0") (("1" (grind-reals) (("1" (mult-ineq -7 -9 (- -)) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal "H") (("2" (name-replace "A" "x*y") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "x*y >= 0") (("1" (grind-reals) (("1" (mult-ineq -8 -10 (+ +)) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal "H") (("2" (name-replace "A" "x*y") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (case "x*y >= 0") (("1" (reveal "H") (("1" (name-replace "A" "x*y") --> -------------------- --> maximum size reached --> -------------------- ¤ 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.0.47Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28