:: deftheorem Def6 defines ExitsAtWhile>0 SCMFSA9A:def 6 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) & WithVariantWhile>0 a,I,s,p holds
for b₅ being Nat holds
( b₅ = ExitsAtWhile>0 (a,I,p,s) iff ex k being Nat st
( b₅ = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) );