let s be State of SCM+FSA ; :: thesis: for a being read-write Int-Location
for I being parahalting Program of SCM+FSA st WithVariantWhile>0 a,I,s holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
let a be read-write Int-Location ; :: thesis: for I being parahalting Program of SCM+FSA st WithVariantWhile>0 a,I,s holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
let I be parahalting Program of SCM+FSA ; :: thesis: ( WithVariantWhile>0 a,I,s implies ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s ) )
assume A1: WithVariantWhile>0 a,I,s ; :: thesis: ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
ProperBodyWhile>0 a,I,s

proof

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 & I is_halting_on (StepWhile>0 a,I,s) . k ) by SCMFSA7B:24, SCMFSA7B:25; :: thesis: verum

end;

hence ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s ) by A1, Th33; :: thesis: verum