products/sources/formale sprachen/PVS/TRS image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: finite_sets_card_from.pvs   Sprache: PVS

Original von: PVS©

(prelude_A4
 (expt_neg_even_TCC1 0
  (expt_neg_even_TCC1-1 nil 3250069458 ("" (grind) nil nil)
   ((even? const-decl "bool" integers nil)) nil))
 (expt_neg_even_TCC2 0
  (expt_neg_even_TCC2-1 nil 3250069458 ("" (grind) nil nil)
   ((even? const-decl "bool" integers nil)) nil))
 (expt_neg_even 0
  (expt_neg_even-1 nil 3250069458
   ("" (expand "even?")
    (("" (skosimp*)
      (("" (replace -1)
        (("" (hide -1)
          (("" (rewrite "expt_times")
            (("" (rewrite "expt_times")
              (("" (case-replace "(-nx!1) ^ 2 = nx!1 ^ 2")
                (("" (hide 2) (("" (grind) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (expt def-decl "real" exponentiation nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (>= const-decl "bool" reals nil)
    (^ const-decl "real" exponentiation nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzreal nonempty-type-eq-decl nil reals 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)
    (expt_times formula-decl nil exponentiation nil)
    (even? const-decl "bool" integers nil))
   nil))
 (expt_neg_odd_TCC1 0
  (expt_neg_odd_TCC1-1 nil 3250069458 ("" (grind) nil nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd? const-decl "bool" integers nil))
   nil))
 (expt_neg_odd_TCC2 0
  (expt_neg_odd_TCC2-1 nil 3250069458 ("" (grind) nil nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd? const-decl "bool" integers nil))
   nil))
 (expt_neg_odd 0
  (expt_neg_odd-1 nil 3250069458
   ("" (expand "odd?")
    (("" (skosimp*)
      (("" (replace -1)
        (("" (case "j!1 >=0")
          (("1" (rewrite "expt_plus")
            (("1" (rewrite "expt_plus")
              (("1" (rewrite "expt_x1")
                (("1" (rewrite "expt_x1")
                  (("1"
                    (lemma "expt_neg_even" ("nx" "nx!1" "n" "2*j!1"))
                    (("1" (split -1)
                      (("1" (assertnil nil)
                       ("2" (hide 2)
                        (("2" (expand "even?")
                          (("2" (inst + "j!1"nil nil)) nil))
                        nil))
                      nil)
                     ("2" (assertnil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (typepred "n!1") (("2" (assertnil nil)) nil)) nil))
          nil))
        nil))
      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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (even? const-decl "bool" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (expt_neg_even formula-decl nil prelude_A4 nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (expt_plus formula-decl nil exponentiation nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (odd? const-decl "bool" integers nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (expt_0pn 0
  (expt_0pn-1 nil 3250069458 ("" (grind) nil nil)
   ((expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (nat_expt application-judgement "nat" exponentiation nil))
   nil))
 (expt_inverse_inv_TCC1 0
  (expt_inverse_inv_TCC1-1 nil 3250069458 ("" (grind) nil nilnil
   nil))
 (expt_inverse_inv 0
  (expt_inverse_inv-1 nil 3250069458
   ("" (skosimp*)
    (("" (rewrite "div_expt") (("" (rewrite "expt_1i"nil nil)) nil))
    nil)
   ((div_expt formula-decl nil exponentiation 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (expt_1i formula-decl nil exponentiation nil))
   nil))
 (expt_product_n0i_TCC1 0
  (expt_product_n0i_TCC1-1 nil 3250069458 ("" (grind) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (expt_product_n0i_TCC2 0
  (expt_product_n0i_TCC2-1 nil 3250069458 ("" (grind) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (expt_product_n0i 0
  (expt_product_n0i-1 nil 3250069458
   ("" (skosimp*)
    (("" (case-replace "x!1=0")
      (("1" (expand "^" 1 2)
        (("1" (expand "^" 1 1)
          (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil))
        nil)
       ("2" (case-replace "y!1=0")
        (("1" (expand "^" 2 1)
          (("1" (expand "^" 2 2)
            (("1" (expand "expt") (("1" (assertnil nil)) nil)) nil))
          nil)
         ("2" (rewrite "mult_expt"nil nil))
        nil))
      nil))
    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)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (mult_expt formula-decl nil exponentiation 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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (expt_division_TCC1 0
  (expt_division_TCC1-1 nil 3250069458 ("" (grind) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (expt_division_TCC2 0
  (expt_division_TCC2-1 nil 3250069458 ("" (grind) nil nilnil nil))
 (expt_division 0
  (expt_division-1 nil 3250069458
   ("" (skosimp*)
    ((""
      (lemma "expt_product_n0i" ("x" "x!1" "y" "1/n0y!1" "pn" "pn!1"))
      (("" (rewrite "expt_inverse_inv" -1) (("" (assertnil nil))
        nil))
      nil))
    nil)
   ((nzreal nonempty-type-eq-decl nil reals 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)
    (> 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)
    (expt_product_n0i formula-decl nil prelude_A4 nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzreal_exp application-judgement "nzreal" exponentiation nil)
    (expt_inverse_inv formula-decl nil prelude_A4 nil))
   nil))
 (A4_0_TCC1 0
  (A4_0_TCC1-1 nil 3250069458 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (A4_0 0
  (A4_0-1 nil 3250069458
   ("" (skosimp*)
    (("" (case "n!1 + 1 + y!1 > 0")
      (("1" (rewrite "div_mult_pos_le2")
        (("1" (rewrite "div_mult_pos_lt1") (("1" (assertnil nil))
          nil))
        nil)
       ("2" (assertnil nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
 (A4_1_TCC1 0
  (A4_1_TCC1-1 nil 3250069458 ("" (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)
    (> 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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (A4_1 0
  (A4_1-1 nil 3250069458
   ("" (skosimp*)
    (("" (typepred "pn!1")
      (("" (lemma "A4_0" ("y" "y!1" "n" "pn!1"))
        (("" (assert) (("" (flatten -1) (("" (assertnil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (A4_0 formula-decl nil prelude_A4 nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
 (A4_2 0
  (A4_2-1 nil 3250069458
   ("" (skosimp*)
    (("" (lemma "A4_0" ("y" "y!1" "n" "n!1"))
      (("" (lemma "trich_lt" ("x" "y!1" "y" "0"))
        (("" (split -1)
          (("1"
            (lemma "both_sides_times_neg_lt1"
             ("y" "-1" "x" "y!1" "nz" "-1"))
            (("1"
              (lemma "lt_times_lt_pos1"
               ("px" "y!1 * -1" "y" "1" "nnz" "n!1 / (n!1 + 1 + y!1)"
                "w" "1"))
              (("1"
                (lemma "both_sides_times_neg_lt1"
                 ("y" "-1" "x" "z!1" "nz" "-1"))
                (("1" (grind) nil nil)) nil)
               ("2" (assertnil nil) ("3" (assertnil nil)
               ("4" (assertnil nil))
              nil))
            nil)
           ("2" (replace -1) (("2" (grind) nil nil)) nil)
           ("3" (lemma "trich_lt" ("x" "n!1" "y" "0"))
            (("3" (split -1)
              (("1" (assertnil nil)
               ("2" (replace -1) (("2" (assertnil nil)) nil)
               ("3" (lemma "A4_1" ("y" "y!1" "pn" "n!1"))
                (("1"
                  (lemma "lt_times_lt_nn1"
                   ("nnx" "0" "y" "n!1 / (n!1 + 1 + y!1)" "nnz" "0" "w"
                    "y!1"))
                  (("1" (grind) nil nil) ("2" (assertnil nil)) nil)
                 ("2" (assertnil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (A4_0 formula-decl nil prelude_A4 nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (lt_times_lt_pos1 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (both_sides_times_neg_lt1 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (lt_times_lt_nn1 formula-decl nil prelude_aux nil)
    (nnreal type-eq-decl nil real_types nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (A4_1 formula-decl nil prelude_A4 nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (trich_lt formula-decl nil real_props nil))
   nil))
 (A4_3_n 0
  (A4_3_n-1 nil 3250069458
   ("" (skosimp*)
    (("" (lemma "A4_1" ("y" "y!1" "pn" "pn!1"))
      ((""
        (lemma "both_sides_times_neg_lt1"
         ("y" "pn!1 / (pn!1 + 1 + y!1)" "x" "1" "nz" "y!1"))
        (("1" (grind) nil nil) ("2" (assertnil nil)
         ("3" (assertnil 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)
    (>= 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)
    (A4_1 formula-decl nil prelude_A4 nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (both_sides_times_neg_lt1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (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))
   nil))
 (A4_3_0_TCC1 0
  (A4_3_0_TCC1-1 nil 3250069458 ("" (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)
    (> 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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (A4_3_0 0
  (A4_3_0-1 nil 3250069458 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> 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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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_times_even_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
     rationals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (A4_3_p_TCC1 0
  (A4_3_p_TCC1-1 nil 3250069458 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> 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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (A4_3_p 0
  (A4_3_p-1 nil 3250069458
   ("" (skosimp*)
    (("" (lemma "A4_1" ("pn" "pn!1" "y" "y!1"))
      (("" (assert)
        (("" (flatten -1)
          ((""
            (lemma "both_sides_times_pos_lt1"
             ("pz" "y!1" "x" "pn!1 / (1 + pn!1 + y!1)" "y" "1"))
            (("" (assertnil 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)
    (>= 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)
    (A4_1 formula-decl nil prelude_A4 nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types 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)
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   nil))
 (A4_4 0
  (A4_4-1 nil 3250069458
   ("" (skosimp*)
    (("" (lemma "A4_1" ("y" "y!1" "pn" "pn!1"))
      ((""
        (lemma "both_sides_plus_lt1" ("x" "-1" "y" "y!1" "z" "pn!1+1"))
        ((""
          (lemma "lt_le_transitivity"
           ("x" "0" "y" "pn!1" "z" "1+pn!1+y!1"))
          ((""
            (lemma "both_sides_plus1"
             ("x" "z!1" "y" "pn!1 * y!1 / (pn!1 + 1 + y!1)" "z"
              "(pn!1 + 1 + y!1)/(pn!1 + 1 + y!1)"))
            (("1" (copy -6)
              (("1" (replace -2 -7 rl)
                (("1" (rewrite "div_distributes" -7)
                  (("1" (rewrite "div_simp" -7)
                    (("1" (replace -7 1)
                      (("1" (replace -1 1)
                        (("1" (hide (-1 -2 -7))
                          (("1"
                            (lemma "both_sides_div_pos_lt1"
                             ("x" "pn!1 * x!1 * (1 + pn!1) * (1+y!1)"
                              "y" "pn!1 * y!1" "pz" "pn!1 + 1 + y!1"))
                            (("1"
                              (lemma "both_sides_times_pos_lt1"
                               ("x"
                                "(pn!1 + 1) * x!1 * (1 + y!
1)"
                                "y"
                                "y!1"
                                "pz"
                                "pn!1"))
                              (("1" (grind) nil nil)) nil)
                             ("2" (assertnil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assertnil nil))
              nil)
             ("2" (assertnil 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)
    (>= 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)
    (A4_1 formula-decl nil prelude_A4 nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (lt_le_transitivity formula-decl nil prelude_aux nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_distributes formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (both_sides_div_pos_lt1 formula-decl nil real_props nil)
    (even_minus_odd_is_odd application-judgement "odd_int" integers
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (div_simp formula-decl nil real_props 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)
    (both_sides_plus1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (both_sides_plus_lt1 formula-decl nil real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil))
 (A4_5pp_TCC1 0
  (A4_5pp_TCC1-1 nil 3250069458
   ("" (skosimp*) (("" (assertnil nil)) nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (A4_5pp 0
  (A4_5pp-1 nil 3250069458
   ("" (skolem!)
    (("" (flatten)
      (("" (induct "n")
        (("1" (skosimp*) (("1" (grind) nil nil)) nil)
         ("2" (skolem!)
          (("2" (skosimp*)
            (("2" (lemma "trich_lt" ("x" "j!1" "y" "0"))
              (("2" (split -1)
                (("1" (assertnil nil)
                 ("2" (replace -1)
                  (("2"
                    (lemma "div_mult_pos_lt2"
                     ("x" "x!1" "py" "1+y!1" "z" "y!1"))
                    (("1"
                      (lemma "lt_times_lt_nn1"
                       ("nnx" "0" "y" "y!1" "nnz" "0" "w" "y!1"))
                      (("1"
                        (lemma "both_sides_plus_lt1"
                         ("x" "0" "y" "y!1 * y!1" "z" "y!1"))
                        (("1"
                          (lemma "div_mult_pos_lt1"
                           ("z" "y!1" "py" "1+y!1" "x" "y!1"))
                          (("1" (grind) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (assertnil nil))
                    nil))
                  nil)
                 ("3" (name "z!1" "j!1*y!1/(j!1+1+y!1)")
                  (("1"
                    (lemma "A4_4"
                     ("y" "y!1" "z" "z!1" "pn" "j!1" "x" "x!1"))
                    (("1" (inst - "z!1")
                      (("1" (lemma "A4_1" ("y" "y!1" "pn" "j!1"))
                        (("1"
                          (lemma "lt_times_lt_nn1"
                           ("nnx" "0" "y" "j!1 / (j!1 + 1 + y!1)" "nnz"
                            "0" "w" "y!1"))
                          (("1" (replace -4)
                            (("1" (bash -3)
                              (("1"
                                (lemma
                                 "both_sides_plus1"
                                 ("y"
                                  "z!1"
                                  "x"
                                  "j!1 * y!1 / (j!1 + 1 + y!1)"
                                  "z"
                                  "(j!1 + 1 + y!1)/(j!1 + 1 + y!1)"))
                                (("1"
                                  (copy -6)
                                  (("1"
                                    (replace -2 -7 rl)
                                    (("1"
                                      (rewrite "div_distributes" -7)
                                      (("1"
                                        (rewrite "div_simp" -7)
                                        (("1"
                                          (replace -7 -9 rl)
                                          (("1"
                                            (lemma
                                             "lt_times_lt_nn1"
                                             ("nnx"
                                              "0"
                                              "y"
                                              "y!1"
                                              "nnz"
                                              "0"
                                              "w"
                                              "y!1"))
                                            (("1"
                                              (lemma
                                               "both_sides_plus_lt1"
                                               ("x"
                                                "0"
                                                "y"
                                                "y!1 * y!1"
                                                "z"
                                                "y!1"))
                                              (("1"
                                                (lemma
                                                 "div_mult_pos_lt1"
                                                 ("z"
                                                  "y!1"
                                                  "x"
                                                  "y!1"
                                                  "py"
                                                  "1+y!1"))
                                                (("1"
                                                  (lemma
                                                   "div_mult_pos_lt2"
                                                   ("x"
                                                    "x!1*(1+j!1)"
                                                    "py"
                                                    "1+y!1"
                                                    "z"
                                                    "y!1"))
                                                  (("1"
                                                    (lemma
                                                     "expt_plus"
                                                     ("n0x"
                                                      "1+x!1"
                                                      "i"
                                                      "1"
                                                      "j"
                                                      "j!1"))
                                                    (("1"
                                                      (replace -1 1)
                                                      (("1"
                                                        (name-replace
                                                         "AA"
                                                         "(1 + x!1) ^ j!1")
                                                        (("1"
                                                          (hide -1)
                                                          (("1"
                                                            (replace
                                                             -14)
                                                            (("1"
                                                              (simplify
                                                               -4)
                                                              (("1"
                                                                (replace
                                                                 -4)
                                                                (("1"
                                                                  (simplify
                                                                   -3)
                                                                  (("1"
                                                                    (replace
                                                                     -3)
                                                                    (("1"
                                                                      (simplify
                                                                       -2)
                                                                      (("1"
                                                                        (replace
                                                                         -15
                                                                         -1)
                                                                        (("1"
                                                                          (simplify
                                                                           -1)
                                                                          (("1"
                                                                            (reveal
                                                                             -2)
                                                                            (("1"
                                                                              (lemma
                                                                               "posreal_expt")
                                                                              (("1"
                                                                                (inst
                                                                                 -
                                                                                 "j!1"
                                                                                 "1+x!1")
                                                                                (("1"
                                                                                  (expand
                                                                                   "^")
                                                                                  (("1"
                                                                                    (replace
                                                                                     -2
                                                                                     -1)
                                                                                    (("1"
                                                                                      (hide
                                                                                       -2)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "expt")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "expt")
                                                                                          (("1"
                                                                                            (lemma
                                                                                             "lt_times_lt_pos1"
                                                                                             ("px"
                                                                                              "AA"
                                                                                              "y"
                                                                                              "((1+j!1)*(1+y!1))/(1 + j!1 + y!1)"
                                                                                              "nnz"
                                                                                              "1+x!1"
                                                                                              "w"
                                                                                              "(1 + j!1 + y!1)/(1+j!1)"))
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "div_times"
                                                                                               ("x"
                                                                                                "(1 + y!1)*(1 + j!1)"
                                                                                                "n0x"
                                                                                                "(1 + j!1 + y!1)"
                                                                                                "y"
                                                                                                "(1 + j!1 + y!1)"
                                                                                                "n0y"
                                                                                                "1 + j!1"))
                                                                                              (("1"
                                                                                                (replace
                                                                                                 -1
                                                                                                 -2)
                                                                                                (("1"
                                                                                                  (lemma
                                                                                                   "div_cancel1"
                                                                                                   ("x"
                                                                                                    "1+y!1"
                                                                                                    "n0z"
                                                                                                    "(1 + j!1 + y!1) * (1 + j!1)"))
                                                                                                  (("1"
                                                                                                    (replace
                                                                                                     -1
                                                                                                     -3)
                                                                                                    (("1"
                                                                                                      (hide
                                                                                                       (-1
                                                                                                        -2))
                                                                                                      (("1"
                                                                                                        (lemma
                                                                                                         "div_mult_pos_lt2"
                                                                                                         ("x"
                                                                                                          "x!1"
                                                                                                          "py"
                                                                                                          "(1+y!1)*(1+j!1)"
                                                                                                          "z"
                                                                                                          "y!1"))
                                                                                                        (("1"
                                                                                                          (replace
                                                                                                           -18
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (lemma
                                                                                                             "both_sides_plus_lt1"
                                                                                                             ("x"
                                                                                                              "y!1 / (1 + y!1)"
                                                                                                              "y"
                                                                                                              "y!1"
                                                                                                              "z"
                                                                                                              "1+j!1"))
                                                                                                            (("1"
                                                                                                              (replace
                                                                                                               -6
                                                                                                               -1)
                                                                                                              (("1"
                                                                                                                (lemma
                                                                                                                 "lt_le_transitivity"
                                                                                                                 ("x"
                                                                                                                  "(1+j!1)*x!1"
                                                                                                                  "y"
                                                                                                                  "y!1 / (1 + y!1)"
                                                                                                                  "z"
                                                                                                                  "y!1"))
                                                                                                                (("1"
                                                                                                                  (lemma
                                                                                                                   "both_sides_plus_lt1"
                                                                                                                   ("x"
                                                                                                                    "(1 + j!1) * x!1"
                                                                                                                    "y"
                                                                                                                    "y!1"
                                                                                                                    "z"
                                                                                                                    "1 + j!1"))
                                                                                                                  (("1"
                                                                                                                    (lemma
                                                                                                                     "div_mult_pos_lt2"
                                                                                                                     ("x"
                                                                                                                      "x!1+1"
                                                                                                                      "py"
                                                                                                                      "1 + j!1"
                                                                                                                      "z"
                                                                                                                      "y!1+1+j!1"))
                                                                                                                    (("1"
                                                                                                                      (grind)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (lemma
                                                                                                           "lt_times_lt_nn1"
                                                                                                           ("nnx"
                                                                                                            "0"
                                                                                                            "y"
                                                                                                            "1+j!1"
                                                                                                            "nnz"
                                                                                                            "0"
                                                                                                            "w"
                                                                                                            "1+y!1"))
                                                                                                          (("2"
                                                                                                            (grind)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil)
                                                                                                   ("2"
                                                                                                    (assert)
                                                                                                    (("2"
                                                                                                      (lemma
                                                                                                       "lt_times_lt_nn1"
                                                                                                       ("nnx"
                                                                                                        "0"
                                                                                                        "y"
                                                                                                        "1 + j!1 + y!1"
                                                                                                        "nnz"
                                                                                                        "0"
                                                                                                        "w"
                                                                                                        "1 + j!1"))
                                                                                                      (("2"
                                                                                                        (grind)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.77 Sekunden  (vorverarbeitet)  ¤





Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff