Quelle  tdiv.prf   Sprache: unbekannt

(tdiv
 (tdiv_TCC1 0
  (tdiv_TCC1-1 nil 3407849557
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "tdiv")
        (("" (lemma "pos_div_ge") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pos_div_ge formula-decl nil real_props nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (tdiv_TCC2 0
  (tdiv_TCC2-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "pos_div_ge") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((tdiv const-decl "integer" tdiv nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nprat_div_posrat_is_nprat application-judgement "nprat" rationals
     nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pos_div_ge formula-decl nil real_props nil))
   nil))
 (tdiv_TCC3 0
  (tdiv_TCC3-1 nil 3407849557
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "tdiv")
        (("" (typepred "negi!1")
          (("" (typepred "ngi2!1")
            (("" (hide -1 -3) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (negint nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nonpos_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)
    (<= 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)
    (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)
    (negrat_div_negrat_is_posrat application-judgement "posrat"
     rationals nil)
    (tdiv const-decl "integer" tdiv nil))
   nil))
 (tdiv_TCC4 0
  (tdiv_TCC4-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "pos_div_ge")
        (("" (inst?) (("" (flatten) (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (/= const-decl "boolean" notequal nil)
    (nonzero_real nonempty-type-eq-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)
    (nonpos_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (negint 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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (nnrrat_div_negrat_is_nprat application-judgement "nprat" rationals
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_div_ge formula-decl nil real_props nil))
   nil))
 (tdiv_nat 0
  (tdiv_nat-1 nil 3407849557
   ("" (skosimp*)
    (("" (lift-if)
      (("" (expand "tdiv")
        (("" (split 1)
          (("1" (flatten)
            (("1" (case "(n!1 - m!1) / m!1 = n!1/m!1 - 1")
              (("1" (lemma "floor_plus_int")
                (("1" (inst -1 "-1" "n!1/m!1") (("1" (ground) nil nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil)
           ("2" (flatten)
            (("2" (lemma "floor_small")
              (("2" (inst?)
                (("2" (expand "abs") (("2" (assert) nil nil)) nil))
                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)
    (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)
    (- 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)
    (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)
    (rat_minus_rat_is_rat application-judgement "rat" rationals nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (integer nonempty-type-from-decl nil integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (floor_plus_int formula-decl nil floor_ceil nil)
    (floor_small formula-decl nil floor_ceil 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)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (tdiv const-decl "integer" tdiv nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (tdiv_neg_d 0
  (tdiv_neg_d-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lift-if)
        (("" (lemma "floor_neg")
          (("" (inst -1 "i!1/j!1")
            (("" (lift-if)
              (("" (expand "integer?") (("" (ground) nil 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)
    (tdiv const-decl "integer" tdiv nil)
    (floor_neg formula-decl nil floor_ceil nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_rat_is_rat application-judgement "rat" rationals nil)
    (integer? const-decl "bool" integers nil)
    (minus_int_is_int application-judgement "int" integers 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)
    (/ 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)
    (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))
 (tdiv_neg 0
  (tdiv_neg-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lift-if)
        (("" (lemma "floor_neg")
          (("" (inst -1 "i!1/j!1")
            (("" (lift-if)
              (("" (expand "integer?") (("" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv const-decl "integer" tdiv nil)
    (floor_neg formula-decl nil floor_ceil nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_rat_is_rat application-judgement "rat" rationals nil)
    (integer? const-decl "bool" integers 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)
    (/ 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)
    (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))
 (tdiv_def 0
  (tdiv_def-1 nil 3407849557
   ("" (skosimp*)
    (("" (lift-if)
      (("" (split 1)
        (("1" (flatten)
          (("1" (lemma "tdiv_nat")
            (("1" (inst?)
              (("1" (lift-if) (("1" (assert) nil nil)) nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (split 2)
            (("1" (flatten)
              (("1" (lemma "tdiv_nat")
                (("1" (inst?)
                  (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil)
             ("2" (flatten)
              (("2" (split 2)
                (("1" (flatten)
                  (("1" (lemma "tdiv_neg")
                    (("1" (inst?)
                      (("1" (lift-if) (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (lemma "tdiv_neg")
                    (("2" (inst?)
                      (("2" (lift-if) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minus_odd_is_odd application-judgement "odd_int" integers nil)
    (/= const-decl "boolean" notequal nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv_neg formula-decl nil tdiv nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (i!1 skolem-const-decl "int" tdiv 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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (tdiv_nat formula-decl nil tdiv nil))
   nil))
 (tdiv_sgn 0
  (tdiv_sgn-1 nil 3407849557
   ("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
    nil)
   ((minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (tdiv const-decl "integer" tdiv nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
   nil))
 (tdiv_value 0
  (tdiv_value-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "floor_val")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (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)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (floor_val formula-decl nil floor_ceil nil))
   nil))
 (tdiv_zero 0
  (tdiv_zero-1 nil 3407849557
   ("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
    nil)
   ((tdiv const-decl "integer" tdiv nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
   nil))
 (tdiv_one 0
  (tdiv_one-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "floor_small")
        (("" (inst -1 "1" "j!1")
          (("" (expand "abs" -1 1)
            (("" (assert)
              (("" (lemma "pos_div_ge")
                (("" (inst -1 "j!1" "1")
                  (("" (flatten)
                    (("" (assert)
                      (("" (lift-if)
                        (("" (lemma "div_eq_zero")
                          (("" (inst -1 "j!1" "1")
                            (("" (ground) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
     real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_eq_zero formula-decl nil real_props nil)
    (pos_div_ge formula-decl nil real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (floor_small formula-decl nil floor_ceil nil))
   nil))
 (tdiv_eq_arg 0
  (tdiv_eq_arg-1 nil 3407849557
   ("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
    nil)
   ((tdiv const-decl "integer" tdiv nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil))
   nil))
 (tdiv_by_one 0
  (tdiv_by_one-1 nil 3407849557
   ("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
    nil)
   ((tdiv const-decl "integer" tdiv nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
   nil))
 (tdiv_eq_0 0
  (tdiv_eq_0-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "floor_eq_0")
        (("" (inst -1 "i!1/j!1")
          (("" (lemma "pos_div_ge")
            (("" (inst?)
              (("" (lemma "div_eq_zero")
                (("" (inst?)
                  (("" (flatten)
                    (("" (expand "sgn")
                      (("" (expand "abs")
                        (("" (lift-if)
                          (("" (lift-if)
                            (("" (assert)
                              ((""
                                (ground)
                                (("1"
                                  (hide 1 3)
                                  (("1"
                                    (lemma "both_sides_times_pos_lt1")
                                    (("1"
                                      (inst -1 "-j!1" "1" "i!1/j!1")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma "both_sides_times_pos_lt1")
                                  (("2"
                                    (inst -1 "j!1" "1" "i!1/j!1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (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)
    (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)
    (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)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (sgn const-decl "int" tdiv 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)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (rat_times_rat_is_rat application-judgement "rat" rationals nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_int_is_int application-judgement "int" 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)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (div_eq_zero formula-decl nil real_props nil)
    (pos_div_ge formula-decl nil real_props nil)
    (floor_eq_0 formula-decl nil floor_ceil nil))
   nil))
 (tdiv_lt 0
  (tdiv_lt-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "floor_small")
        (("" (inst?)
          (("" (assert)
            ((""
              (case "(i!1 = 0 OR sgn(i!1) = sgn(j!1)) = (i!1 / j!1 >= 0)")
              (("1" (lift-if)
                (("1" (expand "sgn") (("1" (ground) nil nil)) nil))
                nil)
               ("2" (hide -1 -2 2)
                (("2" (iff 1)
                  (("2" (split 1)
                    (("1" (flatten)
                      (("1" (expand "sgn")
                        (("1" (ground)
                          (("1" (lemma "pos_div_ge")
                            (("1" (inst -1 "j!1" "i!1")
                              (("1"
                                (assert)
                                (("1"
                                  (lift-if)
                                  (("1" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (flatten)
                      (("2" (expand "sgn")
                        (("2" (lift-if)
                          (("2" (lift-if)
                            (("2" (lemma "pos_div_ge")
                              (("2"
                                (inst -1 "j!1" "i!1")
                                (("2" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (int nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (nonzero_integer nonempty-type-eq-decl nil integers 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)
    (>= const-decl "bool" reals nil) (sgn const-decl "int" tdiv nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (floor_small formula-decl nil floor_ceil nil))
   nil))
 (tdiv_parity 0
  (tdiv_parity-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (expand "sgn")
        (("" (lift-if)
          (("" (lemma "pos_div_ge")
            (("" (inst?)
              (("" (flatten)
                (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (/= const-decl "boolean" notequal nil)
    (nonzero_real nonempty-type-eq-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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pos_div_ge formula-decl nil real_props nil)
    (sgn const-decl "int" tdiv nil))
   nil))
 (tdiv_parity_neg 0
  (tdiv_parity_neg-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (expand "sgn")
        (("" (lift-if)
          (("" (lemma "pos_div_ge")
            (("" (inst?)
              (("" (flatten)
                (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv 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)
    (/= const-decl "boolean" notequal nil)
    (nonzero_real nonempty-type-eq-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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pos_div_ge formula-decl nil real_props nil)
    (sgn const-decl "int" tdiv nil))
   nil))
 (tdiv_smaller 0
  (tdiv_smaller-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (assert)
        (("" (typepred "floor(n!1 / m!1)")
          (("" (lemma "both_sides_times_pos_lt1")
            (("" (inst -1 "m!1" "floor(n!1 / m!1)" "n!1 / m!1")
              (("" (flatten)
                (("" (ground)
                  (("" (case "floor(n!1 / m!1) = n!1 / m!1")
                    (("1" (ground)
                      (("1" (replace -1)
                        (("1" (auto-rewrite-theory "real_props")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv const-decl "integer" tdiv nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (<= 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_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)
    (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)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil))
   nil))
 (tdiv_abs 0
  (tdiv_abs-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (expand "abs")
        (("" (lift-if)
          (("" (lift-if)
            (("" (lift-if)
              (("" (lemma "floor_neg")
                (("" (inst?)
                  (("" (lift-if)
                    (("" (expand "sgn")
                      (("" (lift-if)
                        (("" (assert)
                          (("" (lemma "pos_div_ge")
                            (("" (expand "integer?")
                              ((""
                                (inst?)
                                ((""
                                  (split +)
                                  (("1"
                                    (flatten)
                                    (("1" (ground) nil nil))
                                    nil)
                                   ("2"
                                    (flatten)
                                    (("2"
                                      (ground)
                                      (("2"
                                        (lift-if)
                                        (("2" (ground) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      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)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (tdiv const-decl "integer" tdiv nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers 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)
    (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)
    (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)
    (sgn const-decl "int" tdiv nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (integer? const-decl "bool" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" 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)
    (minus_rat_is_rat application-judgement "rat" rationals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (pos_div_ge formula-decl nil real_props nil)
    (floor_neg formula-decl nil floor_ceil nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   nil))
 (tdiv_max 0
  (tdiv_max-1 nil 3407849557
   ("" (skosimp*)
    (("" (lemma "tdiv_smaller")
      (("" (inst -1 "abs(j!1)" "abs(i!1)")
        (("" (lemma "tdiv_abs")
          (("" (inst?)
            (("" (replace -1)
              (("" (hide -1)
                (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tdiv_smaller formula-decl nil tdiv nil)
    (tdiv_abs formula-decl nil tdiv nil)
    (nil application-judgement "nat" tdiv nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal 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)
    (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)
    (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))
   nil))
 (tdiv_multiple 0
  (tdiv_multiple-1 nil 3407849557
   ("" (skosimp*) (("" (expand "tdiv") (("" (assert) nil nil)) nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (tdiv const-decl "integer" tdiv nil)
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil))
   nil))
 (tdiv_sum 0
  (tdiv_sum-1 nil 3407849557
   ("" (skosimp*)
    (("" (expand "tdiv")
      (("" (lemma "floor_plus_int")
        (("" (inst -1 "k!1*j!1/j!1" "i!1/j!1") (("" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (tdiv const-decl "integer" tdiv 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)
    (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)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nonzero_integer nonempty-type-eq-decl nil integers nil)
    (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
    (floor_plus_int formula-decl nil floor_ceil nil))
   nil)))