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 . (fsloc 0)) holds
( s . (fsloc 0) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) & s . (intloc (2 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . 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 . (fsloc 0)) holds
( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = s . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= $1 & ( $1 - n >= 1 implies ( x1 = (s . (fsloc 0)) . ($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 . (fsloc 0)) . 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 . (fsloc 0)) holds
( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = s . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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 . (fsloc 0)) implies ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,b1)) . (fsloc 0) = b1 . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . (fsloc 0)) . ((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 . (fsloc 0)) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) ) )
assume that
A3: s . (intloc (1 + 1)) = k + 1 and
A4: s . (intloc (1 + 1)) <= len (s . (fsloc 0)) ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,b1)) . (fsloc 0) = b1 . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . (fsloc 0)) . ((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 . (fsloc 0)) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) )
set bs = IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s);
set bs0 = Initialized (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s));
A5: s . (intloc (1 + 1)) >= 1 + 0 by A3, INT_1:7;
then consider m being Integer such that
A6: m = (s . (fsloc 0)) . (s . (intloc (1 + 1))) and
A7: ( m - (s . (intloc (5 + 1))) > 0 implies ( (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (1 + 1)) = 0 & (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) and
A8: ( m - (s . (intloc (5 + 1))) <= 0 implies ( (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 & (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) by A4, Lm16;
reconsider WT = while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))))) as InitHalting good Program of SCM+FSA by Lm4, Th11;
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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,b1)) . (fsloc 0) = b1 . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . (fsloc 0)) . ((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 . (fsloc 0)) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) )
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (fsloc 0) by A3, Th16
.= (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (fsloc 0) by A7, A9, Th14
.= s . (fsloc 0) by A4, A5, Lm16 ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (2 + 1)) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (intloc (2 + 1)) by A3, Th17
.= (Initialized (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s))) . (intloc (2 + 1)) by A7, A9, Th15
.= (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )
A10: (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1)) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (intloc (3 + 1)) by A3, Th17
.= (Initialized (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s))) . (intloc (3 + 1)) by A7, A9, Th15
.= s . (intloc (3 + 1)) by A7, A9, SCMFSA_M:37 ;
now :: thesis: ex n being Element of NAT ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
take x1 = m; :: thesis: ( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) by A10; :: thesis: ( n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus n <= k + 1 ; :: thesis: ( ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((k + 1) - n) & x1 >= 0 + (s . (intloc (5 + 1))) ) ) by A3, A6, A9, XREAL_1:19; :: thesis: for i being Nat st i > (k + 1) - n & i < (k + 1) + 1 holds
ex x2 being Integer st
( x2 = (s . (fsloc 0)) . 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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,b1)) . (fsloc 0) = b1 . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,n)) . (intloc (3 + 1))) - (n . (intloc (3 + 1))) & x1 <= k + 1 & ( (k + 1) - x1 >= 1 implies ( b3 = (n . (fsloc 0)) . ((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 . (fsloc 0)) . x2 & b5 <= n . (intloc (5 + 1)) ) ) ) ) )
(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (1 + 1)) < k + 1 by A3, A7, A8, XREAL_1:29;
then A12: (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (1 + 1)) <= len (s . (fsloc 0)) by A3, A4, XXREAL_0:2;
A13: (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (fsloc 0) = s . (fsloc 0) by A4, A5, Lm16;
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (fsloc 0) by A3, Th16
.= s . (fsloc 0) by A2, A3, A8, A11, A13, A12 ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (2 + 1)) = (IExec (WT,P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (intloc (2 + 1)) by A3, Th17
.= (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (intloc (3 + 1))) - ((IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (3 + 1))) and
A15: n <= k and
A16: ( k - n >= 1 implies ( x1 = ((IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (fsloc 0)) . (k - n) & x1 >= (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (fsloc 0)) . i & x2 <= (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
take y1 = x1; :: thesis: ( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) by A18; :: thesis: ( n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus n1 <= k + 1 by A15, XREAL_1:6; :: thesis: ( ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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 . (fsloc 0)) . 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 . (fsloc 0)) . 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 . (fsloc 0)) . 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 . (fsloc 0)) . x2 & b2 <= s . (intloc (5 + 1)) )
take x2 = m; :: thesis: ( x2 = (s . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) )
thus x2 = (s . (fsloc 0)) . i by A3, A6, A21; :: thesis: x2 <= s . (intloc (5 + 1))
x2 <= 0 + (s . (intloc (5 + 1))) by A11, XREAL_1:20;
hence x2 <= s . (intloc (5 + 1)) ; :: thesis: verum
end;
suppose A22: i <> k + 1 ; :: thesis: ex x2 being Integer st
( b2 = (s . (fsloc 0)) . x2 & b2 <= s . (intloc (5 + 1)) )
i <= k + 1 by A20, INT_1:7;
then i < k + 1 by A22, XXREAL_0:1;
then consider y2 being Integer such that
A23: y2 = ((IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (fsloc 0)) . i and
A24: y2 <= (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)) . (intloc (5 + 1)) by A17, A19;
take x2 = y2; :: thesis: ( x2 = (s . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) )
thus x2 = (s . (fsloc 0)) . 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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) )
A26: (IExec (WT,P,s)) . (intloc (3 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,(IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s)))) . (intloc (3 + 1)) by A3, Th17
.= (Initialized (IExec (((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))),P,s))) . (intloc (3 + 1)) by A3, A7, A8, A25, Th15
.= (s . (intloc (3 + 1))) + 1 by A8, A11, SCMFSA_M:37 ;
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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
take x1 = 0 ; :: thesis: ( n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus n1 = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) by A26; :: thesis: ( n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus n1 <= k + 1 by A25; :: thesis: ( ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) )
thus ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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 . (fsloc 0)) . 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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) )
take x2 = m; :: thesis: ( x2 = (s . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) )
A29: i >= 0 + 1 by A27, INT_1:7;
i <= 1 by A25, A28, INT_1:7;
hence x2 = (s . (fsloc 0)) . i by A3, A6, A25, A29, XXREAL_0:1; :: thesis: x2 <= s . (intloc (5 + 1))
x2 <= 0 + (s . (intloc (5 + 1))) by A11, XREAL_1:20;
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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k + 1 & ( (k + 1) - n >= 1 implies ( x1 = (s . (fsloc 0)) . ((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 . (fsloc 0)) . 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 . (fsloc 0)) implies ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = s . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . 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 . (fsloc 0)) ; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = s . (fsloc 0) & (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) = s . (fsloc 0) by A31, Th14; :: thesis: ( (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
thus (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (2 + 1)) = (Initialized s) . (intloc (2 + 1)) by A31, Th15
.= 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . 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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= 0 & ( 0 - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . 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 . (fsloc 0)) holds
( s . (fsloc 0) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (fsloc 0) & s . (intloc (2 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),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)) := ((fsloc 0),(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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . (fsloc 0)) . (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 . (fsloc 0)) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) ) ; :: thesis: verum