:: deftheorem Def1 defines StepWhile>0 SCMISORT: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,P,s,I) iff ( b₅ . 0 = s & ( for i being Nat holds b₅ . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (b₅ . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (b₅ . i)))) + 2)) ) ) );