products/Sources/formale Sprachen/PVS/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: cSig.mli   Sprache: Unknown

(tmod
 (ml3 0
  (ml3-1 nil 3406631585
   ("" (skosimp*)
    (("" (expand "abs")
      (("" (lift-if)
        (("" (case-replace "floor(i!1 / m!1) = i!1/m!1")
          (("1" (auto-rewrite-theory "real_props")
            (("1" (ground) nil nil)) nil)
           ("2" (ground)
            (("1" (lemma "both_sides_times_pos_lt1")
              (("1" (inst -1 "m!1" "floor(i!1 / m!1)" "i!1 / m!1")
                (("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (typepred "floor(i!1 / m!1)")
              (("2" (lemma "both_sides_times_pos_lt1")
                (("2"
                  (inst -1 "m!1" "i!1 / m!1" " 1 + floor(i!1 / m!1)")
                  (("2" (flatten)
                    (("2" (hide -1) (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals 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)
    (integer nonempty-type-from-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (int nonempty-type-eq-decl nil integers 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (zero_not_lt_zero formula-decl nil real_props nil)
    (div_cancel1 formula-decl nil real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (minus_int_is_int application-judgement "int" 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))
 (ml4 0
  (ml4-1 nil 3406631585
   ("" (skosimp*)
    (("" (expand "abs")
      (("" (lift-if)
        (("" (ground)
          (("1" (typepred "floor(-i!1 / m!1)")
            (("1" (lemma "both_sides_times_pos_lt1")
              (("1"
                (inst -1 "m!1" "-i!1 / m!1" "1 + floor(-i!1 / m!1)")
                (("1" (flatten)
                  (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil)
           ("2" (lemma "both_sides_times_pos_lt1")
            (("2" (inst -1 "m!1" "floor(-i!1 / m!1)" "-i!1 / m!1")
              (("2" (assert)
                (("2" (case-replace "floor(-i!1 / m!1) = -i!1/m!1")
                  (("1" (assert)
                    (("1" (auto-rewrite-theory "real_props")
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (<= const-decl "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)
    (integer nonempty-type-from-decl nil integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (int nonempty-type-eq-decl nil integers 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)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (minus_int_is_int application-judgement "int" integers nil))
   nil))
 (mod_TCC1 0
  (mod_TCC1-1 nil 3406631585
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (case "j!1 >= 0")
        (("1" (lemma "ml3")
          (("1" (inst?)
            (("1" (expand "abs")
              (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
             ("2" (assert) nil nil))
            nil))
          nil)
         ("2" (lemma "ml4")
          (("2" (inst -1 "i!1" "-j!1")
            (("1" (expand "abs")
              (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv nil)
    (ml4 formula-decl nil tmod nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (ml3 formula-decl nil tmod 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)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (j!1 skolem-const-decl "nonzero_integer" tmod nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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))
 (mod_even 0
  (mod_even-1 nil 3406631585
   ("" (skosimp*)
    (("" (expand "mod")
      (("" (expand "tdiv")
        (("" (rewrite "floor_int")
          (("1" (assert) nil nil)
           ("2" (expand "integer?") (("2" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (floor_int formula-decl nil floor_ceil 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)
    (integer nonempty-type-from-decl nil integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (integer? const-decl "bool" integers nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (mod_neg 0
  (mod_neg-1 nil 3406631585
   ("" (auto-rewrite-theory "integers")
    (("" (skosimp*)
      (("" (lift-if)
        (("" (expand "mod")
          (("" (expand "tdiv")
            (("" (case "-i!1/j!1 = -(i!1/j!1)")
              (("1" (replace -1)
                (("1" (hide -1)
                  (("1" (ground)
                    (("1" (rewrite "floor_int")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (nonzero_integer 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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (numfield nonempty-type-eq-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)
    (minus_rat_is_rat application-judgement "rat" rationals nil)
    (closed_neg formula-decl nil integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (floor_int formula-decl nil floor_ceil nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (integer? const-decl "bool" integers nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (mod_neg_d 0
  (mod_neg_d-1 nil 3406631585
   ("" (auto-rewrite-theory "integers")
    (("" (skosimp*)
      (("" (lift-if)
        (("" (expand "mod")
          (("" (expand "tdiv")
            (("" (case "i!1/-j!1=-(i!1/j!1)")
              (("1" (replace -1)
                (("1" (hide -1)
                  (("1" (rewrite "floor_neg")
                    (("1" (lift-if)
                      (("1" (ground)
                        (("1" (rewrite "floor_int")
                          (("1" (assert) nil nil)) nil)
                         ("2" (case "integer_pred(--(i!1/j!1))")
                          (("1" (assert) nil nil)
                           ("2" (assert) nil nil))
                          nil)
                         ("3" (lift-if)
                          (("3" (ground)
                            (("3" (hide 1)
                              (("3"
                                (lemma "integers.closed_neg")
                                (("3"
                                  (inst - "-(i!1/j!1)")
                                  (("3" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (numfield nonempty-type-eq-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)
    (minus_rat_is_rat application-judgement "rat" rationals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (floor_int formula-decl nil floor_ceil nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (closed_neg formula-decl nil integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (integer? const-decl "bool" integers nil)
    (floor_neg formula-decl nil floor_ceil nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (mod_eq_arg 0
  (mod_eq_arg-1 nil 3406631585 ("" (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)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (tdiv const-decl "integer" tdiv nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
 (mod_lt 0
  (mod_lt-1 nil 3406631585
   ("" (skosimp*)
    (("" (lift-if)
      (("" (expand "mod")
        (("" (expand "abs")
          (("" (expand "sgn")
            (("" (grind)
              (("1" (rewrite "floor_small")
                (("1" (lift-if)
                  (("1" (ground) (("1" (rewrite "pos_div_ge") nil nil))
                    nil))
                  nil))
                nil)
               ("2" (rewrite "floor_small")
                (("2" (lift-if)
                  (("2" (ground) (("2" (rewrite "pos_div_ge") nil nil))
                    nil))
                  nil))
                nil)
               ("3" (rewrite "floor_small")
                (("3" (lift-if)
                  (("3" (ground) (("3" (rewrite "pos_div_ge") nil nil))
                    nil))
                  nil))
                nil)
               ("4" (rewrite "floor_small")
                (("4" (lift-if)
                  (("4" (ground) (("4" (rewrite "pos_div_ge") nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv const-decl "integer" tdiv nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_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)
    (pos_div_ge formula-decl nil real_props nil)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil)
    (int_times_even_is_even application-judgement "even_int" integers
     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)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer nonempty-type-from-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)
    (floor_small formula-decl nil floor_ceil nil)
    (sgn const-decl "int" tdiv nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil))
   nil))
 (mod_lt_nat 0
  (mod_lt_nat-1 nil 3406631585
   ("" (skosimp*)
    (("" (rewrite "mod_lt")
      (("1" (expand "sgn") (("1" (propax) nil nil)) nil)
       ("2" (expand "abs") (("2" (propax) nil nil)) nil))
      nil))
    nil)
   ((mod_lt formula-decl nil tmod 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (/= const-decl "boolean" notequal nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sgn const-decl "int" tdiv nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   nil))
 (mod_sum_pos 0
  (mod_sum_pos-1 nil 3406631585
   ("" (skosimp*)
    (("" (expand "mod")
      (("" (expand "tdiv")
        (("" (lemma "floor_plus_int")
          (("" (inst - "k!1*m!1/m!1" "i!1/m!1")
            (("" (replace -1) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (floor_plus_int formula-decl nil floor_ceil nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers 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)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (integer nonempty-type-from-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)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv const-decl "integer" tdiv nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
 (mod_sum 0
  (mod_sum-1 nil 3406631585
   ("" (skosimp*)
    (("" (expand "mod")
      (("" (expand "tdiv")
        (("" (lemma "floor_plus_int")
          (("" (inst - "k!1*j!1/j!1" "i!1/j!1")
            (("" (replace -1) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (floor_plus_int formula-decl nil floor_ceil nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers 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)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (integer nonempty-type-from-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)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv const-decl "integer" tdiv nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
 (mod_it_is 0
  (mod_it_is-1 nil 3406631585
   ("" (skosimp*)
    (("" (replace -1)
      (("" (hide -1)
        (("" (lemma "mod_sum")
          (("" (inst - "b!1" "m!1" "c!1")
            (("" (replace -1)
              (("" (hide -1)
                (("" (rewrite "mod_lt")
                  (("1" (lift-if)
                    (("1" (expand "sgn") (("1" (propax) nil nil)) nil))
                    nil)
                   ("2" (expand "abs") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((mod_sum formula-decl nil tmod 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)
    (mod_lt formula-decl nil tmod nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sgn const-decl "int" tdiv nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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))
   nil))
 (mod_zero 0
  (mod_zero-1 nil 3406631585 ("" (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)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv const-decl "integer" tdiv nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
 (mod_0 0
  (mod_0-1 nil 3406631761
   ("" (skosimp*) (("" (rewrite "mod_zero") nil nil)) nil)
   ((mod_zero formula-decl nil tmod 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))
   shostak))
 (mod_one 0
  (mod_one-1 nil 3406631585
   ("" (grind)
    (("1" (rewrite "floor_small")
      (("1" (lift-if)
        (("1" (ground) (("1" (rewrite "pos_div_ge") nil nil)) nil))
        nil))
      nil)
     ("2" (rewrite "floor_small")
      (("2" (lift-if)
        (("2" (ground) (("2" (rewrite "pos_div_ge") nil nil)) nil))
        nil))
      nil))
    nil)
   ((integer nonempty-type-from-decl nil integers nil)
    (floor_small formula-decl nil floor_ceil nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
     real_defs 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)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (pos_div_ge formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_lt_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)
    (/= 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)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (mod_of_mod 0
  (mod_of_mod-1 nil 3406631585
   ("" (skosimp*)
    (("" (rewrite "mod")
      (("" (expand "tdiv")
        (("" (lemma "mod_sum")
          (("" (inst - "i!1+k!1" "m!1" "-floor(k!1/m!1)")
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mod const-decl "{k | abs(k) < abs(j)}" tmod 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)
    (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)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (mod_sum formula-decl nil tmod nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields 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]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (mod_pos 0
  (mod_pos-1 nil 3406631585
   ("" (skosimp*)
    (("" (typepred "mod(i!1,m!1)")
      (("" (tcc)
        (("" (lemma "both_sides_times_pos_le1")
          (("" (inst -1 "m!1" "floor(i!1 / m!1)" "i!1/m!1")
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod 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)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
     real_defs nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_minus_int_is_int application-judgement "int" 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)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (mod_TCC2 0
  (mod_TCC2-1 nil 3406631585
   ("" (skosimp*)
    (("" (assert) (("" (rewrite "mod_pos") nil nil)) nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (mod_pos formula-decl nil tmod nil))
   nil))
 (mod_to_rem 0
  (mod_to_rem-1 nil 3406631585
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "mod")
        (("" (lemma "rem_def2")
          (("" (inst?)
            (("" (inst -1 "i!1 - m!1 * floor(i!1 / m!1)")
              (("1" (expand "tdiv")
                (("1" (assert)
                  (("1" (hide 2)
                    (("1" (expand "divides") (("1" (inst?) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (assert)
                  (("2" (lemma "mod_pos")
                    (("2" (expand "mod")
                      (("2" (inst?)
                        (("2" (expand "tdiv") (("2" (inst?) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nil application-judgement "below(m)" tmod nil)
    (rem_def2 formula-decl nil modulo_arithmetic 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (integer nonempty-type-from-decl nil integers nil)
    (m!1 skolem-const-decl "posnat" tmod nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i!1 skolem-const-decl "int" tmod nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (mod nonempty-type-eq-decl nil euclidean_division nil)
    (divides const-decl "bool" divides nil)
    (tdiv const-decl "integer" tdiv nil)
    (mod_pos formula-decl nil tmod nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil))
   nil))
 (mod_0_divides 0
  (mod_0_divides-1 nil 3406631585
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "mod")
        (("1" (expand "divides")
          (("1" (inst + "tdiv(i!1,j!1)") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (expand "divides")
        (("2" (skosimp*)
          (("2" (replace -1) (("2" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((divides const-decl "bool" divides nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (tdiv const-decl "integer" tdiv nil)
    (integer nonempty-type-from-decl nil 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)
    (mod const-decl "{k | abs(k) < abs(j)}" tmod nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
   nil)))

[ Verzeichnis aufwärts0.25unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]