Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: limit_vect.prf Sprache: Lisp

Original von: PVS^©

(limit_vect
(cv_unique 0
  (cv_unique-1 nil 3459161645
   ("" (skeep)
    (("" (expand "convergence")
      (("" (rewrite "sub_eq_zero" :dir rl)
        (("" (rewrite "norm_eq_0" :dir rl)
          (("" (name "eps" "norm(l1 - l2)")
            (("" (inst -3 "eps/2")
              (("1" (inst -2 "eps/2")
                (("1" (skosimp*)
                  (("1" (inst -2 "a")
                    (("1" (inst -3 "a")
                      (("1" (assert)
                        (("1" (lemma "norm_triangle[m]")
                          (("1" (inst - "l1" "f(a)" "l2")
                            (("1" (lemma "norm_sym[m]")
                              (("1"
                                (inst - "l1" "f(a)")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence const-decl "bool" limit_vect nil)
    (norm_eq_0 formula-decl nil vectors "vectors/")
    (- const-decl "real" vectors "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     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)
    (eps skolem-const-decl "nnreal" limit_vect nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (norm_triangle formula-decl nil vectors "vectors/")
    (norm_sym formula-decl nil vectors "vectors/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (norm_zero formula-decl nil vectors "vectors/")
    (sub_eq_args formula-decl nil vectors "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sub_eq_zero formula-decl nil vectors "vectors/"))
   nil))
(cv_in_domain 0
  (cv_in_domain-1 nil 3459161910
   ("" (skeep)
    (("" (expand "convergence")
      (("" (rewrite "sub_eq_zero" :dir rl)
        (("" (rewrite "norm_eq_0" :dir rl)
          (("" (inst -1 "norm(l-f(a))")
            (("1" (skeep -1)
              (("1" (inst?)
                (("1" (assert)
                  (("1" (rewrite "norm_sym") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence const-decl "bool" limit_vect nil)
    (norm_eq_0 formula-decl nil vectors "vectors/")
    (- const-decl "real" vectors "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sub_eq_args formula-decl nil vectors "vectors/")
    (norm_zero formula-decl nil vectors "vectors/")
    (norm_sym formula-decl nil vectors "vectors/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors "vectors/")
    (l skolem-const-decl "Vector[m]" limit_vect nil)
    (f skolem-const-decl "[Vector[n] -> Vector[m]]" limit_vect nil)
    (a skolem-const-decl "Vector[n]" limit_vect nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (m formal-const-decl "posnat" limit_vect 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)
    (n formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (sub_eq_zero formula-decl nil vectors "vectors/"))
   nil))
(cv_sum 0
  (cv_sum-1 nil 3459162518
   ("" (skeep)
    (("" (expand "convergence")
      (("" (skosimp)
        (("" (inst - "epsilon!1/4")
          (("" (inst - "epsilon!1/4")
            (("" (skosimp*)
              (("" (inst 1 "min(delta!1, delta!2)")
                (("" (skosimp*)
                  (("" (inst?)
                    (("" (inst?)
                      (("" (assert)
                        (("" (lemma "norm_add_le[m]")
                          (("" (inst - "f1(v!1) - l1" "f2(v!1)-l2")
                            ((""
                              (case "f1(v!1) - l1 + (f2(v!1) - l2) = f1(v!1) + f2(v!1) - (l1 + l2)")
                              (("1" (assert) nil nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (decompose-equality)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence const-decl "bool" limit_vect nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (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)
    (norm_add_le formula-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (+ const-decl "real" vectors "vectors/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "real" vectors "vectors/")
    (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)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil))
   nil))
(cv_neg 0
  (cv_neg-1 nil 3459517119
   ("" (skeep)
    (("" (expand "convergence")
      (("" (skosimp)
        (("" (inst - "epsilon!1")
          (("" (skosimp)
            (("" (inst + "delta!1")
              (("" (skosimp)
                (("" (inst?)
                  (("" (assert)
                    (("" (rewrite "norm_sym")
                      (("" (case-replace "-f(v!1) -- l = l - f(v!1)")
                        (("" (hide-all-but 1)
                          (("" (decompose-equality)
                            (("" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence const-decl "bool" limit_vect 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)
    (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)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil)
    (norm_sym formula-decl nil vectors "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "real" vectors "vectors/")
    (- const-decl "Vector" vectors "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(cv_diff 0
  (cv_diff-2 nil 3459517161
   ("" (skeep)
    (("" (case-replace "f1 - f2 = f1 + (-f2)")
      (("1" (hide -1)
        (("1" (lemma "cv_sum")
          (("1" (inst -1 "a" "f1" "-f2" "l1" "-l2")
            (("1" (assert) (("1" (rewrite "cv_neg") nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (decompose-equality) 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)
    (< 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)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "real" vectors "vectors/")
    (+ const-decl "real" vectors "vectors/")
    (- const-decl "Vector" vectors "vectors/")
    (cv_sum formula-decl nil limit_vect nil)
    (add_neg_sub formula-decl nil vectors "vectors/")
    (cv_neg formula-decl nil limit_vect nil))
   nil)
  (cv_diff-1 nil 3459165514
   ("" (skeep)
    (("" (case-replace "f1 - f2 = f1 + (-f2)")
      (("1" (hide -1)
        (("1" (lemma "cv_sum")
          (("1" (inst -1 "a" "f1" "-f2" "l1" "-l2")
            (("1" (assert) (("1" (rewrite "cv_neg") nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (decompose-equality) nil nil))
      nil))
    nil)
   ((Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (- const-decl "real" vectors "vectors/")
    (+ const-decl "real" vectors "vectors/")
    (- const-decl "Vector" vectors "vectors/")
    (add_neg_sub formula-decl nil vectors "vectors/"))
   nil))
(cv_const 0
  (cv_const-1 nil 3459166889
   ("" (skeep)
    (("" (expand "convergence")
      (("" (skosimp)
        (("" (inst + "1") (("" (skosimp*) (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence const-decl "bool" limit_vect 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)
    (sub_eq_args formula-decl nil vectors "vectors/")
    (norm_zero formula-decl nil vectors "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(cv_scal 0
  (cv_scal-3 nil 3459517484
   ("" (skeep)
    (("" (case-replace "k = 0")
      (("1" (assert)
        (("1" (lemma "cv_const") (("1" (inst - "a" "zero") nil nil))
          nil))
        nil)
       ("2" (expand "convergence")
        (("2" (skosimp*)
          (("2" (inst - "epsilon!1/abs(k)")
            (("1" (skosimp*)
              (("1" (inst + "delta!1")
                (("1" (skosimp*)
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (cross-mult -1)
                        (("1" (lemma "norm_scal[m]")
                          (("1" (inst - "k" "f(v!1)-l")
                            (("1" (rewrite "scal_sub_right")
                              (("1"
                                (expand "*" 2 1)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 3)
              (("2" (case "epsilon!1 / abs(k) > 0")
                (("1" (assert) nil nil)
                 ("2" (hide 2)
                  (("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
                  nil)
                 ("3" (flatten)
                  (("3" (lemma "abs_eq_0")
                    (("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil)
             ("3" (assert) nil nil))
            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)
    (cv_const formula-decl nil limit_vect nil)
    (zero const-decl "Vector" vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" limit_vect 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)
    (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)
    (scal_0 formula-decl nil vectors "vectors/")
    (abs_eq_0 formula-decl nil abs_lems "reals/")
    (abs_nat formula-decl nil abs_lems "reals/")
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (norm_scal formula-decl nil vectors "vectors/")
    (scal_sub_right formula-decl nil vectors "vectors/")
    (* const-decl "Vector" vectors "vectors/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (- const-decl "real" vectors "vectors/")
    (norm const-decl "nnreal" vectors "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (epsilon!1 skolem-const-decl "posreal" limit_vect nil)
    (/= const-decl "boolean" notequal nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (k skolem-const-decl "real" limit_vect 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (convergence const-decl "bool" limit_vect nil))
   nil)
  (cv_scal-2 nil 3459517322
   (";;; Proof cv_scal-1 for formula limit_vect2_real.cv_scal"
    (skosimp)
    ((";;; Proof cv_scal-1 for formula limit_vect2_real.cv_scal"
      (rewrite "scal_function")
      ((";;; Proof cv_scal-1 for formula limit_vect2_real.cv_scal"
        (rewrite "cv_prod")
        ((";;; Proof cv_scal-1 for formula limit_vect2_real.cv_scal"
          (hide 2)
          ((";;; Proof cv_scal-1 for formula limit_vect2_real.cv_scal"
            (rewrite "cv_const") nil))))))))
    ";;; developed with shostak decision procedures")
   nil nil)
  (cv_scal-1 nil 3459517175 ("" (postpone) nil nil) nil shostak))
(lim_TCC1 0
  (lim_TCC1-2 nil 3459518834
   ("" (skosimp*)
    (("" (expand "nonempty?")
      (("" (expand "empty?")
        (("" (expand "member")
          (("" (typepred "x0!1")
            (("" (expand "convergent?")
              (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets 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)
    (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)
    (< 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)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil)
    (convergent? const-decl "bool" limit_vect nil)
    (empty? const-decl "bool" sets nil))
   nil)
  (lim_TCC1-1 nil 3459518767 ("" (subtype-tcc) nil nil) nil nil))
(lim_fun_lemma 0
  (lim_fun_lemma-1 nil 3459518875
   ("" (skolem!)
    (("" (name-replace "ll" "lim(f!1, x0!1)" :hide? nil)
      (("" (expand "lim" -)
        (("" (typepred "choose(LAMBDA l: convergence(f!1, x0!1, l))")
          (("1" (assert) nil nil)
           ("2" (expand "nonempty?")
            (("2" (expand "empty?")
              (("2" (expand "member")
                (("2" (inst?) (("2" (assert) nil nil)) 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)
    (< 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)
    (m formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (convergent? const-decl "bool" limit_vect nil)
    (lim const-decl "Vector[m]" limit_vect nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (convergence const-decl "bool" limit_vect nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil))
   nil))
(lim_fun_def 0
  (lim_fun_def-1 nil 3299406886
   ("" (skolem!)
    (("" (use "lim_fun_lemma")
      (("" (ground)
        (("" (use "cv_unique" ("l2" "lim(f!1, x0!1)"))
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((lim_fun_lemma formula-decl nil limit_vect nil)
    (convergent? const-decl "bool" limit_vect nil)
    (m formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" limit_vect 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)
    (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)
    (cv_unique formula-decl nil limit_vect nil)
    (lim const-decl "Vector[m]" limit_vect nil))
   nil))
(convergence_equiv 0
  (convergence_equiv-1 nil 3299406886
   ("" (skolem!)
    (("" (prop)
      (("1" (expand "convergent?") (("1" (inst?) nil nil)) nil)
       ("2" (rewrite "lim_fun_def")
        (("2" (expand "convergent?") (("2" (inst?) nil nil)) nil)) nil)
       ("3" (rewrite "lim_fun_def") nil nil))
      nil))
    nil)
   ((Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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)
    (convergent? const-decl "bool" limit_vect nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (lim_fun_def formula-decl nil limit_vect nil))
   nil))
(convergent_in_domain 0
  (convergent_in_domain-1 nil 3299406886
   ("" (grind :exclude "convergence")
    (("" (forward-chain "cv_in_domain") (("" (assert) nil nil)) nil))
    nil)
   ((cv_in_domain formula-decl nil limit_vect nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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)
    (convergent? const-decl "bool" limit_vect nil))
   nil))
(lim_in_domain 0
  (lim_in_domain-1 nil 3299406886
   ("" (skosimp)
    (("" (rewrite "lim_fun_def")
      (("" (rewrite "convergent_in_domain") nil nil)) nil))
    nil)
   ((lim_fun_def formula-decl nil limit_vect nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "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)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil)
    (convergent? const-decl "bool" limit_vect nil)
    (convergent_in_domain formula-decl nil limit_vect nil))
   nil))
(sum_fun_convergent 0
  (sum_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (inst 1 "l!1 + l!2") (("" (rewrite "cv_sum") nil nil)) nil))
      nil))
    nil)
   ((cv_sum formula-decl nil limit_vect nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (+ const-decl "real" vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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)
    (convergent? const-decl "bool" limit_vect nil))
   nil))
(neg_fun_convergent 0
  (neg_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (inst + "-l!1")
        (("" (expand "convergence")
          (("" (skosimp*)
            (("" (inst - "epsilon!1")
              (("" (skosimp*)
                (("" (inst + "delta!1")
                  (("" (skosimp*)
                    (("" (inst - "v!1")
                      (("" (assert)
                        (("" (expand "norm")
                          (("" (expand "sqv")
                            (("" (assert) (("" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence const-decl "bool" limit_vect nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (norm const-decl "nnreal" vectors "vectors/")
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "real" vectors "vectors/")
    (- const-decl "real" vectors "vectors/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_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_minus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sqv const-decl "nnreal" vectors "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "Vector" vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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)
    (convergent? const-decl "bool" limit_vect nil))
   nil))
(diff_fun_convergent 0
  (diff_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (inst 1 "l!1 - l!2") (("" (rewrite "cv_diff") nil nil))
        nil))
      nil))
    nil)
   ((cv_diff formula-decl nil limit_vect nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (- const-decl "real" vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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)
    (convergent? const-decl "bool" limit_vect nil))
   nil))
(const_fun_convergent 0
  (const_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skolem!)
      (("" (inst?)
        (("" (rewrite "const_fun") (("" (rewrite "cv_const") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((const_fun const-decl "Vector[m]" limit_vect nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (cv_const formula-decl nil limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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)
    (convergent? const-decl "bool" limit_vect nil))
   nil))
(scal_fun_convergent 0
  (scal_fun_convergent-1 nil 3459522634
   ("" (skosimp*)
    (("" (expand "convergent?")
      (("" (skosimp*)
        (("" (inst + "k!1*l!1")
          (("" (lemma "cv_scal")
            (("" (inst?) (("" (prop) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" limit_vect nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "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)
    (m formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (* const-decl "Vector" vectors "vectors/")
    (n formal-const-decl "posnat" limit_vect nil)
    (cv_scal formula-decl nil limit_vect nil))
   shostak))
(lim_sum_fun_TCC1 0
  (lim_sum_fun_TCC1-1 nil 3299406886
   ("" (skosimp) (("" (rewrite "sum_fun_convergent") nil nil)) nil)
   ((sum_fun_convergent formula-decl nil limit_vect nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "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)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil))
   nil))
(lim_sum_fun 0
  (lim_sum_fun-1 nil 3299406886
   (""
    (auto-rewrite "lim_fun_lemma" "lim_fun_def" "sum_fun_convergent"
                  ("cv_sum"))
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((lim_fun_lemma formula-decl nil limit_vect nil)
    (cv_sum formula-decl nil limit_vect nil)
    (lim_fun_def formula-decl nil limit_vect nil))
   nil))
(lim_neg_fun_TCC1 0
  (lim_neg_fun_TCC1-1 nil 3299406886
   ("" (lemma "neg_fun_convergent") (("" (propax) nil nil)) nil)
   ((neg_fun_convergent formula-decl nil limit_vect nil)) nil))
(lim_neg_fun 0
  (lim_neg_fun-1 nil 3299406886
   (""
    (auto-rewrite "lim_fun_lemma" "lim_fun_def" "neg_fun_convergent"
                  "cv_neg")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((lim_fun_lemma formula-decl nil limit_vect nil)
    (cv_neg formula-decl nil limit_vect nil)
    (lim_fun_def formula-decl nil limit_vect nil))
   nil))
(lim_diff_fun_TCC1 0
  (lim_diff_fun_TCC1-1 nil 3299406886
   ("" (skosimp) (("" (rewrite "diff_fun_convergent") nil nil)) nil)
   ((diff_fun_convergent formula-decl nil limit_vect nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "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)
    (n formal-const-decl "posnat" limit_vect nil)
    (Index type-eq-decl nil vectors "vectors/")
    (Vector type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect nil))
   nil))
(lim_diff_fun 0
  (lim_diff_fun-1 nil 3299406886
   (""
    (auto-rewrite "lim_fun_lemma" "lim_fun_def" "diff_fun_convergent"
                  ("cv_diff"))
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((lim_fun_lemma formula-decl nil limit_vect nil)
    (cv_diff formula-decl nil limit_vect nil)
    (lim_fun_def formula-decl nil limit_vect nil))
   nil))
(lim_const_fun_TCC1 0
  (lim_const_fun_TCC1-1 nil 3459521232
   ("" (skosimp*)
    (("" (expand "convergent?")
      (("" (inst + "l!1")
        (("" (lemma "cv_const")
          (("" (inst - "a!1" "l!1")
            (("" (expand "const_fun") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" limit_vect nil)
    (cv_const formula-decl nil limit_vect nil)
    (const_fun const-decl "Vector[m]" limit_vect nil)
    (n formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (m formal-const-decl "posnat" limit_vect 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)
    (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))
(lim_const_fun 0
  (lim_const_fun-1 nil 3459528905
   ("" (skosimp*)
    (("" (lemma "lim_fun_def")
      (("" (inst - "const_fun(l!1)" "l!1" "a!1")
        (("" (replace -1)
          (("" (expand "const_fun")
            (("" (lemma "cv_const") (("" (inst - "a!1" "l!1") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lim_fun_def formula-decl nil limit_vect nil)
    (cv_const formula-decl nil limit_vect nil)
    (convergent? const-decl "bool" limit_vect nil)
    (const_fun const-decl "Vector[m]" limit_vect nil)
    (m formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" limit_vect 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)
    (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))
   shostak))
(lim_scal_fun_TCC1 0
  (lim_scal_fun_TCC1-1 nil 3459521232
   ("" (skosimp*)
    (("" (lemma "scal_fun_convergent")
      (("" (inst - "a!1" "f!1" "k!1") (("" (prop) nil nil)) nil)) nil))
    nil)
   ((scal_fun_convergent formula-decl nil limit_vect nil)
    (m formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" limit_vect 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)
    (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))
(lim_scal_fun 0
  (lim_scal_fun-1 nil 3459529190
   ("" (skosimp*)
    (("" (lemma "scal_fun_convergent")
      (("" (inst - "a!1" "f!1" "k!1")
        (("" (prop)
          (("" (lemma "lim_fun_def")
            ((""
              (inst - "(LAMBDA (v): k!1 * f!1(v))" "k!1 * lim(f!1,a!1)"
               "a!1")
              (("" (replace -1)
                (("" (lemma "lim_fun_def")
                  (("" (inst - "f!1" "lim(f!1,a!1)" "a!1")
                    (("" (prop)
                      (("" (lemma "cv_scal")
                        (("" (inst - "a!1" "f!1" "k!1" "lim(f!1,a!1)")
                          (("" (prop) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((scal_fun_convergent formula-decl nil limit_vect nil)
    (* const-decl "Vector" vectors "vectors/")
    (convergent? const-decl "bool" limit_vect nil)
    (lim const-decl "Vector[m]" limit_vect nil)
    (cv_scal formula-decl nil limit_vect nil)
    (lim_fun_def formula-decl nil limit_vect nil)
    (m formal-const-decl "posnat" limit_vect nil)
    (Vector type-eq-decl nil vectors "vectors/")
    (Index type-eq-decl nil vectors "vectors/")
    (n formal-const-decl "posnat" limit_vect 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)
    (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))
   shostak)))

¤ Dauer der Verarbeitung: 0.32 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.