let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting Program of SCM+FSA st WithVariantWhile=0 a,I,s,p holds
( while=0 (a,I) is_halting_on s,p & while=0 (a,I) is_closed_on s,p )
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,p holds
( while=0 (a,I) is_halting_on s,p & while=0 (a,I) is_closed_on s,p )
let a be read-write Int-Location ; :: thesis: for I being parahalting Program of SCM+FSA st WithVariantWhile=0 a,I,s,p holds
( while=0 (a,I) is_halting_on s,p & while=0 (a,I) is_closed_on s,p )
let I be parahalting Program of SCM+FSA; :: thesis: ( WithVariantWhile=0 a,I,s,p implies ( while=0 (a,I) is_halting_on s,p & while=0 (a,I) is_closed_on s,p ) )
assume A1: WithVariantWhile=0 a,I,s,p ; :: thesis: ( while=0 (a,I) is_halting_on s,p & while=0 (a,I) is_closed_on s,p )
ProperBodyWhile=0 a,I,s,p

proof

let k be Element of NAT ; :: according to SCMFSA9A:def 1 :: thesis: ( ((StepWhile=0 (a,I,p,s)) . k) . a = 0 implies ( I is_closed_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) ) )
assume ((StepWhile=0 (a,I,p,s)) . k) . a = 0 ; :: thesis: ( I is_closed_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) )
thus ( I is_closed_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) ) by SCMFSA7B:18, SCMFSA7B:19; :: thesis: verum

end;

hence ( while=0 (a,I) is_halting_on s,p & while=0 (a,I) is_closed_on s,p ) by A1, Th20; :: thesis: verum