let P be Instruction-Sequence of SCM+FSA; :: thesis: for k being Nat
for s being State of SCM+FSA st s . (intloc (1 + 1)) = k & s . (intloc (1 + 1)) <= len (s . ()) holds
( s . () = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () & s . (intloc (2 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) & ( k = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . ()) . (k - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > k - n & i < k + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

defpred S1[ Nat] means for s being State of SCM+FSA st s . (intloc (1 + 1)) = \$1 & s . (intloc (1 + 1)) <= len (s . ()) holds
( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = s . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( \$1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= \$1 & ( \$1 - n >= 1 implies ( x1 = (s . ()) . (\$1 - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > \$1 - n & i < \$1 + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) );
A1: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for s being State of SCM+FSA st s . (intloc (1 + 1)) = k + 1 & s . (intloc (1 + 1)) <= len (s . ()) holds
( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = s . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
let s be State of SCM+FSA; :: thesis: ( s . (intloc (1 + 1)) = k + 1 & s . (intloc (1 + 1)) <= len (s . ()) implies ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . () = b1 . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( x1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . ()) . ((k + 1) - x1) & b3 >= n . (intloc (5 + 1)) ) ) & ( for i being Nat st b4 > (k + 1) - x1 & b4 < (k + 1) + 1 holds
ex x2 being Integer st
( b5 = (n . ()) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) ) )

assume that
A3: s . (intloc (1 + 1)) = k + 1 and
A4: s . (intloc (1 + 1)) <= len (s . ()) ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . () = b1 . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( x1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . ()) . ((k + 1) - x1) & b3 >= n . (intloc (5 + 1)) ) ) & ( for i being Nat st b4 > (k + 1) - x1 & b4 < (k + 1) + 1 holds
ex x2 being Integer st
( b5 = (n . ()) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) )

set bs = IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s);
set bs0 = Initialized (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s));
A5: s . (intloc (1 + 1)) >= 1 + 0 by ;
then consider m being Integer such that
A6: m = (s . ()) . (s . (intloc (1 + 1))) and
A7: ( m - (s . (intloc (5 + 1))) > 0 implies ( (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (1 + 1)) = 0 & (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) and
A8: ( m - (s . (intloc (5 + 1))) <= 0 implies ( (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) by ;
reconsider WT = while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))) as InitHalting good Program of SCM+FSA by ;
per cases ( m - (s . (intloc (5 + 1))) > 0 or m - (s . (intloc (5 + 1))) <= 0 ) ;
suppose A9: m - (s . (intloc (5 + 1))) > 0 ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . () = b1 . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( x1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . ()) . ((k + 1) - x1) & b3 >= n . (intloc (5 + 1)) ) ) & ( for i being Nat st b4 > (k + 1) - x1 & b4 < (k + 1) + 1 holds
ex x2 being Integer st
( b5 = (n . ()) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) )

thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . () by
.= (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . () by A7, A9, Th14
.= s . () by A4, A5, Lm16 ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . (intloc (2 + 1)) by
.= (Initialized (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s))) . (intloc (2 + 1)) by A7, A9, Th15
.= (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (2 + 1)) by SCMFSA_M:37
.= s . (intloc (2 + 1)) by A4, A5, Lm16 ; :: thesis: ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )

A10: (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1)) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . (intloc (3 + 1)) by
.= (Initialized (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s))) . (intloc (3 + 1)) by A7, A9, Th15
.= s . (intloc (3 + 1)) by ;
now :: thesis: ex n being Element of NAT ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )
take n = 0 ; :: thesis: ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

take x1 = m; :: thesis: ( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) by A10; :: thesis: ( n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus n <= k + 1 ; :: thesis: ( ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) by ; :: thesis: for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )

thus for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) by INT_1:7; :: thesis: verum
end;
hence ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ; :: thesis: verum
end;
suppose A11: m - (s . (intloc (5 + 1))) <= 0 ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . () = b1 . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,b1)) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( x1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . ()) . ((k + 1) - x1) & b3 >= n . (intloc (5 + 1)) ) ) & ( for i being Nat st b4 > (k + 1) - x1 & b4 < (k + 1) + 1 holds
ex x2 being Integer st
( b5 = (n . ()) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) )

(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (1 + 1)) < k + 1 by ;
then A12: (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (1 + 1)) <= len (s . ()) by ;
A13: (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . () = s . () by A4, A5, Lm16;
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . () by
.= s . () by A2, A3, A8, A11, A13, A12 ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . (intloc (2 + 1)) by
.= (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (2 + 1)) by A2, A3, A8, A11, A13, A12
.= s . (intloc (2 + 1)) by A4, A5, Lm16 ; :: thesis: ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )

hereby :: thesis: verum
per cases ( k <> 0 or k = 0 ) ;
suppose k <> 0 ; :: thesis: ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )

then consider n being Nat, x1 being Integer such that
A14: n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . (intloc (3 + 1))) - ((IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (3 + 1))) and
A15: n <= k and
A16: ( k - n >= 1 implies ( x1 = ((IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . ()) . (k - n) & x1 >= (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (5 + 1)) ) ) and
A17: for i being Nat st i > k - n & i < k + 1 holds
ex x2 being Integer st
( x2 = ((IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . ()) . i & x2 <= (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (5 + 1)) ) by A2, A3, A8, A11, A13, A12;
A18: (IExec (WT,P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + (1 + n) by A3, A8, A11, A14, Th17;
now :: thesis: ex n1 being set ex y1 being Integer st
( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . ()) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )
take n1 = 1 + n; :: thesis: ex y1 being Integer st
( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . ()) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

take y1 = x1; :: thesis: ( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . ()) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) by A18; :: thesis: ( n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . ()) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus n1 <= k + 1 by ; :: thesis: ( ( (k + 1) - n1 >= 1 implies ( y1 = (s . ()) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus ( (k + 1) - n1 >= 1 implies ( y1 = (s . ()) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) by A4, A5, A16, Lm16; :: thesis: for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )

now :: thesis: for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )
let i be Nat; :: thesis: ( i > (k + 1) - n1 & i < (k + 1) + 1 implies ex x2 being Integer st
( b2 = (s . ()) . x2 & b2 <= s . (intloc (5 + 1)) ) )

assume that
A19: i > (k + 1) - n1 and
A20: i < (k + 1) + 1 ; :: thesis: ex x2 being Integer st
( b2 = (s . ()) . x2 & b2 <= s . (intloc (5 + 1)) )

per cases ( i = k + 1 or i <> k + 1 ) ;
suppose A21: i = k + 1 ; :: thesis: ex x2 being Integer st
( b2 = (s . ()) . x2 & b2 <= s . (intloc (5 + 1)) )

take x2 = m; :: thesis: ( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )
thus x2 = (s . ()) . i by A3, A6, A21; :: thesis: x2 <= s . (intloc (5 + 1))
x2 <= 0 + (s . (intloc (5 + 1))) by ;
hence x2 <= s . (intloc (5 + 1)) ; :: thesis: verum
end;
suppose A22: i <> k + 1 ; :: thesis: ex x2 being Integer st
( b2 = (s . ()) . x2 & b2 <= s . (intloc (5 + 1)) )

i <= k + 1 by ;
then i < k + 1 by ;
then consider y2 being Integer such that
A23: y2 = ((IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . ()) . i and
A24: y2 <= (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (5 + 1)) by ;
take x2 = y2; :: thesis: ( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )
thus x2 = (s . ()) . i by A4, A5, A23, Lm16; :: thesis: x2 <= s . (intloc (5 + 1))
thus x2 <= s . (intloc (5 + 1)) by A4, A5, A24, Lm16; :: thesis: verum
end;
end;
end;
hence for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ; :: thesis: verum
end;
hence ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ; :: thesis: verum
end;
suppose A25: k = 0 ; :: thesis: ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )

A26: (IExec (WT,P,s)) . (intloc (3 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,(IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)))) . (intloc (3 + 1)) by
.= (Initialized (IExec (((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s))) . (intloc (3 + 1)) by A3, A7, A8, A25, Th15
.= (s . (intloc (3 + 1))) + 1 by ;
now :: thesis: ex n1 being Element of NAT ex x1 being Element of NAT st
( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . ()) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )
take n1 = 1; :: thesis: ex x1 being Element of NAT st
( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . ()) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

take x1 = 0 ; :: thesis: ( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . ()) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) by A26; :: thesis: ( n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . ()) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus n1 <= k + 1 by A25; :: thesis: ( ( (k + 1) - n1 >= 1 implies ( x1 = (s . ()) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) )

thus ( (k + 1) - n1 >= 1 implies ( x1 = (s . ()) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) by A25; :: thesis: for i being Nat st i > (k + 1) - n1 & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )

hereby :: thesis: verum
let i be Nat; :: thesis: ( i > (k + 1) - n1 & i < (k + 1) + 1 implies ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) )

assume that
A27: i > (k + 1) - n1 and
A28: i < (k + 1) + 1 ; :: thesis: ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )

take x2 = m; :: thesis: ( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) )
A29: i >= 0 + 1 by ;
i <= 1 by ;
hence x2 = (s . ()) . i by ; :: thesis: x2 <= s . (intloc (5 + 1))
x2 <= 0 + (s . (intloc (5 + 1))) by ;
hence x2 <= s . (intloc (5 + 1)) ; :: thesis: verum
end;
end;
hence ( k + 1 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . ()) . ((k + 1) - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A30: S1[ 0 ]
proof
let s be State of SCM+FSA; :: thesis: ( s . (intloc (1 + 1)) = 0 & s . (intloc (1 + 1)) <= len (s . ()) implies ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = s . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . ()) . (0 - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > 0 - n & i < 0 + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ) )

set s0 = Initialized s;
assume that
A31: s . (intloc (1 + 1)) = 0 and
s . (intloc (1 + 1)) <= len (s . ()) ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = s . () & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . ()) . (0 - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > 0 - n & i < 0 + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () = s . () by ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . ()) . (0 - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > 0 - n & i < 0 + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) = () . (intloc (2 + 1)) by
.= s . (intloc (2 + 1)) by SCMFSA_M:37 ; :: thesis: ( 0 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . ()) . (0 - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > 0 - n & i < 0 + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )

thus ( 0 = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . ()) . (0 - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > 0 - n & i < 0 + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A30, A1);
hence for k being Nat
for s being State of SCM+FSA st s . (intloc (1 + 1)) = k & s . (intloc (1 + 1)) <= len (s . ()) holds
( s . () = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () & s . (intloc (2 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) & ( k = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . ()) . (k - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > k - n & i < k + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ) ; :: thesis: verum