| products/sources/formale Sprachen/Coq/ide/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sqrt.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.119 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
