let I be good InitHalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st ( for s being State of SCM+FSA holds
( (IExec I,s) . a < s . a or (IExec I,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 holds
( (IExec I,s) . a < s . a or (IExec I,s) . a <= 0 ) ) implies while>0 a,I is InitHalting )
assume A1: for s being State of SCM+FSA holds
( (IExec I,s) . a < s . a or (IExec I,s) . a <= 0 ) ; :: thesis: while>0 a,I is InitHalting

now

let t be State of SCM+FSA ; :: thesis: ( t . a > 0 implies (IExec I,b₁) . a < b₁ . a )
assume A2: t . a > 0 ; :: thesis: (IExec I,b₁) . a < b₁ . a

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

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

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

end;

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

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

end;

end;

end;

hence while>0 a,I is InitHalting by Th29; :: thesis: verum