let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P )
let I be Program of SCM+FSA; :: thesis: for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P )
let a be read-write Int-Location; :: thesis: ( s . a <= 0 implies ( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P ) )
set s0 = Initialized s;
assume s . a <= 0 ; :: thesis: ( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P )
then A1: (Initialized s) . a <= 0 by SCMFSA_M:37;
then A2: while>0 (a,I) is_closed_on Initialized s,P by SCMFSA_9:38;
while>0 (a,I) is_halting_on Initialized s,P by A1, SCMFSA_9:38;
hence ( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P ) by A2, SCM_HALT:30, SCM_HALT:31; :: thesis: verum