Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: partial_function_props.prf Sprache: Lisp

Original von: PVS^©

(powerseries
(powerseries_TCC1 0
  (powerseries_TCC1-1 nil 3507981245
   ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(powerseries_TCC2 0
  (powerseries_TCC2-1 nil 3507981245 ("" (subtype-tcc) nil nil) nil
   nil))
(powerseries_TCC3 0
  (powerseries_TCC3-1 nil 3507981245 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
(cauchy_powerseries_TCC1 0
  (cauchy_powerseries_TCC1-1 nil 3507981245 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (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))
   nil))
(cauchy_powerseries_TCC2 0
  (cauchy_powerseries_TCC2-1 nil 3507981245
   ("" (skosimp*)
    (("" (typepred "cxs!1")
      (("" (expand "cauchys_real?")
        (("" (typepred "cx!1")
          (("" (expand "cauchy_real?")
            (("" (skosimp*)
              ((""
                (inst +
                 "(LAMBDA i: IF i = 0 THEN xs!1(i) ELSE xs!1(i)*x!1^i ENDIF)")
                (("" (assert)
                  (("" (expand "cauchys_prop")
                    (("" (skosimp*)
                      (("" (inst - "n!1")
                        (("" (lemma "trichotomy" ("x" "n!1"))
                          (("" (split -1)
                            (("1" (assert)
                              (("1"
                                (lemma
                                 "mul_lemma"
                                 ("x"
                                  "xs!1(n!1)"
                                  "y"
                                  "x!1 ^ n!1"
                                  "cx"
                                  "cxs!1(n!1)"
                                  "cy"
                                  "cauchy_power(cx!1, n!1)"))
                                (("1"
                                  (lemma
                                   "power_lemma"
                                   ("x" "x!1" "pn" "n!1" "cx" "cx!1"))
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (assert) nil nil)
                             ("3" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchys_real nonempty-type-eq-decl nil sum nil)
    (cauchys_real? const-decl "bool" sum nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (trichotomy formula-decl nil real_axioms nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (power_lemma formula-decl nil power nil)
    (cauchy_power const-decl "cauchy_real" power nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (mul_lemma formula-decl nil mul nil)
    (cauchys_prop const-decl "bool" sum nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(powerseries_lemma_TCC1 0
  (powerseries_lemma_TCC1-1 nil 3507981245
   ("" (skosimp*)
    (("" (expand "cauchys_real?")
      (("" (inst + "xs!1")
        (("" (expand "cauchys_prop") (("" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((cauchys_real? const-decl "bool" sum nil)
    (cauchys_prop const-decl "bool" sum 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))
(powerseries_lemma 0
  (powerseries_lemma-1 nil 3507981245
   ("" (skosimp*)
    (("" (expand "powerseries")
      (("" (expand "cauchy_powerseries")
        ((""
          (lemma "sum_lemma"
           ("xs"
            "(LAMBDA i: IF i = 0 THEN xs!1(i) ELSE xs!1(i) * x!1 ^ i ENDIF)"
            "m" "m!1" "cxs"
            "(LAMBDA i: IF i = 0 THEN cxs!1(i) ELSE cauchy_mul(cxs!1(i), cauchy_power(cx!1, i)) ENDIF)"))
          (("1" (assert)
            (("1" (hide 2)
              (("1" (skosimp*)
                (("1" (lemma "trichotomy" ("x" "n!1"))
                  (("1" (inst - "n!1")
                    (("1" (split -1)
                      (("1" (simplify)
                        (("1" (assert)
                          (("1"
                            (lemma "mul_lemma"
                             ("x" "xs!1(n!1)" "y" "x!1 ^ n!1" "cx"
                              "cxs!1(n!1)" "cy"
                              "cauchy_power(cx!1, n!1)"))
                            (("1" (assert)
                              (("1"
                                (lemma
                                 "power_lemma"
                                 ("x" "x!1" "cx" "cx!1" "pn" "n!1"))
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (assert) nil nil) ("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((powerseries const-decl "real" powerseries nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cauchy_power const-decl "cauchy_real" power nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (cauchy_mul const-decl "cauchy_real" mul nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (cauchy_real nonempty-type-eq-decl nil cauchy nil)
    (cauchy_real? const-decl "bool" cauchy 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)
    (sum_lemma formula-decl nil sum nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (trichotomy formula-decl nil real_axioms nil)
    (power_lemma formula-decl nil power nil)
    (mul_lemma formula-decl nil mul nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (cauchy_powerseries const-decl "cauchy_real" powerseries nil))
   nil)))

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