:: deftheorem Def3 defines ExitsAtWhile=0 SCMFSA9A:def 3 :
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) ) );