Quelle csequence_rest.prf Sprache: Lisp

(csequence_rest
(rest_finite 0
  (rest_finite-1 nil 3513477709
   ("" (skolem-typepred)
    (("" (expand "is_finite" -) (("" (propax) nil nil)) nil)) nil)
   ((nonempty_finite_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_rest nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(rest_infinite 0
  (rest_infinite-1 nil 3513477709
   ("" (skolem-typepred)
    (("" (expand "is_finite" +) (("" (flatten) nil nil)) nil)) nil)
   ((infinite_csequence type-eq-decl nil csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_rest nil))
   nil))
(rest_empty_add 0
  (rest_empty_add-1 nil 3513477777
   ("" (skolem!)
    (("" (prop)
      (("1" (inst + "first(nseq!1)")
        (("1" (decompose-equality) nil nil)) nil)
       ("2" (skolem!) (("2" (replace -1) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((csequence_add_extensionality formula-decl nil csequence_codt nil)
    (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_rest nil))
   shostak))
(rest_empty 0
  (rest_empty-1 nil 3513477823
   ("" (skolem!)
    (("" (expand* "is_finite" "is_finite" "length" "length")
      (("" (ground) nil nil)) nil))
    nil)
   ((length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   shostak))
(rest_nonempty 0
  (rest_nonempty-1 nil 3513477866
   ("" (skolem!)
    (("" (use "rest_empty")
      (("" (lemma "length_empty?_rew" ("cseq" "nseq!1"))
        (("" (ground) nil nil)) nil))
      nil))
    nil)
   ((rest_empty formula-decl nil csequence_rest nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_rest nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length_empty?_rew formula-decl nil csequence_length nil))
   shostak))
(rest_first_TCC1 0
  (rest_first_TCC1-1 nil 3513477709
   ("" (skosimp) (("" (expand* "index?" "index?") nil nil)) nil)
   ((index? def-decl "bool" csequence_nth nil)) nil))
(rest_first 0
  (rest_first-1 nil 3513477945
   ("" (skosimp) (("" (expand* "nth" "nth") nil nil)) nil)
   ((nth def-decl "T" csequence_nth nil)) shostak))
(rest_length 0
  (rest_length-1 nil 3513477958
   ("" (expand "length" 1 2) (("" (propax) nil nil)) nil)
   ((length def-decl "{n | has_length(fseq, n)}" csequence_length nil))
   shostak))
(rest_index 0
  (rest_index-1 nil 3513477977
   ("" (expand "index?" 1 2) (("" (propax) nil nil)) nil)
   ((index? def-decl "bool" csequence_nth nil)) shostak))
(rest_nth_TCC1 0
  (rest_nth_TCC1-1 nil 3513477709
   ("" (expand "index?") (("" (propax) nil nil)) nil)
   ((index? def-decl "bool" csequence_nth nil)) nil))
(rest_nth 0
  (rest_nth-1 nil 3513478014
   ("" (expand "nth" 1 2) (("" (propax) nil nil)) nil)
   ((nth def-decl "T" csequence_nth nil)) shostak))
(rest_some 0
  (rest_some-1 nil 3513478020
   ("" (expand "some" 1 1) (("" (propax) nil nil)) nil)
   ((some inductive-decl "boolean" csequence_codt nil)) shostak))
(rest_every 0
  (rest_every-1 nil 3513478028
   ("" (expand "every" 1 1) (("" (propax) nil nil)) nil)
   ((every coinductive-decl "boolean" csequence_codt nil)) shostak)))

quality100%

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