let I be InitHalting good 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