let s be State of SCM+FSA; :: thesis: for aa, bb, cc being Int-Location
for I being parahalting Program of {INT,(INT *)} holds ProperForUpBody aa,bb,cc,I,s
let aa, bb, cc be Int-Location ; :: thesis: for I being parahalting Program of {INT,(INT *)} holds ProperForUpBody aa,bb,cc,I,s
let I be parahalting Program of {INT,(INT *)}; :: 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