Quelle cauchy.prf Sprache: Lisp

(cauchy
(cauchy_real_TCC1 0
  (cauchy_real_TCC1-1 nil 3250063205
   ("" (expand "cauchy_real?")
    (("" (inst 1 "0") (("" (grind) nil nil)) nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (^ const-decl "real" exponentiation nil)
    (cauchy_real? const-decl "bool" cauchy nil))
   nil))
(cauchy_nzreal_TCC1 0
  (cauchy_nzreal_TCC1-1 nil 3250063205
   ("" (expand "cauchy_nzreal?")
    (("" (inst 1 "1") (("" (grind) nil nil)) nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (^ const-decl "real" exponentiation nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil))
   nil))
(cauchy_nnreal_TCC1 0
  (cauchy_nnreal_TCC1-1 nil 3250063205
   ("" (expand "cauchy_nnreal?")
    (("" (inst 1 "1") (("" (grind) nil nil)) nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (^ const-decl "real" exponentiation nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil))
   nil))
(cauchy_npreal_TCC1 0
  (cauchy_npreal_TCC1-1 nil 3250063205
   ("" (expand "cauchy_npreal?")
    (("" (inst + "0") (("" (grind) nil nil)) nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil)
    (npreal type-eq-decl nil real_types nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (^ const-decl "real" exponentiation nil)
    (cauchy_npreal? const-decl "bool" cauchy nil))
   nil))
(cauchy_posreal_TCC1 0
  (cauchy_posreal_TCC1-1 nil 3250063205
   ("" (expand "cauchy_posreal?")
    (("" (inst + "1")
      (("" (expand "cauchy_prop") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_posreal? const-decl "bool" cauchy nil))
   nil))
(cauchy_negreal_TCC1 0
  (cauchy_negreal_TCC1-1 nil 3250063205
   ("" (expand "cauchy_negreal?")
    (("" (inst + "-1") (("" (grind) nil nil)) nil)) nil)
   ((minus_odd_is_odd application-judgement "odd_int" 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (^ const-decl "real" exponentiation nil)
    (cauchy_negreal? const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(cauchy_smallreal_TCC1 0
  (cauchy_smallreal_TCC1-1 nil 3250063205
   ("" (expand "cauchy_smallreal?")
    (("" (inst + "0")
      (("" (expand "cauchy_prop") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (smallreal nonempty-type-eq-decl nil prelude_aux nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_smallreal? const-decl "bool" cauchy nil))
   nil))
(subtype_TCC1 0
  (subtype_TCC1-1 nil 3250063205
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_nzreal?")
        (("" (expand "cauchy_real?")
          (("" (skosimp) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_nzreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nzreal? const-decl "bool" cauchy 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)
    (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)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
(subtype_TCC2 0
  (subtype_TCC2-1 nil 3250063205
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_nnreal?")
        (("" (expand "cauchy_real?")
          (("" (skosimp*) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nnreal? const-decl "bool" cauchy 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)
    (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)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nnreal type-eq-decl nil real_types nil))
   shostak))
(subtype_TCC3 0
  (subtype_TCC3-1 nil 3250063205
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_real?")
        (("" (expand "cauchy_npreal?")
          (("" (skosimp*) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_npreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_npreal? const-decl "bool" cauchy 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)
    (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)
    (npreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (cauchy_real? const-decl "bool" cauchy nil))
   shostak))
(subtype_TCC4 0
  (subtype_TCC4-1 nil 3250063205
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_nnreal?")
        (("" (expand "cauchy_posreal?")
          (("" (skosimp*) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_posreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_posreal? const-decl "bool" cauchy 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)
    (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)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil))
   shostak))
(subtype_TCC5 0
  (subtype_TCC5-1 nil 3250063206
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_nzreal?")
        (("" (expand "cauchy_posreal?")
          (("" (skosimp*) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_posreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_posreal? const-decl "bool" cauchy 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)
    (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)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (cauchy_nzreal? const-decl "bool" cauchy nil))
   shostak))
(subtype_TCC6 0
  (subtype_TCC6-1 nil 3250063206
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_nzreal?")
        (("" (expand "cauchy_negreal?")
          (("" (skosimp*) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_negreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_negreal? const-decl "bool" cauchy 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)
    (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)
    (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)
    (cauchy_nzreal? const-decl "bool" cauchy nil))
   shostak))
(subtype_TCC7 0
  (subtype_TCC7-1 nil 3250063206
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_npreal?")
        (("" (expand "cauchy_negreal?")
          (("" (skosimp*) (("" (inst 1 "x!2") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_negreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_negreal? const-decl "bool" cauchy 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)
    (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)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (npreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (cauchy_npreal? const-decl "bool" cauchy nil))
   shostak))
(subtype_TCC8 0
  (subtype_TCC8-1 nil 3250063206
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "cauchy_real?")
        (("" (expand "cauchy_smallreal?")
          (("" (skosimp*) (("" (inst 1 "sx!1") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cauchy_smallreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_smallreal? const-decl "bool" cauchy 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)
    (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)
    (smallreal nonempty-type-eq-decl nil prelude_aux nil)
    (- const-decl "[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)
    (cauchy_real? const-decl "bool" cauchy nil))
   shostak))
(cauchy_zero_TCC1 0
  (cauchy_zero_TCC1-1 nil 3250063205
   ("" (expand "cauchy_nnreal?")
    (("" (inst 1 "0") (("" (grind) nil nil)) nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (^ const-decl "real" exponentiation nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil))
   nil))
(unique_cauchy_zero 0
  (unique_cauchy_zero-1 nil 3250063205
   ("" (skosimp*)
    (("" (expand "cauchy_prop")
      (("" (expand "cauchy_zero")
        (("" (lemma "trich_lt" ("x" "x!1" "y" "0"))
          (("" (split -1)
            (("1" (lemma "epsilon_log2" ("px" "-x!1"))
              (("1" (skolem!)
                (("1"
                  (lemma "div_mult_pos_lt1"
                   ("z" "1" "py" "2^p!1" "x" "-x!1"))
                  (("1"
                    (lemma "both_sides_times_neg_lt1"
                     ("y" "1" "nz" "-1" "x" "-x!1 * 2 ^ p!1"))
                    (("1" (split)
                      (("1" (flatten)
                        (("1" (inst - "p!1")
                          (("1" (assert) (("1" (grind) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (flatten 1)
                        (("2" (skolem!)
                          (("2" (replace -1)
                            (("2"
                              (lemma "expt_ge1" ("b" "2" "n" "p!2"))
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil)
             ("2" (replace -1)
              (("2" (split)
                (("1" (assert) nil nil)
                 ("2" (flatten)
                  (("2" (skolem!)
                    (("2" (lemma "expt_ge1" ("b" "2" "n" "p!1"))
                      (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("3" (lemma "epsilon_log2" ("px" "x!1"))
              (("1" (skolem!)
                (("1"
                  (lemma "div_mult_pos_lt1"
                   ("z" "1" "py" "2^p!1" "x" "x!1"))
                  (("1" (split 1)
                    (("1" (flatten 1)
                      (("1" (inst - "p!1")
                        (("1" (assert) (("1" (grind) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (flatten 1)
                      (("2" (skolem!)
                        (("2" (replace -1) (("2" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy 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)
    (trich_lt formula-decl nil real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil 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)
    (epsilon_log2 formula-decl nil appendix nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" 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)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (expt_ge1 formula-decl nil exponentiation nil)
    (above nonempty-type-eq-decl nil integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cauchy_zero const-decl "cauchy_nnreal" cauchy nil))
   nil))
(unique_cauchy_zero2 0
  (unique_cauchy_zero2-1 nil 3250063205
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (expand "cauchy_prop")
          (("1" (skolem!)
            (("1" (expand "cauchy_zero")
              (("1" (inst - "p!1")
                (("1" (flatten)
                  (("1" (rewrite "zero_times1")
                    (("1" (rewrite "lt_equiv_le_plus_one" -1)
                      (("1" (rewrite "lt_plus_one_equiv_le" -2)
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (flatten)
        (("2"
          (lemma "extensionality_postulate"
           ("f" "cx!1" "g" "cauchy_zero"))
          (("2" (lemma "unique_cauchy_zero" ("x" "0"))
            (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_exp application-judgement "posint" exponentiation nil)
    (cauchy_prop const-decl "bool" cauchy nil)
    (cauchy_zero const-decl "cauchy_nnreal" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (lt_equiv_le_plus_one formula-decl nil prelude_aux nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lt_plus_one_equiv_le formula-decl nil prelude_aux nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (zero_times1 formula-decl nil real_props 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)
    (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil)
    (extensionality_postulate formula-decl nil functions nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (unique_cauchy_zero formula-decl nil cauchy nil))
   nil))
(unique_cauchy_zero3 0
  (unique_cauchy_zero3-1 nil 3250063205
   ("" (skosimp*)
    ((""
      (lemma "extensionality_postulate" ("f" "cx!1" "g" "cauchy_zero"))
      (("" (lemma "unique_cauchy_zero2" ("cx" "cx!1"))
        (("" (grind) 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)
    (cauchy_zero const-decl "cauchy_nnreal" cauchy nil)
    (cauchy_nnreal nonempty-type-eq-decl nil cauchy nil)
    (cauchy_nnreal? const-decl "bool" cauchy nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (extensionality_postulate formula-decl nil functions nil)
    (unique_cauchy_zero2 formula-decl nil cauchy nil))
   nil)))

quality99%

¤ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.