Quelle  csequence_prefix_append.prf   Sprache: Lisp

(csequence_prefix_append
 (prefix_append_eta 0
  (prefix_append_eta-1 nil 3513622372
   ("" (skolem + ("_" "t!1"))
    (("" (induct "fseq" :name "is_finite_induction")
      (("1" (assert) nil nil) ("2" (assert) nil nil)
       ("3" (skosimp)
        (("3" (use "length_empty?_rew")
          (("3" (expand "length" +)
            (("3" (expand "prefix" +)
              (("3" (expand* "append" "append_struct")
                (("3" (expand "coreduce" +)
                  (("3" (reduce) (("3" (decompose-equality 3) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (prefix? coinductive-decl "bool" csequence_prefix nil)
    (prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix
     nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (has_length def-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (T formal-type-decl nil csequence_prefix_append nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (coreduce adt-def-decl "{c: csequence[T] |
         inj_empty?(op(x)) AND empty?(c) OR
          inj_nonempty?(op(x)) AND nonempty?(c)}"
     csequence_codt_coreduce nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (add_finite application-judgement "nonempty_finite_csequence[T]"
     csequence_prefix_append nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (append_struct const-decl "csequence_struct" csequence_append nil))
   shostak)))