// example from page 106
// not provable since inReachableState is missing

\javaSource "source/control";

\problem {

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

}