:: deftheorem Def1 defines StepWhile=0 SCMFSA_9:def 1 :
for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location
for P being Instruction-Sequence of SCM+FSA
for b₅ being sequence of (product (the_Values_of SCM+FSA)) holds
( b₅ = StepWhile=0 (a,I,P,s) iff ( b₅ . 0 = s & ( for i being Nat holds b₅ . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b₅ . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b₅ . i)))) + 2)) ) ) );