Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: div.prf Sprache: Lisp

Original von: PVS^©

(rem (ml1 0
      (ml1-1 nil 3249307029
       ("" (skolem!)
        (("" (expand "div")
          (("" (expand "sgn")
            (("" (expand "abs")
              (("" (assert)
                (("" (lemma "both_sides_times_pos_lt1")
                  (("" (inst - "m!1" "n!1/m!1" "floor(n!1/m!1)+1")
                    (("" (flatten)
                      (("" (ground)
                        (("" (typepred "floor(n!1 / m!1)")
                          (("" (propax) nil))))))))))))))))))))
        nil)
       ((int_abs_is_nonneg application-judgement
         "{j: nonneg_int | j >= i}" real_defs nil)
        (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
         real_defs nil)
        (nonneg_floor_is_nat application-judgement "nat" floor_ceil
         nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (div const-decl "integer" div nil)
        (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
             real_defs nil)
        (both_sides_times_pos_lt1 formula-decl nil real_props nil)
        (NOT const-decl "[bool -> bool]" booleans nil)
        (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
         rationals nil)
        (posint_times_posint_is_posint application-judgement "posint"
         integers nil)
        (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
        (< const-decl "bool" reals nil)
        (<= const-decl "bool" reals nil)
        (AND const-decl "[bool, bool -> bool]" booleans nil)
        (integer nonempty-type-from-decl nil integers nil)
        (+ const-decl "[numfield, numfield -> numfield]" number_fields
           nil)
        (nat nonempty-type-eq-decl nil naturalnumbers nil)
        (/ const-decl "[numfield, nznum -> numfield]" number_fields
           nil)
        (nznum nonempty-type-eq-decl nil number_fields nil)
        (/= const-decl "boolean" notequal nil)
        (numfield nonempty-type-eq-decl nil number_fields nil)
        (posnat nonempty-type-eq-decl nil integers nil)
        (nonneg_int 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)
        (posreal nonempty-type-eq-decl nil real_types nil)
        (> const-decl "bool" reals nil)
        (nonneg_real nonempty-type-eq-decl nil real_types 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)
        (nnint_plus_posint_is_posint application-judgement "posint"
         integers nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
         rationals nil)
        (sgn const-decl "int" real_defs nil)
        (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
         integers nil))
       nil))
     (ml3 0
      (ml3-1 nil 3249307029
       ("" (skosimp*)
        (("" (case "i!1 >= 0")
          (("1" (expand "abs")
            (("1" (lift-if)
              (("1" (split 1)
                (("1" (flatten)
                  (("1" (lemma "div_smaller")
                    (("1" (inst?) (("1" (assert) nil)))))))
                 ("2" (flatten)
                  (("2" (lemma "ml1") (("2" (inst?) nil)))))))))))
           ("2" (expand "abs")
            (("2" (lift-if)
              (("2" (lemma "div_neg")
                (("2" (inst?)
                  (("2" (split 2)
                    (("1" (flatten)
                      (("1" (lemma "ml1")
                        (("1" (inst -1 "m!1" "-i!1")
                          (("1" (assert) nil) ("2" (assert) nil)))))))
                     ("2" (flatten)
                      (("2" (lemma "div_smaller")
                        (("2" (inst -1 "m!1" "-i!1")
                          (("1" (assert) nil)
                           ("2" (assert) nil))))))))))))))))))))
        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)
        (>= 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)
        (ml1 formula-decl nil rem nil)
        (real_ge_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (i!1 skolem-const-decl "int" rem nil)
        (nat nonempty-type-eq-decl nil naturalnumbers nil)
        (posnat nonempty-type-eq-decl nil integers nil)
        (> const-decl "bool" reals nil)
        (nonneg_int nonempty-type-eq-decl nil integers nil)
        (real_le_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (div_smaller formula-decl nil div nil)
        (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
             real_defs nil)
        (/= const-decl "boolean" notequal nil)
        (nonzero_integer nonempty-type-eq-decl nil integers nil)
        (minus_int_is_int application-judgement "int" integers nil)
        (numfield nonempty-type-eq-decl nil number_fields nil)
        (- const-decl "[numfield -> numfield]" number_fields nil)
        (rat_div_nzrat_is_rat application-judgement "rat" rationals
         nil)
        (div_nat formula-decl nil div nil)
        (div_neg formula-decl nil div nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil))
       nil))
     (rem_TCC1 0
      (rem_TCC1-1 nil 3249307029
       ("" (skosimp*)
        (("" (lemma "ml3")
          (("" (case "j!1 >= 0")
            (("1" (inst?)
              (("1" (expand "abs" 1 2) (("1" (assert) nil)))
               ("2" (assert) nil)))
             ("2" (inst -1 "i!1" "-j!1")
              (("1" (lemma "div_neg_d")
                (("1" (inst?)
                  (("1" (replace -1)
                    (("1" (expand "abs" 2 2)
                      (("1" (assert) nil)))))))))
               ("2" (assert) nil))))))))
        nil)
       ((ml3 formula-decl nil rem nil)
        (numfield nonempty-type-eq-decl nil number_fields nil)
        (- const-decl "[numfield -> numfield]" number_fields nil)
        (minus_int_is_int application-judgement "int" integers nil)
        (div_neg_d formula-decl nil div 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)
        (AND const-decl "[bool, bool -> bool]" booleans nil)
        (j!1 skolem-const-decl "nonzero_integer" rem nil)
        (> const-decl "bool" reals nil)
        (posnat nonempty-type-eq-decl nil integers nil)
        (nonneg_int nonempty-type-eq-decl nil integers nil)
        (minus_nzint_is_nzint application-judgement "nzint" integers
         nil)
        (int_abs_is_nonneg application-judgement
         "{j: nonneg_int | j >= i}" real_defs 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)
        (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
         real_defs nil)
        (abs_nat_rew formula-decl nil abs_rews 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)
        (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)
        (nonzero_integer nonempty-type-eq-decl nil integers nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil))
       nil))
     (rem_neg 0
      (rem_neg-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem")
          (("" (rewrite "div_neg") (("" (assert) nil))))))
        nil)
       ((mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (minus_int_is_int application-judgement "int" integers nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (real_ge_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (real_gt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (nonzero_integer 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)
        (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)
        (div_neg formula-decl nil div nil))
       nil))
     (rem_neg_d 0
      (rem_neg_d-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem")
          (("" (rewrite "div_neg_d") (("" (assert) nil))))))
        nil)
       ((mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (minus_int_is_int application-judgement "int" integers nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (real_ge_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (real_gt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (nonzero_integer 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)
        (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)
        (div_neg_d formula-decl nil div nil)
        (minus_nzint_is_nzint application-judgement "nzint" integers
         nil))
       nil))
     (rem_even 0
      (rem_even-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem") (("" (rewrite "div_even") nil)))) nil)
       ((mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (nonzero_integer 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)
        (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)
        (div_even formula-decl nil div nil))
       nil))
     (rem_eq_arg 0
      (rem_eq_arg-1 nil 3249307029
       ("" (skolem!)
        (("" (expand "rem")
          (("" (rewrite "div_eq_arg") (("" (assert) nil))))))
        nil)
       ((mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (nzint_times_nzint_is_nzint application-judgement "nzint"
         integers nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (nonzero_integer 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)
        (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)
        (div_eq_arg formula-decl nil div nil))
       nil))
     (rem_zero 0
      (rem_zero-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem")
          (("" (rewrite "div_zero") (("" (assert) nil))))))
        nil)
       ((rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (int_times_even_is_even application-judgement "even_int"
         integers nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (nonzero_integer 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)
        (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)
        (div_zero formula-decl nil div nil))
       nil))
     (rem_lt 0
      (rem_lt-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem")
          (("" (rewrite "div_lt") (("" (assert) nil))))))
        nil)
       ((mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (int_times_even_is_even application-judgement "even_int"
         integers nil)
        (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
         real_defs nil)
        (real_ge_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (int_abs_is_nonneg application-judgement
         "{j: nonneg_int | j >= i}" real_defs nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (nonzero_integer 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)
        (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)
        (div_lt formula-decl nil div nil))
       nil))
     (rem_it_is 0
      (rem_it_is-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem")
          (("" (case "div(a!1,m!1) = c!1")
            (("1" (assert) nil)
             ("2" (hide 2)
              (("2" (expand "div")
                (("2" (expand "sgn")
                  (("2" (expand "abs")
                    (("2" (replace -1)
                      (("2" (hide -1)
                        (("2" (lemma "floor_plus_int")
                          (("2"
                            (case "(b!1 + m!1 * c!1) / m!1 = b!1 / m!1 + c!1")
                            (("1" (replace -1)
                              (("1"
                                (hide -1)
                                (("1"
                                  (inst -1 "c!1" "b!1/m!1")
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (lemma "floor_small")
                                        (("1"
                                          (inst?)
                                          (("1"
                                            (expand "abs")
                                            (("1"
                                              (assert)
                                              nil)))))))))))))))))
                             ("2" (hide -1 -2 2)
                              (("2"
                                (assert)
                                nil))))))))))))))))))))))))
        nil)
       ((nil application-judgement "nat" div nil)
        (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
         integers nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (sgn const-decl "int" real_defs nil)
        (floor_plus_int formula-decl nil floor_ceil nil)
        (floor_small formula-decl nil floor_ceil nil)
        (* const-decl "[numfield, numfield -> numfield]" number_fields
           nil)
        (+ const-decl "[numfield, numfield -> numfield]" number_fields
           nil)
        (/ const-decl "[numfield, nznum -> numfield]" number_fields
           nil)
        (nznum nonempty-type-eq-decl nil number_fields nil)
        (numfield nonempty-type-eq-decl nil number_fields nil)
        (nnrat_plus_nnrat_is_nnrat application-judgement "nonneg_rat"
         rationals nil)
        (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
             real_defs nil)
        (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
         real_defs nil)
        (int_abs_is_nonneg application-judgement
         "{j: nonneg_int | j >= i}" real_defs nil)
        (div_nat formula-decl nil div nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
         integers nil)
        (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
         rationals nil)
        (nonneg_floor_is_nat application-judgement "nat" floor_ceil
         nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (number nonempty-type-decl nil numbers nil)
        (boolean nonempty-type-decl nil booleans 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)
        (/= const-decl "boolean" notequal nil)
        (nonzero_integer nonempty-type-eq-decl nil integers nil)
        (integer nonempty-type-from-decl nil integers nil)
        (div const-decl "integer" div nil)
        (bool nonempty-type-eq-decl nil booleans nil)
        (>= const-decl "bool" reals nil)
        (nat nonempty-type-eq-decl nil naturalnumbers nil)
        (nonneg_int nonempty-type-eq-decl nil integers nil)
        (> const-decl "bool" reals nil)
        (posnat nonempty-type-eq-decl nil integers nil))
       nil))
     (rem_eq_0 0
      (rem_eq_0-1 nil 3249307029 ("" (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)
        (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)
        (nonzero_integer nonempty-type-eq-decl nil integers nil)
        (real_ge_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
         rationals nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem nil)
        (div const-decl "integer" div nil)
        (int_abs_is_nonneg application-judgement
         "{j: nonneg_int | j >= i}" real_defs nil)
        (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
         real_defs nil)
        (nonneg_floor_is_nat application-judgement "nat" floor_ceil
         nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rat_div_nzrat_is_rat application-judgement "rat" rationals
         nil))
       nil))
     (rem_one 0
      (rem_one-1 nil 3249307029
       ("" (skosimp*)
        (("" (lift-if)
          (("" (split 1)
            (("1" (flatten)
              (("1" (expand "abs")
                (("1" (lift-if)
                  (("1" (split -1)
                    (("1" (flatten)
                      (("1" (lemma "rem_eq_arg")
                        (("1" (inst -1 "1")
                          (("1" (lemma "rem_neg_d")
                            (("1" (inst -1 "1" "1")
                              (("1" (assert) nil)))))))))))
                     ("2" (flatten)
                      (("2" (lemma "rem_eq_arg")
                        (("2" (inst?) (("2" (assert) nil)))))))))))))))
             ("2" (flatten)
              (("2" (lemma "rem_lt")
                (("2" (inst?)
                  (("2" (expand "abs")
                    (("2" (lift-if) (("2" (ground) nil))))))))))))))))
        nil)
       ((rem_lt formula-decl nil rem 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)
        (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)
        (nonzero_integer nonempty-type-eq-decl nil integers 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_nzint_is_nzint application-judgement "nzint" integers
         nil)
        (rem_neg_d formula-decl nil rem nil)
        (rem_eq_arg formula-decl nil rem nil)
        (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
             real_defs nil))
       nil))
     (rem_TCC2 0
      (rem_TCC2-1 nil 3249307029
       ("" (skosimp*)
        (("" (expand "rem")
          (("" (lemma "div_smaller")
            (("" (inst?)
              (("" (assert)
                (("" (lemma "ml1")
                  (("" (inst - "m!1" "n!1") (("" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ((nil application-judgement "nat" div nil)
        (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
         integers nil)
        (mult_divides1 application-judgement "(divides(n))" divides
         nil)
        (mult_divides2 application-judgement "(divides(m))" divides
         nil)
        (rem const-decl "{k | abs(k) < abs(j)}" rem 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)
        (rational_pred const-decl "[real -> boolean]" rationals nil)
        (rational nonempty-type-from-decl nil rationals nil)
        (integer_pred const-decl "[rational -> boolean]" integers nil)
        (int nonempty-type-eq-decl nil integers nil)
        (bool nonempty-type-eq-decl nil booleans nil)
        (>= const-decl "bool" reals nil)
        (nonneg_int nonempty-type-eq-decl nil integers nil)
        (> const-decl "bool" reals nil)
        (posnat nonempty-type-eq-decl nil integers nil)
        (nat nonempty-type-eq-decl nil naturalnumbers nil)
        (ml1 formula-decl nil rem nil)
        (div_nat formula-decl nil div nil)
        (real_le_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (real_lt_is_strict_total_order name-judgement
         "(strict_total_order?[real])" real_props nil)
        (nonneg_floor_is_nat application-judgement "nat" floor_ceil
         nil)
        (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
         rationals nil)
        (real_ge_is_total_order name-judgement "(total_order?[real])"
         real_props nil)
        (int_minus_int_is_int application-judgement "int" integers nil)
        (div_smaller formula-decl nil div nil))
       nil)))

¤ Dauer der Verarbeitung: 0.91 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.