|
(sign (sign_mult_clos 0
(sign_mult_clos-1 nil 3427062350 ("" (tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(nzint_times_nzint_is_nzint application-judgement "nzint"
integers nil))
nil))
(sign_div_clos 0
(sign_div_clos-1 nil 3427062350 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat"
rationals nil))
nil))
(sign_neg_clos 0
(sign_neg_clos-1 nil 3427062350 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(minus_nzint_is_nzint application-judgement "nzint" integers
nil))
nil))
(sign_sq_clos 0
(sign_sq_clos-1 nil 3427062350 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(sq const-decl "nonneg_real" sq nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil))
nil))
(sign_id 0
(sign_id-1 nil 3427476319 ("" (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)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil))
shostak))
(sign_pos 0
(sign_pos-1 nil 3427062350 ("" (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_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil))
nil))
(sign_eq_1 0
(sign_eq_1-1 nil 3427062373 ("" (grind) nil nil)
((sign const-decl "Sign" sign nil)) shostak))
(sign_eq_neg1 0
(sign_eq_neg1-1 nil 3427062379 ("" (grind) nil nil)
((sign const-decl "Sign" sign nil)) shostak))
(sign_nat 0
(sign_nat-1 nil 3443439591 ("" (grind) nil nil)
((sign const-decl "Sign" sign nil)) shostak))
(sign_abs 0
(sign_abs-1 nil 3427062350 ("" (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_odd_is_odd application-judgement "odd_int" integers
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)
(sign const-decl "Sign" sign nil))
nil))
(sign_nneg 0
(sign_nneg-1 nil 3443439645
("" (skeep)
(("" (rewrite "sign_abs" :dir rl) (("" (assert) nil nil))
nil))
nil)
((sign_abs formula-decl nil sign 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(square_eps 0
(square_eps-1 nil 3427062350
("" (skosimp*)
(("" (typepred "eps!1")
(("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil)
((Sign type-eq-decl nil sign nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(/= const-decl "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(sign_mult_clos application-judgement "Sign" sign nil))
nil))
(sq_eps 0
(sq_eps-1 nil 3427062350
("" (skosimp*)
(("" (expand "sq")
(("" (typepred "eps!1")
(("" (prop)
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((sq const-decl "nonneg_real" sq nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
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)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil))
nil))
(sq_eq_sign 0
(sq_eq_sign-1 nil 3436177032
("" (skeep)
(("" (ground)
(("1" (lemma "sq_eq_abs")
(("1" (inst?)
(("1" (assert)
(("1" (hide -2)
(("1" (expand "abs")
(("1" (lift-if)
(("1" (lift-if)
(("1" (lift-if)
(("1" (ground)
(("1" (inst + "1")
(("1" (assert) nil nil)) nil)
("2" (inst + "-1")
(("2" (assert) nil nil)) nil)
("3" (inst + "-1")
(("3" (assert) nil nil)) nil)
("4" (inst + "1")
(("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1 * lr)
(("2" (hide -1)
(("2" (rewrite "sq_times")
(("2" (assert)
(("2" (rewrite "sq_eps") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
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)
(real nonempty-type-from-decl nil reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(real_times_real_is_real application-judgement "real" reals
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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(sq_eq_abs formula-decl nil sq nil)
(sq_times formula-decl nil sq nil)
(sq_nz_pos application-judgement "posreal" sq nil)
(sign_sq_clos application-judgement "Sign" sign nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_eps formula-decl nil sign nil))
shostak))
(sq_sign 0
(sq_sign-1 nil 3427062350 ("" (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_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil)
(sq const-decl "nonneg_real" sq nil))
nil))
(sign_sign 0
(sign_sign-1 nil 3427110655 ("" (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_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil))
shostak))
(sign_times_abs 0
(sign_times_abs-1 nil 3427062350
("" (skosimp*)
(("" (expand "sign")
(("" (expand "abs")
(("" (case "x!1 >= 0")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((sign const-decl "Sign" sign 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil))
nil))
(abs_sign 0
(abs_sign-1 nil 3427062350 ("" (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)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nzint nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals
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))
nil))
(abs_pos 0
(abs_pos-1 nil 3427062350 ("" (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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(/= const-decl "boolean" notequal nil))
nil))
(sign_neg 0
(sign_neg-1 nil 3427062350 ("" (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)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(/= const-decl "boolean" notequal nil)
(sign const-decl "Sign" sign nil))
nil))
(sign_minus 0
(sign_minus-1 nil 3427062350 ("" (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_minus_real_is_real application-judgement "real" reals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(/= const-decl "boolean" notequal nil)
(sign const-decl "Sign" sign nil))
nil))
(sign_mult 0
(sign_mult-1 nil 3427062350
("" (skolem 1 ("x" "y"))
(("" (grind)
(("1" (rewrite "pos_times_ge") nil nil)
("2" (rewrite "pos_times_ge") nil nil)
("3" (rewrite "pos_times_ge") nil nil)
("4" (rewrite "pos_times_ge") nil nil))
nil))
nil)
((sign const-decl "Sign" sign nil)
(/= const-decl "boolean" notequal nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(pos_times_ge formula-decl nil 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))
nil))
(sign_div 0
(sign_div-1 nil 3427062350
("" (skosimp*)
(("" (expand "sign")
(("" (rewrite "pos_div_ge")
(("" (lift-if) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((sign const-decl "Sign" sign nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(pos_div_ge formula-decl nil real_props nil))
nil))
(sign_mult_pos 0
(sign_mult_pos-1 nil 3427062350
("" (grind)
(("1" (rewrite "pos_times_ge") nil nil)
("2" (rewrite "pos_times_ge") nil nil))
nil)
((pos_times_ge formula-decl nil 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(sign const-decl "Sign" sign nil))
nil))
(sign_div_pos1 0
(sign_div_pos1-1 nil 3427535661
("" (skeep)
(("" (rewrite "sign_div")
(("" (rewrite "sign_eq_1") (("" (assert) nil nil)) nil))
nil))
nil)
((sign_div formula-decl nil sign 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)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint"
integers nil)
(sign_eq_1 formula-decl nil sign nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sign_div_pos2_TCC1 0
(sign_div_pos2_TCC1-1 nil 3427535780 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(sign_div_pos2 0
(sign_div_pos2-1 nil 3427535796
("" (skeep)
(("" (case "x=0")
(("1" (grind) nil nil)
("2" (rewrite "sign_div")
(("2" (case "sign(y)=1")
(("1" (assert) nil nil)
("2" (rewrite "sign_eq_1") nil nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil)
(Sign type-eq-decl nil sign nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzint nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sign_eq_1 formula-decl nil sign nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(sign_div formula-decl nil sign nil))
shostak))
(sign_mult_neg 0
(sign_mult_neg-1 nil 3427536087
("" (skeep)
(("" (case "y=0")
(("1" (grind) nil nil)
("2" (rewrite "sign_mult")
(("2" (rewrite "sign_eq_neg1")
(("2" (rewrite "sign_neg") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(sign const-decl "Sign" sign nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign_eq_neg1 formula-decl nil sign nil)
(bool nonempty-type-eq-decl nil booleans nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nzint_times_nzint_is_nzint application-judgement "nzint"
integers nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(sign_neg formula-decl nil sign nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(sign_mult formula-decl nil sign nil))
shostak))
(sign_div_neg1 0
(sign_div_neg1-1 nil 3427536569
("" (skeep)
(("" (rewrite "sign_div")
(("" (rewrite "sign_eq_neg1") (("" (assert) nil nil)) nil))
nil))
nil)
((sign_div formula-decl nil sign 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)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint"
integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(sign_eq_neg1 formula-decl nil sign nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
shostak))
(sign_div_neg2_TCC1 0
(sign_div_neg2_TCC1-1 nil 3427536604 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(sign_div_neg2 0
(sign_div_neg2-1 nil 3427536605
("" (skeep)
(("" (case "x=0")
(("1" (grind) nil nil)
("2" (rewrite "sign_div")
(("2" (rewrite "sign_neg")
(("2" (case "sign(y)=-1")
(("1" (assert) nil nil)
("2" (rewrite "sign_eq_neg1") nil nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(sign const-decl "Sign" sign nil)
(sign_neg formula-decl nil sign nil)
(sign_neg_clos application-judgement "Sign" sign nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(sign_eq_neg1 formula-decl nil sign nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzint nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(Sign type-eq-decl nil sign nil)
(sign_mult_clos application-judgement "Sign" sign nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(sign_div formula-decl nil sign nil))
shostak))
(sign_div_mult 0
(sign_div_mult-1 nil 3427476377 ("" (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)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sign const-decl "Sign" sign nil))
shostak))
(sign_and_abs 0
(sign_and_abs-1 nil 3427062350
("" (skosimp*)
(("" (prop)
(("1" (lemma "sign_times_abs")
(("1" (inst-cp - "x!1")
(("1" (inst - "y!1") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) 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)
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(sign_times_abs formula-decl nil sign nil))
nil))
(sign_le 0
(sign_le-1 nil 3427476576 ("" (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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil))
shostak))
(sign_ge 0
(sign_ge-1 nil 3427476580 ("" (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)
(sign const-decl "Sign" sign nil))
shostak))
(sign_dichotomy 0
(sign_dichotomy-1 nil 3427540190 ("" (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_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign const-decl "Sign" sign nil))
shostak))
(sign_ext_TCC1 0
(sign_ext_TCC1-1 nil 3594054736 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil))
nil))
(sign_ext_TCC2 0
(sign_ext_TCC2-1 nil 3594054736 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(real_times_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))
nil))
(sign_ext_TCC3 0
(sign_ext_TCC3-1 nil 3594054736 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(real_times_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))
nil))
(sign_ext_mult 0
(sign_ext_mult-1 nil 3594054744
("" (skeep)
(("" (lemma "nnreal_times_nnreal_is_nnreal")
(("" (case "x = 0 OR y = 0")
(("1" (grind) nil nil)
("2" (flatten)
(("2" (lemma "nzreal_times_nzreal_is_nzreal")
(("2" (inst - "x" "y")
(("1" (flatten)
(("1" (inst - "abs(x)" "abs(y)")
(("1" (grind) nil nil)) nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types
nil)
(/= const-decl "boolean" notequal nil)
(x skolem-const-decl "real" sign nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(minus_real_is_real application-judgement "real" reals nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzreal_times_nzreal_is_nzreal judgement-tcc nil real_types
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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(y skolem-const-decl "real" sign nil)
(< const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign 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)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_times_real_is_real application-judgement "real" reals
nil))
nil)))
¤ Dauer der Verarbeitung: 0.56 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.
|
