(PVSHOL
 (f_TCC1 0
  (f_TCC1-1 nil 3310429087 3310429088 ("" (cond-disjoint-tcc) nil nil)
   unfinished nil 751 460 nil shostak))
 (f_TCC2 0
  (f_TCC2-1 nil 3310429088 3310429089 ("" (cond-coverage-tcc) nil nil)
   unfinished nil 276 170 nil shostak))
 (Test 0
  (Test-1 nil 3310429133 3310726846
   ("" (expand "Reachable")
    (("" (skolem!)
      (("" (flatten)
        (("" (inst-cp -1 "a" "b" "d")
          (("" (bddsimp)
            (("1" (inst - "b" "d" "d") (("1" (grind) nil nil)) nil)
             ("2" (grind) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((state type-decl nil PVSHOL nil)
    (boolean nonempty-type-decl nil booleans nil)
    (a? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (a adt-constructor-decl "(a?)" PVSHOL nil)
    (b? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (b adt-constructor-decl "(b?)" PVSHOL nil)
    (d? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (d adt-constructor-decl "(d?)" PVSHOL nil)
    (R const-decl "bool" PVSHOL nil)
    (Reachable const-decl "bool" PVSHOL nil))
   363333 5530 t shostak))
 (Test2 0
  (Test2-2 "Using lambda to define P" 3310431768 3310431768
   ("" (expand "Reachable")
    ((""
      (inst -1
       "(lambda (r,s:state): r=s OR r=a or ((r=b OR r=c) & (s=d OR s=e)) OR r=d & s=e)")
      (("" (grind) nil nil)) nil))
    nil)
   proved-complete nil 185261 3600 t shostak)
  (Test2-1 nil 3310429898 3310431047
   ("" (expand "Reachable")
    (("" (inst -1 "myP") (("" (grind) nil nil)) nil)) nil)
   proved
   ((state type-decl nil PVSHOL nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (PRED type-eq-decl nil defined_types nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (a? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (a adt-constructor-decl "(a?)" PVSHOL nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (b? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (b adt-constructor-decl "(b?)" PVSHOL nil)
    (c? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (c adt-constructor-decl "(c?)" PVSHOL nil)
    (d? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (d adt-constructor-decl "(d?)" PVSHOL nil)
    (e? adt-recognizer-decl "[state -> boolean]" PVSHOL nil)
    (e adt-constructor-decl "(e?)" PVSHOL nil)
    (R const-decl "bool" PVSHOL nil)
    (Reachable const-decl "bool" PVSHOL nil))
   40569 2070 t shostak)))