products/sources/formale sprachen/PVS/fault_tolerance/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: csequence_singleton.prf   Sprache: Unknown

(csequence_singleton
 (singleton_is_nonempty_finite 0
  (singleton_is_nonempty_finite-1 nil 3513602144
   ("" (skolem-typepred)
    (("" (expand* "singleton_cseq?" "is_finite" "is_finite")
      (("" (ground) nil nil)) nil))
    nil)
   ((is_finite inductive-decl "bool" csequence_props nil)
    (singleton_cseq? const-decl "bool" csequence_singleton nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_singleton nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (singleton_cseq_length_TCC1 0
  (singleton_cseq_length_TCC1-1 nil 3513602144
   ("" (skosimp)
    (("" (use "singleton_is_nonempty_finite") (("" (flatten) nil nil))
      nil))
    nil)
   ((singleton_is_nonempty_finite judgement-tcc nil csequence_singleton
     nil)
    (T formal-type-decl nil csequence_singleton nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (singleton_cseq? const-decl "bool" csequence_singleton nil)
    (cseq!1 skolem-const-decl "csequence[T]" csequence_singleton nil))
   nil))
 (singleton_cseq_length 0
  (singleton_cseq_length-1 nil 3513602213 ("" (grind) nil nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (T formal-type-decl nil csequence_singleton nil)
    (singleton_cseq? const-decl "bool" csequence_singleton nil))
   shostak))
 (singleton_cseq_index 0
  (singleton_cseq_index-1 nil 3513602225
   ("" (skolem-typepred)
    (("" (expand* "singleton_cseq?" "index?" "index?")
      (("" (ground) nil nil)) nil))
    nil)
   ((index? def-decl "bool" csequence_nth nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (>= const-decl "bool" reals 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)
    (singleton_cseq? const-decl "bool" csequence_singleton nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_singleton nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
 (singleton_cseq_TCC1 0
  (singleton_cseq_TCC1-1 nil 3513602144 ("" (subtype-tcc) nil nil)
   ((singleton_cseq? const-decl "bool" csequence_singleton nil)) nil))
 (singleton_def_TCC1 0
  (singleton_def_TCC1-1 nil 3513602144 ("" (subtype-tcc) nil nil)
   ((singleton_cseq? const-decl "bool" csequence_singleton nil)) nil))
 (singleton_def 0
  (singleton_def-1 nil 3513602256 ("" (grind-with-ext) nil nil)
   ((add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_singleton nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (singleton_cseq? const-decl "bool" csequence_singleton nil)
    (singleton_cseq const-decl "(singleton_cseq?)" csequence_singleton
     nil))
   shostak))
 (singleton_cseq_first 0
  (singleton_cseq_first-1 nil 3513602271 ("" (grind) nil nil)
   ((singleton_cseq const-decl "(singleton_cseq?)" csequence_singleton
     nil))
   shostak))
 (singleton_cseq_rest 0
  (singleton_cseq_rest-1 nil 3513602276 ("" (grind) nil nil)
   ((singleton_cseq const-decl "(singleton_cseq?)" csequence_singleton
     nil))
   shostak))
 (singleton_cseq_last 0
  (singleton_cseq_last-1 nil 3513602279 ("" (grind) nil nil)
   ((singleton_cseq const-decl "(singleton_cseq?)" csequence_singleton
     nil)
    (T formal-type-decl nil csequence_singleton nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (nth def-decl "T" csequence_nth nil)
    (last const-decl "T" csequence_nth nil))
   shostak))
 (singleton_cseq_some 0
  (singleton_cseq_some-1 nil 3513602283
   ("" (expand* "singleton_cseq" "some" "some") nil nil)
   ((some inductive-decl "boolean" csequence_codt nil)
    (singleton_cseq const-decl "(singleton_cseq?)" csequence_singleton
     nil))
   shostak))
 (singleton_cseq_every 0
  (singleton_cseq_every-1 nil 3513602321
   ("" (expand* "singleton_cseq" "every" "every") nil nil)
   ((every coinductive-decl "boolean" csequence_codt nil)
    (singleton_cseq const-decl "(singleton_cseq?)" csequence_singleton
     nil))
   shostak)))

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]