Quelle csequence_singleton.prf Sprache: Lisp

(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)))

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.