let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being parahalting Program of SCM+FSA holds ProperBodyWhile>0 a,I,s
let a be read-write Int-Location ; :: thesis: for I being parahalting Program of SCM+FSA holds ProperBodyWhile>0 a,I,s
let I be parahalting Program of SCM+FSA; :: thesis: ProperBodyWhile>0 a,I,s
let k be Element of NAT ; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (a,I,s)) . k) . a > 0 implies ( I is_closed_on (StepWhile>0 (a,I,s)) . k & I is_halting_on (StepWhile>0 (a,I,s)) . k ) )
assume ((StepWhile>0 (a,I,s)) . k) . a > 0 ; :: thesis: ( I is_closed_on (StepWhile>0 (a,I,s)) . k & I is_halting_on (StepWhile>0 (a,I,s)) . k )
thus I is_closed_on (StepWhile>0 (a,I,s)) . k by SCMFSA7B:24; :: thesis: I is_halting_on (StepWhile>0 (a,I,s)) . k
thus I is_halting_on (StepWhile>0 (a,I,s)) . k by SCMFSA7B:25; :: thesis: verum