Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: absconv_series_aux.prf Sprache: Lisp

Original von: PVS^©

(finite_enumeration
(finite_enumeration_TCC1 0
  (finite_enumeration_TCC1-1 nil 3322363999
   ("" (expand "nonempty?")
    (("" (expand "empty?")
      (("" (expand "member")
        (("" (skosimp*)
          (("" (lemma "bij_exists" ("S" "X!1"))
            (("" (skosimp)
              (("" (lemma "bijective_inverse_exists" ("f" "f!1"))
                (("1" (expand "exists1")
                  (("1" (flatten)
                    (("1" (skosimp)
                      (("1" (inst - "x!1")
                        (("1"
                          (lemma "bij_inv_is_bij_alt"
                           ("f" "f!1" "g" "x!1"))
                          (("1" (propax) nil nil)
                           ("2" (propax) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" sets nil)
    (exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (below type-eq-decl nil nat_types nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (bijective? const-decl "bool" functions 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (below type-eq-decl nil naturalnumbers nil)
    (bij_exists formula-decl nil finite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (T formal-type-decl nil finite_enumeration nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   shostak))
(finite_enumeration_bij 0
  (finite_enumeration_bij-1 nil 3322365352
   ("" (skosimp)
    (("" (expand "finite_enumeration") (("" (propax) nil nil)) nil))
    nil)
   ((finite_enumeration const-decl "[below[card(X)] -> (X)]"
     finite_enumeration nil))
   shostak))
(finite_enumeration_image 0
  (finite_enumeration_image-1 nil 3322365404
   ("" (skosimp)
    (("" (expand "fullset")
      (("" (expand "image")
        (("" (expand "restrict")
          (("" (apply-extensionality :hide? t)
            (("" (lemma "finite_enumeration_bij" ("X" "X!1"))
              (("" (expand "bijective?")
                (("" (flatten)
                  (("" (expand "surjective?")
                    (("" (inst - "x!1")
                      (("" (skosimp)
                        (("" (inst + "x!2") (("" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset const-decl "set" sets nil)
    (restrict const-decl "R" restrict nil)
    (finite_enumeration_bij formula-decl nil finite_enumeration nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (below type-eq-decl nil nat_types nil)
    (TRUE const-decl "bool" booleans nil)
    (finite_enumeration const-decl "[below[card(X)] -> (X)]"
     finite_enumeration nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil finite_enumeration nil)
    (image const-decl "set[R]" function_image nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.