products/Sources/formale Sprachen/Isabelle/Doc/Sledgehammer/document/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: middle_third_pigeonhole.pvs   Sprache: Lisp

Untersuchung PVS©
(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)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.17Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff