theorem Th29: :: SCMFSA9A:29

for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )