(transitions
 (states_TCC1 0
  (states_TCC1-1 nil 3237448483 nil nil nil nil nil nil nil shostak))
 (REACHABLE_weak_induction 0
  (REACHABLE_weak_induction-1 nil 3237479804 nil nil nil nil nil nil
   nil shostak))
 (REACHABLE_induction 0
  (REACHABLE_induction-1 nil 3237479804 nil nil nil nil nil nil nil
   shostak))
 (indinv_is_invariant 0
  (indinv_is_invariant-1 nil 3237457696 3237479844
   ("" (skosimp)
    (("" (expand "invariant")
      (("" (skosimp)
        (("" (lemma "REACHABLE_weak_induction")
          (("" (inst?) (("" (lazy-grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   unchecked
   ((invariant const-decl "bool" transitions nil)
    (REACHABLE_weak_induction formula-decl nil transitions nil)
    (indinv const-decl "bool" transitions nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (states formal-nonempty-type-decl nil transitions nil))
   29558 2020 t shostak))
 (invariant_closed_on_reachable 0
  (invariant_closed_on_reachable-1 nil 3237776390 3237776971
   ("" (skosimp*)
    (("" (expand "invariant")
      (("" (case "REACHABLE(t!1)")
        (("1" (inst - "t!1") (("1" (ground) nil nil)) nil)
         ("2" (hide -1 -3 2)
          (("2" (expand "REACHABLE" +)
            (("2" (ground) (("2" (inst?) (("2" (ground) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((invariant const-decl "bool" transitions nil)
    (states formal-nonempty-type-decl nil transitions nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (REACHABLE inductive-decl "bool" transitions nil))
   125198 5900 t shostak)))