let s be State of SCM+FSA ; :: thesis: for aa, bb, cc being Int-Location
for I being parahalting Program of SCM+FSA holds ProperForUpBody aa,bb,cc,I,s
let aa, bb, cc be Int-Location ; :: thesis: for I being parahalting Program of SCM+FSA holds ProperForUpBody aa,bb,cc,I,s
let I be parahalting Program of SCM+FSA ; :: thesis: ProperForUpBody aa,bb,cc,I,s
let i be Element of NAT ; :: according to SFMASTR3:def 7 :: thesis: ( i < ((s . cc) - (s . bb)) + 1 implies ( I is_closed_on (StepForUp aa,bb,cc,I,s) . i & I is_halting_on (StepForUp aa,bb,cc,I,s) . i ) )
assume i < ((s . cc) - (s . bb)) + 1 ; :: thesis: ( I is_closed_on (StepForUp aa,bb,cc,I,s) . i & I is_halting_on (StepForUp aa,bb,cc,I,s) . i )
thus I is_closed_on (StepForUp aa,bb,cc,I,s) . i by SCMFSA7B:24; :: thesis: I is_halting_on (StepForUp aa,bb,cc,I,s) . i
thus I is_halting_on (StepForUp aa,bb,cc,I,s) . i by SCMFSA7B:25; :: thesis: verum