let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds
if>0 (a,I,J) is_halting_onInit s,p
let s be State of SCM+FSA; for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds
if>0 (a,I,J) is_halting_onInit s,p
let I, J be really-closed MacroInstruction of SCM+FSA ; for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds
if>0 (a,I,J) is_halting_onInit s,p
let a be read-write Int-Location; ( s . a > 0 & I is_halting_onInit s,p implies if>0 (a,I,J) is_halting_onInit s,p )
set Is = Initialized s;
assume
s . a > 0
; ( not I is_halting_onInit s,p or if>0 (a,I,J) is_halting_onInit s,p )
then A1:
(Initialized s) . a > 0
by SCMFSA_M:37;
assume
I is_halting_onInit s,p
; if>0 (a,I,J) is_halting_onInit s,p
then
I is_halting_on Initialized s,p
by Th27;
then
if>0 (a,I,J) is_halting_on Initialized s,p
by A1, SCMFSA8B:19;
hence
if>0 (a,I,J) is_halting_onInit s,p
by Th27; verum