Quelle cont_vect2_vect2.prf Sprache: Lisp

(cont_vect2_vect2
(continuity_def 0
  (continuity_def-1 nil 3302273405
   ("" (skosimp*)
    (("" (expand "continuous_vv?")
      (("" (expand "convergence") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((continuous_vv? const-decl "bool" cont_vect2_vect2 nil)
    (convergence const-decl "bool" limit_vect2_vect2 nil))
   nil))
(continuity_def2 0
  (continuity_def2-1 nil 3302273405
   ("" (skosimp*)
    (("" (rewrite "continuity_def")
      (("" (rewrite "convergent_in_domain") (("" (assert) nil nil))
        nil))
      nil))
    nil)
   ((continuity_def formula-decl nil cont_vect2_vect2 nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (convergent_in_domain formula-decl nil limit_vect2_vect2 nil))
   nil))
(sum_continuous_vv 0
  (sum_continuous_vv-1 nil 3302273405
   (""
    (grind :defs nil :rewrites
     ("continuity_def2" "sum_fun_convergent"))
    nil nil)
   ((sum_fun_convergent formula-decl nil limit_vect2_vect2 nil)
    (continuity_def2 formula-decl nil cont_vect2_vect2 nil))
   nil))
(diff_continuous_vv 0
  (diff_continuous_vv-2 nil 3442334818
   (""
    (grind :defs nil :rewrites
     ("continuity_def2" "diff_fun_convergent"))
    nil nil)
   ((diff_fun_convergent formula-decl nil limit_vect2_vect2 nil)
    (continuity_def2 formula-decl nil cont_vect2_vect2 nil))
   nil)
  (diff_continuous_vv-1 nil 3302273405
   (""
    (grind :defs nil :rewrites
     ("continuity_def2" "diff_fun_convergent"))
    nil nil)
   nil nil))
(const_continuous_vv 0
  (const_continuous_vv-1 nil 3302273405
   (""
    (grind :defs nil :rewrites
     ("continuity_def2" "const_fun_convergent" "adherence_fullset"))
    nil nil)
   ((const_fun_convergent formula-decl nil limit_vect2_vect2 nil)
    (continuity_def2 formula-decl nil cont_vect2_vect2 nil))
   nil))
(identity_continuous_vv 0
  (identity_continuous_vv-1 nil 3445172211
   ("" (skeep)
    (("" (expand "continuous_vv?")
      (("" (expand "convergence")
        (("" (skosimp*)
          (("" (inst + "epsilon!1") (("" (skosimp*) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_vv? const-decl "bool" cont_vect2_vect2 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))
   shostak))
(neg_continuous_vv 0
  (neg_continuous_vv-1 nil 3302273405
   (""
    (grind :defs nil :rewrites
     ("continuity_def2" "neg_fun_convergent"))
    nil nil)
   ((neg_fun_convergent formula-decl nil limit_vect2_vect2 nil)
    (continuity_def2 formula-decl nil cont_vect2_vect2 nil))
   nil))
(sum_cont_vv_fun 0
  (sum_cont_vv_fun-1 nil 3393866517
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "continuous_vv?")
        (("" (skosimp*)
          (("" (inst?)
            (("" (inst?)
              (("" (lemma "sum_continuous_vv")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sum_continuous_vv formula-decl nil cont_vect2_vect2 nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 nil))
   shostak))
(diff_cont_vv_fun 0
  (diff_cont_vv_fun-1 nil 3393866553
   ("" (skosimp*)
    (("" (expand "continuous_vv?")
      (("" (skosimp*)
        (("" (inst?)
          (("" (inst?) (("" (rewrite "diff_continuous_vv") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_vv? const-decl "bool" cont_vect2_vect2 nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (diff_continuous_vv formula-decl nil cont_vect2_vect2 nil))
   shostak))
(const_cont_vv_fun 0
  (const_cont_vv_fun-1 nil 3393866606
   ("" (skosimp*)
    (("" (expand "continuous_vv?")
      (("" (skosimp*)
        (("" (lemma "const_continuous_vv") (("" (inst?) nil nil)) nil))
        nil))
      nil))
    nil)
   ((continuous_vv? const-decl "bool" cont_vect2_vect2 nil)
    (const_continuous_vv formula-decl nil cont_vect2_vect2 nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
   shostak))
(neg_cont_vv_fun 0
  (neg_cont_vv_fun-1 nil 3393866960
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "continuous_vv?")
        (("" (skosimp*)
          (("" (inst?) (("" (rewrite "neg_continuous_vv") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((neg_continuous_vv formula-decl nil cont_vect2_vect2 nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 nil))
   shostak))
(id_cont_vv_fun 0
  (id_cont_vv_fun-1 nil 3445172346
   ("" (expand "continuous_vv?")
    (("" (skosimp*)
      (("" (lemma "identity_continuous_vv") (("" (inst?) nil nil))
        nil))
      nil))
    nil)
   ((Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (identity_continuous_vv formula-decl nil cont_vect2_vect2 nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 nil))
   shostak))
(continuous_vv_fun_TCC1 0
  (continuous_vv_fun_TCC1-1 nil 3302273405
   ("" (inst + "(LAMBDA (x: Vect2): zero)")
    (("" (expand "continuous_vv?")
      (("" (skosimp*)
        (("" (expand "continuous_vv?")
          (("" (skosimp*)
            (("" (inst + "1")
              (("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_vv? const-decl "bool" cont_vect2_vect2 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)
    (>= 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)
    (neg_zero formula-decl nil vectors_2D "vectors/")
    (sub_zero_left formula-decl nil vectors_2D "vectors/")
    (norm_zero formula-decl nil vectors_2D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (continuous_vv? const-decl "bool" cont_vect2_vect2 nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil))
   nil))
(sum_fun_continuous_vv 0
  (sum_fun_continuous_vv-1 nil 3302273405
   ("" (skosimp*)
    (("" (typepred "h1!1")
      (("" (typepred "h2!1")
        (("" (expand "continuous_vv?")
          (("" (skosimp*)
            (("" (inst?)
              (("" (inst?) (("" (rewrite "sum_continuous_vv") nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 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)
    (sum_continuous_vv formula-decl nil cont_vect2_vect2 nil))
   nil))
(diff_fun_continuous_vv 0
  (diff_fun_continuous_vv-1 nil 3302273405
   ("" (skosimp*)
    (("" (typepred "h1!1")
      (("" (typepred "h2!1")
        (("" (expand "continuous_vv?")
          (("" (skosimp*)
            (("" (inst?)
              (("" (inst?)
                (("" (rewrite "diff_continuous_vv") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 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)
    (diff_continuous_vv formula-decl nil cont_vect2_vect2 nil))
   nil))
(const_fun_continuous_vv 0
  (const_fun_continuous_vv-1 nil 3302273405
   ("" (expand "continuous_vv?")
    (("" (grind :defs nil :rewrites ("const_continuous_vv")) nil nil))
    nil)
   ((const_continuous_vv formula-decl nil cont_vect2_vect2 nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 nil))
   nil))
(neg_fun_continuous_vv 0
  (neg_fun_continuous_vv-1 nil 3302273405
   ("" (skosimp*)
    (("" (typepred "h!1")
      (("" (expand "continuous_vv?")
        (("" (skosimp*)
          (("" (inst?) (("" (rewrite "neg_continuous_vv") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous_vv_fun nonempty-type-eq-decl nil cont_vect2_vect2 nil)
    (continuous_vv? const-decl "bool" cont_vect2_vect2 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)
    (neg_continuous_vv formula-decl nil cont_vect2_vect2 nil))
   nil)))

quality95%

¤ Dauer der Verarbeitung: 0.15 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.