// example from page 106
// provable since inReachableState is part of the assumption
// In the KeY system, inReachableState cannot be expanded as described in
// the book (since the resulting formula would be too large). Rather, apply rule
// "referenced_object_is_created" on the term c.data. Then the proof can be closed
// automatically

\javaSource "source/control";


\problem {

    \forall Control c;( inReachableState & \forall Data data;(data.<created>=TRUE -> data.d >= 0) ->
			(c.<created>=TRUE & c!=null & c.data!=null -> c.data.d >= 0) )

}