SSL csequence_add.prf   Interaktion und
PortierbarkeitLisp

(csequence_add
 (add_finite 0
  (add_finite-1 nil 3513474090
   ("" (expand "is_finite") (("" (propax) nil nil)) nil)
   ((is_finite inductive-decl "bool" csequence_props nil)) nil))
 (add_infinite 0
  (add_infinite-1 nil 3513474090
   ("" (expand "is_finite") (("" (propax) nil nil)) nil)
   ((is_finite inductive-decl "bool" csequence_props nil)) nil))
 (add_length 0
  (add_length-1 nil 3513474119
   ("" (expand "length" 1 1) (("" (propax) nil nil)) nil)
   ((length def-decl "{n | has_length(fseq, n)}" csequence_length nil))
   shostak))
 (add_index_TCC1 0
  (add_index_TCC1-1 nil 3513474090 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (>= const-decl "bool" 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (add_index 0
  (add_index-1 nil 3513474177
   ("" (expand "index?" 1 1) (("" (propax) nil nil)) nil)
   ((index? def-decl "bool" csequence_nth nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (add_nth_TCC1 0
  (add_nth_TCC1-1 nil 3513474090
   ("" (expand "index?") (("" (propax) nil nil)) nil)
   ((index? def-decl "bool" csequence_nth nil)) nil))
 (add_nth 0
  (add_nth-1 nil 3513474195
   ("" (expand "nth" 1 1) (("" (propax) nil nil)) nil)
   ((nth def-decl "T" csequence_nth nil)) shostak))
 (add_last_TCC1 0
  (add_last_TCC1-1 nil 3513474090 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil csequence_add nil)
    (csequence type-decl nil csequence_codt nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil))
   nil))
 (add_last 0
  (add_last-1 nil 3513474207
   ("" (skolem!)
    (("" (expand "last")
      (("" (expand "length" 1 1)
        (("" (expand "nth" 1 1)
          (("" (use "length_empty?_rew")
            (("" (lift-if) (("" (lift-if) (("" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((last const-decl "T" csequence_nth nil)
    (nth def-decl "T" csequence_nth nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (csequence type-decl nil csequence_codt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (T formal-type-decl nil csequence_add nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil))
   shostak))
 (add_some 0
  (add_some-1 nil 3513474245
   ("" (expand "some" 1 1) (("" (propax) nil nil)) nil)
   ((some inductive-decl "boolean" csequence_codt nil)) shostak))
 (add_every 0
  (add_every-1 nil 3513474251
   ("" (expand "every" 1 1) (("" (propax) nil nil)) nil)
   ((every coinductive-decl "boolean" csequence_codt nil)) shostak)))