Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: numbers_infinite.prf Sprache: Lisp

Original von: PVS^©

(numbers_infinite
(nat_infinite 0
  (nat_infinite-1 nil 3314538968
   ("" (expand "is_finite_type")
    (("" (skolem!)
      ((""
        (lemma
         "composition_injective[below[N!1 + 1], nat, below[N!1]]")
        (("" (inst - "LAMBDA (n: below[N!1 + 1]): n" "g!1")
          (("1" (lemma "injection_n_to_m")
            (("1" (inst - "N!1" "N!1 + 1")
              (("1" (assert) (("1" (inst?) nil nil)) nil)) nil))
            nil)
           ("2" (expand "injective?") (("2" (skosimp) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((N!1 skolem-const-decl "nat" numbers_infinite nil)
    (injective? const-decl "bool" functions nil)
    (g!1 skolem-const-decl "[nat -> below[N!1]]" numbers_infinite nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (O const-decl "T3" function_props nil)
    (injection_n_to_m formula-decl nil nat_fun_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (composition_injective judgement-tcc nil function_props 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (below type-eq-decl nil nat_types nil)
    (is_finite_type const-decl "bool" finite_sets nil))
   shostak))
(int_infinite 0
  (int_infinite-1 nil 3314539260
   ("" (lemma "nat_infinite")
    (("" (rewrite "finite_full")
      (("" (rewrite "finite_full")
        (("" (assert)
          ((""
            (lemma "finite_subset[int]"
             ("A" "fullset[int]" "s" "fullset[nat]"))
            (("" (rewrite "finite_extension[int, nat]")
              (("" (expand* "extend" "subset?" "member" "fullset") nil
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_full formula-decl nil finite_sets 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)
    (finite_extension formula-decl nil extend_set_props nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (finite_subset formula-decl nil finite_sets 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)
    (fullset const-decl "set" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (nat_infinite formula-decl nil numbers_infinite nil))
   shostak))
(rat_infinite 0
  (rat_infinite-1 nil 3314539402
   ("" (lemma "nat_infinite")
    (("" (rewrite "finite_full")
      (("" (rewrite "finite_full")
        (("" (assert)
          ((""
            (lemma "finite_subset[rat]"
             ("A" "fullset[rat]" "s" "fullset[nat]"))
            (("" (rewrite "finite_extension[rat, nat]")
              (("" (expand* "extend" "subset?" "member" "fullset") nil
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_full formula-decl nil finite_sets 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)
    (finite_extension formula-decl nil extend_set_props nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (finite_subset formula-decl nil finite_sets 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)
    (fullset const-decl "set" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (rat nonempty-type-eq-decl nil rationals nil)
    (nat_infinite formula-decl nil numbers_infinite nil))
   shostak))
(real_infinite 0
  (real_infinite-1 nil 3314539488
   ("" (lemma "nat_infinite")
    (("" (rewrite "finite_full")
      (("" (rewrite "finite_full")
        (("" (assert)
          ((""
            (lemma "finite_subset[real]"
             ("A" "fullset[real]" "s" "fullset[nat]"))
            (("" (rewrite "finite_extension[real, nat]")
              (("" (expand* "extend" "subset?" "member" "fullset") nil
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_full formula-decl nil finite_sets 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)
    (finite_extension formula-decl nil extend_set_props nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (finite_subset formula-decl nil finite_sets 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)
    (fullset const-decl "set" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (nat_infinite formula-decl nil numbers_infinite nil))
   shostak)))

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