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,b3,b2)) . a < b2 . a
let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( t . a > 0 implies (IExec (I,b2,b1)) . a < b1 . a )
assume A2: t . a > 0 ; :: thesis: (IExec (I,b2,b1)) . a < b1 . 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,b2,b1)) . a < b1 . a
hence (IExec (I,Q,t)) . a < t . a ; :: thesis: verum
end;
suppose (IExec (I,Q,t)) . a <= 0 ; :: thesis: (IExec (I,b2,b1)) . a < b1 . 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