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