Quelle limit_vect2_real.prf Sprache: Lisp

(limit_vect2_real
(cv_unique 0
  (cv_unique-1 nil 3299406886
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    (("" (rewrite "abs_diff_0")
      (("" (name "eps" "abs(l1!1 - l2!1)")
        (("" (replace -1)
          (("" (inst -4 "eps/2")
            (("1" (inst -5 "eps/2")
              (("1" (assert)
                (("1" (skosimp*)
                  (("1"
                    (case " EXISTS (x: Vect2): a!1 /= x AND norm(x - a!1) < delta!1 AND norm(x - a!1) < delta!2")
                    (("1" (skosimp*)
                      (("1" (inst?)
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (case "0 < norm(x!1 - a!1)")
                              (("1"
                                (assert)
                                (("1"
                                  (lemma "triangle2")
                                  (("1"
                                    (inst
                                     -
                                     "eps/2"
                                     "eps/2"
                                     "l1!1"
                                     "f!1(x!1)"
                                     "l2!1")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma "norm_eq_0")
                                (("2"
                                  (inst?)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (replace -1 * lr)
                                      (("2"
                                        (assert)
                                        (("2"
                                          (rewrite "sub_eq_zero")
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide -4 -5)
                      (("2" (name "DEL" "min(delta!1,delta!2)")
                        (("2" (inst + "(a!1`x + DEL/2, a!1`y)")
                          (("2" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((abs_diff_0 formula-decl nil abs_lems "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sqrt_square formula-decl nil sqrt "reals/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (posreal_min application-judgement
     "{z: posreal | z <= x AND z <= y}" real_defs nil)
    (triangle2 formula-decl nil abs_lems "reals/")
    (sub_eq_zero formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (norm_eq_0 formula-decl nil vectors_2D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (< const-decl "bool" reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (posreal nonempty-type-eq-decl nil real_types nil)
    (eps skolem-const-decl
     "{n: nonneg_real | n >= l1!1 - l2!1 AND n >= -(l1!1 - l2!1)}"
     limit_vect2_real nil)
    (l2!1 skolem-const-decl "real" limit_vect2_real nil)
    (l1!1 skolem-const-decl "real" limit_vect2_real 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)
    (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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (>= const-decl "bool" reals 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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" limit_vect2_real nil))
   nil))
(cv_in_domain 0
  (cv_in_domain-1 nil 3299406886
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    (("" (rewrite "abs_diff_0")
      (("" (inst - "abs(l!1 - f!1(x!1))")
        (("1" (skosimp*)
          (("1" (inst?)
            (("1" (assert)
              (("1" (rewrite "abs_diff_commute" -)
                (("1" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (abs_diff_0 formula-decl nil abs_lems "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sub_eq_args formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (abs_diff_commute formula-decl nil abs_lems "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" limit_vect2_real nil))
   nil))
(cv_sum 0
  (cv_sum-1 nil 3299406886
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    (("" (inst - "epsilon!1/2")
      (("" (inst - "epsilon!1/2")
        (("" (skosimp*)
          (("" (inst 1 "min(delta!1, delta!2)")
            (("" (skosimp*)
              (("" (inst?)
                (("" (inst?)
                  (("" (assert)
                    ((""
                      (lemma "triangle"
                       ("x" "f1!1(x!1) - l1!1" "y" "f2!1(x!1) - l2!1"))
                      (("" (assert) 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)
    (triangle formula-decl nil real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (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)
    (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_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (convergence const-decl "bool" limit_vect2_real nil))
   nil))
(cv_neg 0
  (cv_neg-1 nil 3299406886
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    (("" (inst - "epsilon!1")
      (("" (skolem!)
        (("" (inst + "delta!1")
          (("" (skosimp)
            (("" (inst?)
              (("" (assert)
                (("" (expand "-")
                  (("" (lemma "abs_neg")
                    (("" (inst - "f!1(x!1) - l!1")
                      (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (- const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (abs_neg formula-decl nil abs_lems "reals/")
    (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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergence const-decl "bool" limit_vect2_real nil))
   nil))
(cv_diff 0
  (cv_diff-1 nil 3299406886
   ("" (skosimp*)
    (("" (rewrite "diff_function")
      (("" (lemma "cv_sum")
        (("" (inst?)
          (("" (inst - "(-f2!1)" "-l2!1")
            (("" (assert)
              (("" (hide 2)
                (("" (lemma "cv_neg")
                  (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((diff_function formula-decl nil vect2_fun_ops "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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_minus_real_is_real application-judgement "real" reals nil)
    (cv_neg formula-decl nil limit_vect2_real nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (cv_sum formula-decl nil limit_vect2_real nil))
   nil))
(cv_prod 0
  (cv_prod-2 nil 3442332189
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    ((""
      (lemma "prod_epsilon" ("y1" "l1!1" "y2" "l2!1" "e" "epsilon!1"))
      (("" (skosimp*)
        (("" (inst - "e1!1")
          (("" (inst - "e2!1")
            (("" (skosimp*)
              (("" (inst 1 "min(delta!1, delta!2)")
                (("" (skosimp*)
                  (("" (inst?)
                    (("" (inst?)
                      (("" (assert)
                        (("" (lemma "prod_bound")
                          ((""
                            (inst -1 "e1!1" "e2!1" "f1!1(x!1)"
                             "f2!1(x!1)" "l1!1" "l2!1")
                            (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((prod_epsilon formula-decl nil epsilon_lemmas "analysis/")
    (prod_bound formula-decl nil epsilon_lemmas "analysis/")
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (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)
    (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_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (convergence const-decl "bool" limit_vect2_real nil))
   nil)
  (cv_prod-1 nil 3299406886
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    ((""
      (lemma "prod_epsilon"
       ("y1" "l1!1" "y2" "l2!1" "epsilon" "epsilon!1"))
      (("" (skosimp*)
        (("" (inst - "e1!1")
          (("" (inst - "e2!1")
            (("" (skosimp*)
              (("" (inst 1 "min(delta!1, delta!2)")
                (("" (skosimp*)
                  (("" (inst?)
                    (("" (inst?)
                      (("" (assert) (("" (postpone) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(cv_const 0
  (cv_const-1 nil 3299406886
   ("" (expand "convergence")
    (("" (skosimp*)
      (("" (expand "const_fun") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((abs_0 formula-decl nil abs_lems "reals/")
    (const_fun const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (convergence const-decl "bool" limit_vect2_real nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(cv_scal 0
  (cv_scal-1 nil 3299406886
   ("" (skosimp)
    (("" (rewrite "scal_function")
      (("" (rewrite "cv_prod")
        (("" (hide 2) (("" (rewrite "cv_const") nil nil)) nil)) nil))
      nil))
    nil)
   ((scal_function formula-decl nil vect2_fun_ops "vectors/")
    (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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (cv_const formula-decl nil limit_vect2_real nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (const_fun const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (cv_prod formula-decl nil limit_vect2_real nil))
   nil))
(cv_inv 0
  (cv_inv-2 nil 3442332397
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    (("" (lemma "inv_epsilon" ("y1" "l!1" "e" "epsilon!1"))
      (("" (assert)
        (("" (skosimp)
          (("" (inst? -)
            (("" (skosimp*)
              (("" (inst + "delta!1")
                (("" (skosimp*)
                  (("" (inst?)
                    (("" (assert)
                      ((""
                        (lemma "inv_bound"
                         ("e1" "e1!1" "x1" "g!1(x!1)" "y1" "l!1"))
                        (("" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((inv_epsilon formula-decl nil epsilon_lemmas "analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (inv_bound formula-decl nil epsilon_lemmas "analysis/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     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)
    (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)
    (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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (/ const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (/= const-decl "boolean" notequal nil)
    (convergence const-decl "bool" limit_vect2_real nil))
   nil)
  (cv_inv-1 nil 3299406886
   ("" (expand "convergence")
    (("" (grind :defs nil :rewrites "convergence_inv[T]") nil nil))
    nil)
   nil nil))
(cv_div 0
  (cv_div-1 nil 3299406886
   ("" (skosimp*)
    (("" (rewrite "div_function")
      (("" (assert)
        (("" (use "cv_prod" ("l2" "1/l2!1"))
          (("" (assert) (("" (rewrite "cv_inv") nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((div_function formula-decl nil vect2_fun_ops "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cv_prod formula-decl nil limit_vect2_real nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (/ const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (cv_inv formula-decl nil limit_vect2_real nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
(lim_TCC1 0
  (lim_TCC1-1 nil 3445162370
   ("" (skeep)
    (("" (typepred "x0")
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (expand "convergent?")
            (("" (skosimp*)
              (("" (expand "member") (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" limit_vect2_real 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   nil))
(lim_fun_lemma 0
  (lim_fun_lemma-1 nil 3299406886
   ("" (skolem!)
    (("" (name-replace "ll" "lim(f!1, x0!1)" :hide? nil)
      (("" (expand "lim" -)
        (("" (typepred "x0!1")
          (("" (expand "convergent?")
            (("" (skosimp*) (("" (assert) nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (lim const-decl "real" limit_vect2_real nil)
    (NOT const-decl "[bool -> bool]" booleans 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_vect2_real nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (cv_unique formula-decl nil limit_vect2_real nil)
    (lim const-decl "real" limit_vect2_real 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)
   ((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_vect2_real nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (lim_fun_def formula-decl nil limit_vect2_real 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_vect2_real nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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_vect2_real 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_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (convergent_in_domain formula-decl nil limit_vect2_real 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)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (cv_sum formula-decl nil limit_vect2_real nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (convergent? const-decl "bool" limit_vect2_real nil))
   nil))
(neg_fun_convergent 0
  (neg_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (forward-chain "cv_neg") (("" (inst?) nil nil)) nil)) nil))
    nil)
   ((numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (cv_neg formula-decl nil limit_vect2_real nil)
    (convergent? const-decl "bool" limit_vect2_real 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)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (cv_diff formula-decl nil limit_vect2_real nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (convergent? const-decl "bool" limit_vect2_real nil))
   nil))
(prod_fun_convergent 0
  (prod_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (inst 1 "l!1 * l!2") (("" (rewrite "cv_prod") nil nil))
        nil))
      nil))
    nil)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (cv_prod formula-decl nil limit_vect2_real nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (convergent? const-decl "bool" limit_vect2_real nil))
   nil))
(const_fun_convergent 0
  (const_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skolem!)
      (("" (inst?) (("" (rewrite "cv_const") nil nil)) nil)) nil))
    nil)
   ((cv_const formula-decl nil limit_vect2_real nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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_vect2_real nil))
   nil))
(scal_fun_convergent 0
  (scal_fun_convergent-1 nil 3299406886
   ("" (expand "convergent?")
    (("" (skosimp*)
      (("" (inst 1 "b!1 * l!1") (("" (rewrite "cv_scal") nil nil))
        nil))
      nil))
    nil)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (cv_scal formula-decl nil limit_vect2_real nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (convergent? const-decl "bool" limit_vect2_real nil))
   nil))
(inv_fun_convergent 0
  (inv_fun_convergent-1 nil 3299406886
   ("" (skosimp)
    (("" (rewrite "lim_fun_def")
      (("" (expand "convergent?")
        (("" (skosimp)
          (("" (assert)
            (("" (inst 2 "1/l!1") (("" (rewrite "cv_inv") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lim_fun_def formula-decl nil limit_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cv_inv formula-decl nil limit_vect2_real nil))
   nil))
(div_fun_convergent 0
  (div_fun_convergent-1 nil 3299406886
   ("" (skosimp)
    (("" (rewrite "lim_fun_def")
      (("" (expand "convergent?")
        (("" (skosimp*)
          (("" (assert)
            (("" (inst 2 "l!1 / l!2") (("" (rewrite "cv_div") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lim_fun_def formula-decl nil limit_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cv_div formula-decl nil limit_vect2_real nil))
   nil))
(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_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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))
   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_vect2_real nil)
    (cv_sum formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (real_plus_real_is_real application-judgement "real" reals 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_vect2_real 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_vect2_real nil)
    (cv_neg formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (minus_real_is_real application-judgement "real" reals 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_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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))
   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_vect2_real nil)
    (cv_diff formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(lim_prod_fun_TCC1 0
  (lim_prod_fun_TCC1-1 nil 3299406886
   ("" (skosimp) (("" (rewrite "prod_fun_convergent") nil nil)) nil)
   ((prod_fun_convergent formula-decl nil limit_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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))
   nil))
(lim_prod_fun 0
  (lim_prod_fun-1 nil 3299406886
   (""
    (auto-rewrite "lim_fun_lemma" "lim_fun_def" "prod_fun_convergent"
                  ("cv_prod"))
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((lim_fun_lemma formula-decl nil limit_vect2_real nil)
    (cv_prod formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(lim_const_fun_TCC1 0
  (lim_const_fun_TCC1-1 nil 3299406886
   ("" (lemma "const_fun_convergent") (("" (propax) nil nil)) nil)
   ((const_fun_convergent formula-decl nil limit_vect2_real nil)) nil))
(lim_const_fun 0
  (lim_const_fun-1 nil 3299406886
   (""
    (auto-rewrite "lim_fun_lemma" "lim_fun_def" "const_fun_convergent"
                  ("cv_const"))
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((cv_const formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil))
   nil))
(lim_scal_fun_TCC1 0
  (lim_scal_fun_TCC1-1 nil 3299406886
   ("" (lemma "scal_fun_convergent") (("" (propax) nil nil)) nil)
   ((scal_fun_convergent formula-decl nil limit_vect2_real nil)) nil))
(lim_scal_fun 0
  (lim_scal_fun-1 nil 3299406886
   (""
    (auto-rewrite "lim_fun_lemma" "lim_fun_def" "scal_fun_convergent"
                  "cv_scal")
    (("" (skosimp) (("" (assert) nil nil)) nil)) nil)
   ((lim_fun_lemma formula-decl nil limit_vect2_real nil)
    (cv_scal formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(lim_inv_fun_TCC1 0
  (lim_inv_fun_TCC1-1 nil 3299406886
   ("" (skosimp) (("" (rewrite "inv_fun_convergent") nil nil)) nil)
   ((inv_fun_convergent formula-decl nil limit_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
(lim_inv_fun 0
  (lim_inv_fun-1 nil 3299406886
   ("" (skosimp)
    (("" (assert)
      (("" (delete 1)
        ((""
          (auto-rewrite "lim_fun_def" "lim_fun_lemma"
                        "inv_fun_convergent" ("cv_inv"))
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (lim_fun_lemma formula-decl nil limit_vect2_real nil)
    (cv_inv formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil))
   nil))
(lim_div_fun_TCC1 0
  (lim_div_fun_TCC1-1 nil 3299406886
   ("" (skosimp) (("" (rewrite "div_fun_convergent") nil nil)) nil)
   ((div_fun_convergent formula-decl nil limit_vect2_real nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil))
   nil))
(lim_div_fun 0
  (lim_div_fun-1 nil 3299406886
   ("" (skosimp)
    (("" (assert)
      (("" (delete 1)
        ((""
          (auto-rewrite "lim_fun_def" "lim_fun_lemma"
                        "div_fun_convergent" "cv_div")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (lim_fun_lemma formula-decl nil limit_vect2_real nil)
    (cv_div formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil))
   nil))
(convergence_order 0
  (convergence_order-1 nil 3442333462
   ("" (grind :exclude ("abs" "norm" "-") :if-match nil)
    (("" (case "l2!1 < l1!1")
      (("1" (case "l2!1 < l1!1")
        (("1" (name "eps" "(l1!1 - l2!1)/2")
          (("1" (assert)
            (("1" (inst - "eps")
              (("1" (inst - "eps")
                (("1" (skosimp*)
                  (("1" (inst?)
                    (("1" (inst?)
                      (("1" (inst?)
                        (("1" (assert) (("1" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (propax) nil nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((< const-decl "bool" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_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)
    (>= const-decl "bool" reals nil)
    (sub_eq_args formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (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" limit_vect2_real nil))
   shostak))
(convergence_lower_bound 0
  (convergence_lower_bound-1 nil 3442333554
   ("" (skosimp*)
    (("" (lemma "cv_const")
      (("" (inst - "b!1" "a!1")
        (("" (use "convergence_order" ("f2" "f!1"))
          (("" (assert)
            (("" (skosimp*)
              (("" (expand "const_fun")
                (("" (assert) (("" (inst?) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cv_const formula-decl nil limit_vect2_real nil)
    (convergence_order formula-decl nil limit_vect2_real nil)
    (const_fun const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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))
(convergence_upper_bound 0
  (convergence_upper_bound-1 nil 3442333686
   ("" (skosimp*)
    (("" (lemma "cv_const")
      (("" (inst - "b!1" "a!1")
        (("" (assert)
          (("" (use "convergence_order" ("f1" "f!1"))
            (("" (expand "const_fun") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cv_const formula-decl nil limit_vect2_real nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (const_fun const-decl "[Vect2 -> real]" vect2_fun_ops "vectors/")
    (convergence_order formula-decl nil limit_vect2_real nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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_le1 0
  (lim_le1-1 nil 3299406886
   ("" (skosimp)
    (("" (assert)
      (("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
        (("" (rewrite "lim_fun_def")
          (("" (use "convergence_upper_bound") (("" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (convergence_upper_bound formula-decl nil limit_vect2_real nil)
    (lim const-decl "real" limit_vect2_real nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(lim_ge1 0
  (lim_ge1-1 nil 3299406886
   ("" (skosimp)
    (("" (assert)
      (("" (name-replace "ll" "lim(f!1, a!1)" :hide? nil)
        (("" (rewrite "lim_fun_def")
          (("" (use "convergence_lower_bound" ("b" "b!1"))
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (convergence_lower_bound formula-decl nil limit_vect2_real nil)
    (lim const-decl "real" limit_vect2_real nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(lim_order1 0
  (lim_order1-1 nil 3299406886
   ("" (skosimp)
    (("" (assert)
      (("" (name-replace "ll1" "lim(f1!1, a!1)" :hide? nil)
        (("" (name-replace "ll2" "lim(f2!1, a!1)" :hide? nil)
          (("" (rewrite "lim_fun_def")
            (("" (rewrite "lim_fun_def")
              (("" (use "convergence_order" ("l1" "ll1" "l2" "ll2"))
                (("" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (convergence_order formula-decl nil limit_vect2_real nil)
    (lim_fun_def formula-decl nil limit_vect2_real nil)
    (lim const-decl "real" limit_vect2_real nil)
    (convergent? const-decl "bool" limit_vect2_real nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.