let s be State of SCM+FSA; :: thesis: for aa, bb, cc being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being parahalting Program of holds ProperForUpBody aa,bb,cc,I,s,p
let aa, bb, cc be Int-Location ; :: thesis: for p being Instruction-Sequence of SCM+FSA
for I being parahalting Program of holds ProperForUpBody aa,bb,cc,I,s,p
let p be Instruction-Sequence of SCM+FSA; :: thesis: for I being parahalting Program of holds ProperForUpBody aa,bb,cc,I,s,p
let I be parahalting Program of ; :: thesis: ProperForUpBody aa,bb,cc,I,s,p
let i be Element of NAT ; :: according to SFMASTR3:def 2 :: thesis: ( i < ((s . cc) - (s . bb)) + 1 implies ( I is_closed_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) & I is_halting_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) ) )
assume i < ((s . cc) - (s . bb)) + 1 ; :: thesis: ( I is_closed_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) & I is_halting_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) )
thus I is_closed_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by SCMFSA7B:18; :: thesis: I is_halting_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0))))))
thus I is_halting_on (StepForUp (aa,bb,cc,I,p,s)) . i,p +* (while>0 ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),((I ';' (AddTo (aa,(intloc 0)))) ';' (SubFrom ((1 -stRWNotIn ({aa,bb,cc} \/ (UsedIntLoc I))),(intloc 0)))))) by SCMFSA7B:19; :: thesis: verum