for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being InitHalting really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Nat st
( s2 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 2 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) )