(pvsio_examples
 (pp_TCC1 0
  (pp_TCC1-1 nil 3578924707
   ("" (skeep*) (("" (inst 1 "((:1:),true,1)") nil nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (list type-decl nil list_adt nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (every adt-def-decl "boolean" list_adt nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (>= const-decl "bool" reals nil)
    (nonneg_rat nonempty-type-eq-decl nil rationals nil)
    (> const-decl "bool" reals nil)
    (posrat nonempty-type-eq-decl nil rationals nil)
    (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (TRUE const-decl "bool" booleans nil))
   nil)))