Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_prefix_suffix.prf Sprache: Lisp

Original von: PVS^©

(csequence_prefix_suffix
(prefix_suffix_eta 0
  (prefix_suffix_eta-1 nil 3513622227
   ("" (induct "n")
    (("1" (skolem!)
      (("1" (expand* "prefix" "suffix")
        (("1" (rewrite "o_empty_left") nil nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "prefix" +)
        (("2" (expand "suffix" +)
          (("2" (lift-if)
            (("2" (rewrite "o_empty_left")
              (("2" (ground)
                (("2" (rewrite "o_add")
                  (("2" (decompose-equality)
                    (("2" (inst - "rest(cseq!1)") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (o_add formula-decl nil csequence_concatenate nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (add_finite application-judgement "nonempty_finite_csequence[T]"
     csequence_prefix_suffix nil)
    (o_nonempty_left application-judgement "nonempty_csequence"
     csequence_prefix_suffix nil)
    (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil)
    (empty_csequence nonempty-type-eq-decl nil csequence_props nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (o_empty_left formula-decl nil csequence_concatenate nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))"
     csequence_suffix nil)
    (suffix? inductive-decl "bool" csequence_suffix nil)
    (prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix
     nil)
    (prefix? coinductive-decl "bool" csequence_prefix nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (O const-decl "csequence" csequence_concatenate nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_prefix_suffix nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(prefix_suffix_extensionality 0
  (prefix_suffix_extensionality-1 nil 3513622296
   ("" (skosimp)
    (("" (lemma "prefix_suffix_eta")
      (("" (inst-cp - "cseq2!1" "n!1")
        (("" (inst - "cseq1!1" "n!1") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((prefix_suffix_eta formula-decl nil csequence_prefix_suffix nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_prefix_suffix nil))
   shostak)))

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