theorem Th19:
for
s being
State of
SCM+FSA for
a being
read-write Int-Location for
bb,
cc being
Int-Location for
k being
Nat for
p being
Instruction-Sequence of
SCM+FSA for
Ig being
really-closed good MacroInstruction of
SCM+FSA st
s . (intloc 0) = 1 &
ProperForUpBody a,
bb,
cc,
Ig,
s,
p &
k < ((s . cc) - (s . bb)) + 1 holds
((StepForUp (a,bb,cc,Ig,p,s)) . (k + 1)) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations) = (IExec ((Ig ";" (AddTo (a,(intloc 0)))),(p +* (while>0 ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),((Ig ";" (AddTo (a,(intloc 0)))) ";" (SubFrom ((1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc Ig))),(intloc 0))))))),((StepForUp (a,bb,cc,Ig,p,s)) . k))) | (({a,bb,cc} \/ (UsedILoc Ig)) \/ FinSeq-Locations)