Quelle convergence_sequences.prf Sprache: Lisp

(convergence_sequences
(unique_limit 0
  (unique_limit-1 nil 3253549181
   ("" (skosimp)
    (("" (expand "convergence")
      (("" (rewrite "abs_diff_0")
        (("" (name "eps" "abs(l1!1 - l2!1)/3")
          (("" (assert)
            (("" (inst -2 "eps")
              (("" (inst -3 "eps")
                (("" (skolem!)
                  (("" (skolem!)
                    (("" (inst -2 "n!1+n!2")
                      (("" (inst -3 "n!1+n!2")
                        (("" (assert)
                          (("" (lemma "triangle2")
                            ((""
                              (inst -1 "eps" "eps" "l1!1"
                               "u!1(n!1+n!2)" "l2!1")
                              (("" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" convergence_sequences nil)
    (nnreal type-eq-decl nil real_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (sequence type-eq-decl nil sequences nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (triangle2 formula-decl nil abs_lems "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (abs_diff_0 formula-decl nil abs_lems "reals/"))
   nil))
(limit_lemma 0
  (limit_lemma-1 nil 3253549181
   ("" (skolem-typepred)
    (("" (name-replace "ll" "limit(v!1)" :hide? nil)
      (("" (expand "limit")
        (("" (expand "convergent?")
          ((""
            (lemma "epsilon_ax"
             ("p" "LAMBDA (l: real): convergence(v!1, l)"))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (limit const-decl "real" convergence_sequences nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (convergence const-decl "bool" convergence_sequences nil)
    (convergent? const-decl "bool" convergence_sequences nil)
    (sequence type-eq-decl nil sequences 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))
   nil))
(limit_def 0
  (limit_def-1 nil 3253549181
   ("" (skolem!)
    (("" (use "limit_lemma")
      (("" (ground)
        (("" (use "unique_limit") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((limit_lemma formula-decl nil convergence_sequences nil)
    (convergent? const-decl "bool" convergence_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (unique_limit formula-decl nil convergence_sequences nil)
    (limit const-decl "real" convergence_sequences nil))
   nil))
(convergence_subsequence 0
  (convergence_subsequence-1 nil 3253549181
   (""
    (grind :defs nil :rewrites ("subseq" "convergence") :if-match nil)
    (("" (delete -1 -2 -3 -4)
      (("" (inst -1 "epsilon!1")
        (("" (skolem!)
          (("" (inst 1 "n!1")
            (("" (skosimp)
              (("" (inst? -2)
                (("" (replace -2)
                  (("" (inst?)
                    (("" (assert)
                      (("" (use "extract_incr3")
                        (("" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (extract_incr3 formula-decl nil sequence_props 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)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (extraction type-eq-decl nil sequence_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (subseq const-decl "bool" sequence_props nil)
    (convergence const-decl "bool" convergence_sequences nil))
   nil))
(limit_accumulation 0
  (limit_accumulation-1 nil 3253549181
   (""
    (grind :defs nil :rewrites ("convergence" "accumulation") :if-match
     nil)
    (("" (inst?)
      (("" (skolem!)
        (("" (inst -5 "n!1+n!2")
          (("" (inst 1 "n!1+n!2") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (>= 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)
    (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)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (accumulation const-decl "bool" convergence_sequences nil)
    (convergence const-decl "bool" convergence_sequences nil))
   nil))
(g_TCC1 0
  (g_TCC1-1 nil 3253549181 ("" (skosimp) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(g_TCC2 0
  (g_TCC2-1 nil 3253549181 ("" (skosimp) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(g_TCC3 0 (g_TCC3-1 nil 3253549181 ("" (skosimp*) nil nil) nil nil))
(g_prop 0
  (g_prop-1 nil 3253549181
   ("" (skosimp*)
    (("" (expand "accumulation")
      (("" (name-replace "y" "g(u!1, a!1)(n!1 + 1)" :hide? nil)
        (("" (expand "g" -1)
          (("" (assert)
            ((""
              (lemma "epsilon_ax"
               ("p"
                "LAMBDA (i: nat): g(u!1, a!1)(n!1) < i AND abs(u!1(i) - a!1) < 1 / (1 + n!1)"))
              (("" (replace -2)
                (("" (split -1)
                  (("1" (assert) nil nil)
                   ("2" (inst -2 "1/(1+n!1)" "g(u!1, a!1)(n!1) + 1")
                    (("2" (skosimp)
                      (("2" (inst 1 "i!1") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((accumulation const-decl "bool" convergence_sequences nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (g def-decl "nat" convergence_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(g_increasing 0
  (g_increasing-1 nil 3253549181
   ("" (skosimp)
    (("" (rewrite "strict_incr_condition")
      (("" (skolem!)
        (("" (forward-chain "g_prop")
          (("" (inst?) (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((strict_incr_condition formula-decl nil sequence_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (g def-decl "nat" convergence_sequences nil)
    (g_prop formula-decl nil convergence_sequences nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
(g_convergence 0
  (g_convergence-1 nil 3253549181
   ("" (skosimp*)
    (("" (forward-chain "g_prop")
      (("" (inst -1 "n!1") (("" (flatten) nil nil)) nil)) nil))
    nil)
   ((g_prop formula-decl nil convergence_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(accumulation_subsequence 0
  (accumulation_subsequence-1 nil 3253549181
   ("" (skolem!)
    (("" (prop)
      (("1" (inst 1 "LAMBDA (i : nat) : u!1(g(u!1, a!1)(i))")
        (("1" (split)
          (("1" (forward-chain "g_increasing")
            (("1" (expand "subseq")
              (("1" (inst 1 "g(u!1, a!1)") (("1" (skolem!) nil nil))
                nil))
              nil))
            nil)
           ("2" (forward-chain "g_convergence")
            (("2" (expand "convergence")
              (("2" (skolem!)
                (("2" (lemma "archimedean2" ("x" "epsilon!1"))
                  (("2" (skolem!)
                    (("2" (inst 1 "a!2")
                      (("2" (skosimp)
                        (("2" (assert)
                          (("2" (inst -2 "i!1 - 1")
                            (("2" (assert)
                              (("2"
                                (case "1/i!1 <= 1/a!2")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (rewrite "both_sides_div_pos_le2")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2"
        (grind :defs nil :rewrites
         ("subseq" "convergence" "accumulation") :if-match nil)
        (("2" (inst? -6)
          (("2" (skolem!)
            (("2" (inst -5 "n!1 + n!2")
              (("2" (inst -6 "n!1+n!2")
                (("2" (inst?)
                  (("2" (assert)
                    (("2" (assert)
                      (("2" (use "extract_incr3")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subseq const-decl "bool" sequence_props nil)
    (extraction type-eq-decl nil sequence_props nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (u!1 skolem-const-decl "sequence[real]" convergence_sequences nil)
    (a!1 skolem-const-decl "real" convergence_sequences nil)
    (g_increasing formula-decl nil convergence_sequences nil)
    (convergence const-decl "bool" convergence_sequences nil)
    (archimedean2 formula-decl nil real_facts "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_div_pos_le2 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (<= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (g_convergence formula-decl nil convergence_sequences nil)
    (g def-decl "nat" convergence_sequences nil)
    (sequence type-eq-decl nil sequences 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)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (extract_incr3 formula-decl nil sequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (accumulation const-decl "bool" convergence_sequences nil))
   nil))
(cauchy_accumulation 0
  (cauchy_accumulation-1 nil 3253549181
   (""
    (grind :defs nil :rewrites ("cauchy" "accumulation" "convergence")
     :if-match nil)
    (("" (inst -4 "epsilon!1/2")
      (("" (skolem!)
        (("" (inst -5 "epsilon!1/2" "n!1")
          (("" (skosimp)
            (("" (inst 1 "i!1")
              (("" (skosimp)
                (("" (inst -4 "i!1" "i!2")
                  (("" (assert)
                    (("" (lemma "triangle2")
                      (("" (assert)
                        ((""
                          (inst -1 "epsilon!1/2" "epsilon!1/2"
                           "u!1(i!2)" "u!1(i!1)" "a!1")
                          (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (triangle2 formula-decl nil abs_lems "reals/")
    (sequence type-eq-decl nil sequences 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" convergence_sequences nil)
    (accumulation const-decl "bool" convergence_sequences nil)
    (cauchy const-decl "bool" convergence_sequences nil))
   nil))
(cauchy_subsequence 0
  (cauchy_subsequence-1 nil 3253549181
   ("" (skosimp)
    (("" (rewrite "cauchy_accumulation" 1)
      (("" (rewrite "accumulation_subsequence")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((cauchy_accumulation formula-decl nil convergence_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sequence type-eq-decl nil sequences nil)
    (accumulation_subsequence formula-decl nil convergence_sequences
     nil))
   nil))
(increasing_bounded_convergence 0
  (increasing_bounded_convergence-1 nil 3253549181
   ("" (skosimp)
    (("" (assert)
      ((""
        (grind :defs nil :if-match nil :rewrites
         ("increasing?" "convergence"))
        (("" (use "supfun_is_sup[nat]")
          (("" (skolem!)
            (("" (inst 1 "x!1")
              (("" (skosimp)
                (("" (inst -4 "x!1" "i!1")
                  (("" (assert)
                    (("" (use "supfun_is_bound" ("x" "i!1"))
                      (("" (assert)
                        (("" (expand "abs")
                          (("" (lift-if) (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers 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)
    (supfun_is_sup formula-decl nil real_fun_supinf nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (sequence type-eq-decl nil sequences nil)
    (supfun_is_bound formula-decl nil real_fun_supinf nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" convergence_sequences nil)
    (increasing? const-decl "bool" real_fun_preds "reals/"))
   nil))
(decreasing_bounded_convergence 0
  (decreasing_bounded_convergence-1 nil 3253549181
   ("" (skosimp)
    (("" (assert)
      ((""
        (grind :defs nil :if-match nil :rewrites
         ("decreasing?" "convergence"))
        (("" (use "inffun_is_inf[nat]")
          (("" (skolem!)
            (("" (inst 1 "x!1")
              (("" (skosimp)
                (("" (inst -4 "x!1" "i!1")
                  (("" (assert)
                    (("" (use "inffun_is_bound" ("x" "i!1"))
                      (("" (assert)
                        (("" (expand "abs") (("" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers 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)
    (inffun_is_inf formula-decl nil real_fun_supinf nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (sequence type-eq-decl nil sequences nil)
    (inffun_is_bound formula-decl nil real_fun_supinf nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" convergence_sequences nil)
    (decreasing? const-decl "bool" real_fun_preds "reals/"))
   nil))
(bolzano_weierstrass1 0
  (bolzano_weierstrass1-1 nil 3253549181
   ("" (skolem!)
    (("" (use "monotone_subsequence")
      (("" (skosimp)
        (("" (use* "bounded_above_subseq" "bounded_below_subseq")
          (("" (assert)
            (("" (expand "subseq")
              (("" (skolem!)
                ((""
                  (auto-rewrite "supfun_is_sup2[nat]"
                                "inffun_is_inf2[nat]"
                                "supfun_is_bound[nat]"
                                "inffun_is_bound[nat]"
                                "accumulation_subsequence")
                  (("" (ground)
                    (("1"
                      (forward-chain "increasing_bounded_convergence")
                      (("1" (inst? +)
                        (("1" (ground)
                          (("1" (inst - "0")
                            (("1" (use "supfun_is_bound" ("g" "s!1"))
                              (("1"
                                (use "inffun_is_bound" ("h" "w!1"))
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (skolem!)
                            (("2" (inst?)
                              (("2"
                                (replace*)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("3" (inst?) (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2"
                      (forward-chain "decreasing_bounded_convergence")
                      (("2" (inst? +)
                        (("2" (ground)
                          (("1" (skolem!)
                            (("1" (inst?)
                              (("1"
                                (replace -5)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (inst - "0")
                            (("2" (use "inffun_is_bound" ("h" "s!1"))
                              (("2"
                                (use "supfun_is_bound" ("g" "w!1"))
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("3" (inst?) (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monotone_subsequence formula-decl nil monotone_subsequence nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences 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)
    (bounded_above_subseq formula-decl nil sequence_props nil)
    (bounded_below_subseq formula-decl nil sequence_props nil)
    (subseq const-decl "bool" sequence_props nil)
    (decreasing_bounded_convergence formula-decl nil
     convergence_sequences nil)
    (inffun_is_inf2 formula-decl nil real_fun_supinf nil)
    (inf const-decl "real" real_fun_supinf nil)
    (increasing_bounded_convergence formula-decl nil
     convergence_sequences nil)
    (supfun_is_sup2 formula-decl nil real_fun_supinf nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (supfun_is_bound formula-decl nil real_fun_supinf nil)
    (extraction type-eq-decl nil sequence_props nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (inffun_is_bound formula-decl nil real_fun_supinf nil)
    (sup const-decl "real" real_fun_supinf nil)
    (accumulation_subsequence formula-decl nil convergence_sequences
     nil))
   nil))
(bolzano_weierstrass2 0
  (bolzano_weierstrass2-1 nil 3253549181
   ("" (skolem!)
    (("" (use "bolzano_weierstrass1")
      (("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((bolzano_weierstrass1 formula-decl nil convergence_sequences nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(bolzano_weierstrass3 0
  (bolzano_weierstrass3-1 nil 3253549181
   ("" (skosimp)
    (("" (use "bolzano_weierstrass1")
      (("" (skosimp)
        (("" (rewrite "accumulation_subsequence")
          (("" (skosimp)
            (("" (inst?)
              (("" (assert)
                (("" (expand "convergent?") (("" (inst?) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bolzano_weierstrass1 formula-decl nil convergence_sequences nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences 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)
    (accumulation_subsequence formula-decl nil convergence_sequences
     nil)
    (convergent? const-decl "bool" convergence_sequences nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(bolzano_weierstrass4 0
  (bolzano_weierstrass4-1 nil 3253549181
   ("" (skosimp)
    (("" (case "bounded_above?(u!1) AND bounded_below?(u!1)")
      (("1" (ground)
        (("1" (case "a!1 <= inf(u!1) AND sup(u!1) <= b!1")
          (("1" (ground)
            (("1" (use "bolzano_weierstrass1")
              (("1" (skosimp)
                (("1" (inst + "a!2") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (ground)
            (("1" (rewrite "inffun_is_inf2[nat]")
              (("1" (skolem!)
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (rewrite "supfun_is_sup2[nat]")
              (("2" (skolem!)
                (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (delete 2)
        (("2" (grind :if-match nil)
          (("1" (inst + "a!1")
            (("1" (skolem!)
              (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (inst + "b!1")
            (("2" (skolem!)
              (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bounded_below? const-decl "bool" real_fun_preds "reals/")
    (sequence type-eq-decl nil sequences nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (sup const-decl "real" real_fun_supinf nil)
    (inf const-decl "real" real_fun_supinf nil)
    (<= const-decl "bool" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bolzano_weierstrass1 formula-decl nil convergence_sequences nil)
    (supfun_is_sup2 formula-decl nil real_fun_supinf nil)
    (inffun_is_inf2 formula-decl nil real_fun_supinf nil))
   nil))
(prefix_bounded1 0
  (prefix_bounded1-1 nil 3253549181
   ("" (skolem 1 (_ "u!1"))
    (("" (induct "n")
      (("1" (inst 1 "u!1(0)")
        (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)
       ("2" (skosimp*)
        (("2" (inst 1 "max(a!1, u!1(j!1+1))")
          (("2" (skosimp) (("2" (inst?) (("2" (assert) nil nil)) nil))
            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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (sequence type-eq-decl nil sequences nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
(prefix_bounded2 0
  (prefix_bounded2-1 nil 3253549181
   ("" (skolem 1 (_ "u!1"))
    (("" (induct "n")
      (("1" (inst 1 "u!1(0)")
        (("1" (skosimp) (("1" (assert) nil nil)) nil)) nil)
       ("2" (skosimp*)
        (("2" (inst 1 "min(a!1, u!1(j!1+1))")
          (("2" (skosimp)
            (("2" (inst -1 "i!1") (("2" (assert) nil nil)) nil)) 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (sequence type-eq-decl nil sequences nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil))
(cauchy_bounded 0
  (cauchy_bounded-1 nil 3253549181
   ("" (skosimp)
    (("" (expand "cauchy")
      (("" (inst - "1")
        (("" (skolem!)
          (("" (inst - "n!1" _)
            (("" (auto-rewrite "bounded_above?" "bounded_below?" "abs")
              (("" (ground)
                (("1" (use "prefix_bounded1" ("n" "n!1"))
                  (("1" (skolem!)
                    (("1" (inst + "a!1 + 1")
                      (("1" (skolem!)
                        (("1" (inst-cp - "n!1")
                          (("1" (inst - "x!1")
                            (("1" (inst - "x!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (use "prefix_bounded2" ("n" "n!1"))
                  (("2" (skolem!)
                    (("2" (inst + "a!1 - 1")
                      (("2" (skolem!)
                        (("2" (inst-cp - "n!1")
                          (("2" (inst - "x!1")
                            (("2" (inst - "x!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (cauchy const-decl "bool" convergence_sequences nil)
    (prefix_bounded2 formula-decl nil convergence_sequences nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (prefix_bounded1 formula-decl nil convergence_sequences nil)
    (sequence type-eq-decl nil sequences nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(convergence_cauchy1 0
  (convergence_cauchy1-1 nil 3253549181
   (""
    (grind :defs nil :rewrites ("convergent?" "convergence" "cauchy")
     :if-match nil)
    (("" (delete -1 -2 -3)
      (("" (inst -1 "epsilon!1/2")
        (("" (skolem!)
          (("" (inst? 1)
            (("" (skosimp)
              (("" (inst-cp -1 "i!1")
                (("" (inst -1 "j!1")
                  (("" (assert)
                    (("" (rewrite "abs_diff_commute" -1)
                      (("" (rewrite "abs_diff_commute" -2)
                        (("" (lemma "triangle2")
                          ((""
                            (inst -1 "epsilon!1/2" "epsilon!1/2"
                             "u!1(j!1)" "l!1" "u!1(i!1)")
                            (("" (assert)
                              ((""
                                (rewrite "abs_diff_commute" +)
                                (("" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sequence type-eq-decl nil sequences nil)
    (abs_diff_commute formula-decl nil abs_lems "reals/")
    (triangle2 formula-decl nil abs_lems "reals/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (>= 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)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cauchy const-decl "bool" convergence_sequences nil)
    (convergent? const-decl "bool" convergence_sequences nil)
    (convergence const-decl "bool" convergence_sequences nil))
   nil))
(convergence_cauchy2 0
  (convergence_cauchy2-1 nil 3253549181
   ("" (skosimp)
    (("" (use "bolzano_weierstrass2")
      (("1" (skolem!)
        (("1" (expand "convergent?")
          (("1" (inst?) (("1" (rewrite "cauchy_accumulation") nil nil))
            nil))
          nil))
        nil)
       ("2" (rewrite "cauchy_bounded") nil nil))
      nil))
    nil)
   ((bolzano_weierstrass2 formula-decl nil convergence_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bounded_above? const-decl "bool" real_fun_preds "reals/")
    (sequence type-eq-decl nil sequences nil)
    (u!1 skolem-const-decl "sequence[real]" convergence_sequences nil)
    (bounded_below? const-decl "bool" real_fun_preds "reals/")
    (convergent? const-decl "bool" convergence_sequences nil)
    (cauchy_accumulation formula-decl nil convergence_sequences nil)
    (cauchy_bounded formula-decl nil convergence_sequences nil))
   nil))
(convergence_cauchy 0
  (convergence_cauchy-1 nil 3253549181
   ("" (skolem!)
    (("" (prop)
      (("1" (rewrite "convergence_cauchy1") nil nil)
       ("2" (rewrite "convergence_cauchy2") nil nil))
      nil))
    nil)
   ((sequence type-eq-decl nil sequences 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)
    (convergence_cauchy1 formula-decl nil convergence_sequences nil)
    (convergence_cauchy2 formula-decl nil convergence_sequences nil))
   nil)))

quality95%

¤ 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.0.54Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

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.