Quelle sign3.prf Sprache: Lisp

(sign3
(sign3_mult_clos 0
  (sign3_mult_clos-1 nil 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 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))
   nil))
(sign3_div_clos 0
  (sign3_div_clos-1 nil 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (/= const-decl "boolean" notequal nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (Sign type-eq-decl nil sign nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
   nil))
(sign3_neg_clos 0
  (sign3_neg_clos-1 nil 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_int_is_int application-judgement "int" integers nil))
   nil))
(sign3_sq_clos 0
  (sign3_sq_clos-1 nil 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sq const-decl "nonneg_real" sq nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil))
   nil))
(sign3_sign 0
  (sign3_sign-1 nil 3427536907 ("" (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)
    (/= const-decl "boolean" notequal nil)
    (sign3 const-decl "Sign3" sign3 nil)
    (sign const-decl "Sign" sign nil))
   shostak))
(sign3_id 0
  (sign3_id-1 nil 3427476433 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_0 0
  (sign3_0-1 nil 3443439847 ("" (grind) nil nil)
   ((sign3 const-decl "Sign3" sign3 nil)) shostak))
(sign3_eq_1 0
  (sign3_eq_1-1 nil 3427537113 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_eq_neg1 0
  (sign3_eq_neg1-1 nil 3427537122 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_pos 0
  (sign3_pos-1 nil 3411901965 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil))
   nil))
(sign3_abs 0
  (sign3_abs-1 nil 3411901965 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil))
   nil))
(sign3_nneg 0
  (sign3_nneg-1 nil 3443439796
   ("" (skeep)
    (("" (rewrite "sign3_abs" :dir rl) (("" (assert) nil nil)) nil))
    nil)
   ((sign3_abs formula-decl nil sign3 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 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil))
   nil))
(sq_eps 0
  (sq_eps-1 nil 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sq_sign3 0
  (sq_sign3-1 nil 3411901965 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil)
    (sq const-decl "nonneg_real" sq nil))
   nil))
(sign3_times_abs 0
  (sign3_times_abs-1 nil 3411901965 ("" (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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sign3 const-decl "Sign3" sign3 nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   nil))
(abs_sign3 0
  (abs_sign3-1 nil 3411901965 ("" (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)
    (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)
    (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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_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))
(sign3_neg 0
  (sign3_neg-1 nil 3411901965 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil))
   nil))
(sign3_minus 0
  (sign3_minus-1 nil 3411901965 ("" (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_minus_real_is_real application-judgement "real" reals nil)
    (sign3 const-decl "Sign3" sign3 nil))
   nil))
(sign3_mult 0
  (sign3_mult-1 nil 3411901965
   ("" (skeep)
    (("" (grind)
      (("1" (mult-cases -1) nil nil) ("2" (mult-cases -1) nil nil)
       ("3" (mult-cases -1) nil nil) ("4" (mult-cases -1) nil nil)
       ("5" (mult-cases 2) nil nil) ("6" (mult-cases 2) nil nil))
      nil))
    nil)
   ((sign3 const-decl "Sign3" sign3 nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero_times3 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)
    (pos_times_gt formula-decl nil real_props nil))
   nil))
(sign3_div 0
  (sign3_div-1 nil 3411901965
   ("" (skeep)
    (("" (grind)
      (("1" (cross-mult -1) (("1" (assert) nil nil)) nil)
       ("2" (cross-mult -1) (("2" (assert) nil nil)) nil)
       ("3" (cross-mult 3) (("3" (assert) nil nil)) nil)
       ("4" (cross-mult 3) (("4" (assert) nil nil)) nil))
      nil))
    nil)
   ((sign3 const-decl "Sign3" sign3 nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (sign3_mult_clos application-judgement "Sign3" sign3 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)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_mult_neg_gt1 formula-decl nil extra_real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil))
   nil))
(sign3_mult_pos 0
  (sign3_mult_pos-1 nil 3411901965
   ("" (skeep)
    (("" (rewrite "sign3_mult")
      (("" (rewrite "sign3_eq_1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sign3_mult formula-decl nil sign3 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)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign3_eq_1 formula-decl nil sign3 nil))
   nil))
(sign3_div_pos1 0
  (sign3_div_pos1-1 nil 3427537156
   ("" (skeep)
    (("" (rewrite "sign3_div")
      (("" (rewrite "sign3_eq_1") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sign3_div formula-decl nil sign3 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)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign3_eq_1 formula-decl nil sign3 nil))
   shostak))
(sign3_div_pos2_TCC1 0
  (sign3_div_pos2_TCC1-1 nil 3427536906 ("" (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))
(sign3_div_pos2 0
  (sign3_div_pos2-1 nil 3427537178
   ("" (skeep)
    (("" (rewrite "sign3_div")
      (("" (case "sign3(y)=1")
        (("1" (assert) nil nil) ("2" (rewrite "sign3_eq_1") nil nil))
        nil))
      nil))
    nil)
   ((sign3_div formula-decl nil sign3 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)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign3_eq_1 formula-decl nil sign3 nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_mult_neg 0
  (sign3_mult_neg-1 nil 3427537213
   ("" (skeep)
    (("" (rewrite "sign3_mult")
      (("" (rewrite "sign3_eq_neg1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((sign3_mult formula-decl nil sign3 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)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (sign3_neg_clos application-judgement "Sign3" sign3 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)
    (sign3_eq_neg1 formula-decl nil sign3 nil))
   shostak))
(sign3_div_neg1 0
  (sign3_div_neg1-1 nil 3427537238
   ("" (skeep)
    (("" (rewrite "sign3_div")
      (("" (rewrite "sign3_eq_neg1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((sign3_div formula-decl nil sign3 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)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign3_neg_clos application-judgement "Sign3" sign3 nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sign3_eq_neg1 formula-decl nil sign3 nil))
   shostak))
(sign3_div_neg2_TCC1 0
  (sign3_div_neg2_TCC1-1 nil 3427536906 ("" (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))
(sign3_div_neg2 0
  (sign3_div_neg2-1 nil 3427537278
   ("" (skeep)
    (("" (rewrite "sign3_div")
      (("" (case "sign3(y)=-1")
        (("1" (assert) nil nil)
         ("2" (rewrite "sign3_eq_neg1") nil nil))
        nil))
      nil))
    nil)
   ((sign3_div formula-decl nil sign3 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)
    (sign3_mult_clos application-judgement "Sign3" sign3 nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign3_eq_neg1 formula-decl nil sign3 nil)
    (sign3_neg_clos application-judgement "Sign3" sign3 nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign3 type-eq-decl nil sign3 nil)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_div_mult_TCC1 0
  (sign3_div_mult_TCC1-1 nil 3427476510 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil)
    (/= const-decl "boolean" notequal nil))
   nil))
(sign3_div_mult 0
  (sign3_div_mult-1 nil 3427476511 ("" (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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (/= const-decl "boolean" notequal nil)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_and_abs 0
  (sign3_and_abs-1 nil 3411901965
   ("" (skosimp*)
    (("" (prop)
      (("1" (lemma "sign3_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)
    (sign3_times_abs formula-decl nil sign3 nil))
   nil))
(sign3_le 0
  (sign3_le-1 nil 3427476684 ("" (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)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak))
(sign3_ge 0
  (sign3_ge-1 nil 3427476690 ("" (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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sign3 const-decl "Sign3" sign3 nil))
   shostak)))

quality94%

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.