let I be InitHalting good really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) holds
while>0 (a,I) is InitHalting
let a be read-write Int-Location; :: thesis: ( ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) implies while>0 (a,I) is InitHalting )
assume A1: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ; :: thesis: while>0 (a,I) is InitHalting

now :: thesis: for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA st t . a > 0 holds
(IExec (I,Q,t)) . a < t . a

let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA st t . a > 0 holds
(IExec (I,b₃,b₂)) . a < b₂ . a
let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a > 0 implies (IExec (I,b₂,b₁)) . a < b₁ . a )
assume A2: t . a > 0 ; :: thesis: (IExec (I,b₂,b₁)) . a < b₁ . a

per cases ( (IExec (I,Q,t)) . a < t . a or (IExec (I,Q,t)) . a <= 0 ) by A1;

suppose (IExec (I,Q,t)) . a < t . a ; :: thesis: (IExec (I,b₂,b₁)) . a < b₁ . a

hence (IExec (I,Q,t)) . a < t . a ; :: thesis: verum

end;

suppose (IExec (I,Q,t)) . a <= 0 ; :: thesis: (IExec (I,b₂,b₁)) . a < b₁ . a

hence (IExec (I,Q,t)) . a < t . a by A2; :: thesis: verum

end;

end;

end;

hence while>0 (a,I) is InitHalting by SCM_HALT:76; :: thesis: verum