defpred S1[ Element of 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 )))))),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 )))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( $1 = 0 or 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 )))))),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 Element of 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:
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 )))))),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 )))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or 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 )))))),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 Element of 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 =
Initialize s;
assume A2:
(
s . (intloc (1 + 1)) = 0 &
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 )))))),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 )))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or 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 )))))),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 Element of NAT st i > 0 - n & i < 0 + 1 holds
ex x2 being Integer st
( x2 = (s . (fsloc 0 )) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )
hence
(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 )))))),s) . (fsloc 0 ) = s . (fsloc 0 )
by Th34;
:: 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 )))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or 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 )))))),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 Element of 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 )))))),s) . (intloc (5 + 1)) =
(Initialize s) . (intloc (5 + 1))
by A2, Th35
.=
s . (intloc (5 + 1))
by SCMFSA6C:3
;
:: 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( 0 = 0 or 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 )))))),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 Element of 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 )))))),s) . (intloc (2 + 1)) =
(Initialize s) . (intloc (2 + 1))
by A2, Th35
.=
s . (intloc (2 + 1))
by SCMFSA6C:3
;
:: thesis: ( 0 = 0 or 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 )))))),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 Element of 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
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 )))))),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
Element of
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;
A3:
now let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )assume A4:
S1[
k]
;
:: thesis: S1[k + 1]now 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 )))))),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 )))))),b1) . (intloc (5 + 1)) = b1 . (intloc (5 + 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 )))))),b1) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Element of 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 )))))),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 Element of 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 A5:
(
s . (intloc (1 + 1)) = k + 1 &
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 )))))),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 )))))),b1) . (intloc (5 + 1)) = b1 . (intloc (5 + 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 )))))),b1) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Element of 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 )))))),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 Element of 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)) ) ) ) ) )then A6:
s . (intloc (1 + 1)) >= 1
+ 0
by INT_1:20;
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 ))))),
s;
set bs0 =
Initialize (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 ))))),s);
consider m being
Integer such that A7:
(
m = (s . (fsloc 0 )) . (s . (intloc (1 + 1))) & (
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 ))))),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 ))))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) ) & (
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 ))))),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 ))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) )
by A5, A6, Lm16;
per cases
( m - (s . (intloc (5 + 1))) > 0 or m - (s . (intloc (5 + 1))) <= 0 )
;
suppose A8:
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 )))))),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 )))))),b1) . (intloc (5 + 1)) = b1 . (intloc (5 + 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 )))))),b1) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Element of 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 )))))),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 Element of 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 )))))),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 )))))),(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 ))))),s)) . (fsloc 0 )
by A5, Lm5, Th36
.=
(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 ))))),s) . (fsloc 0 )
by A7, A8, Th34
.=
s . (fsloc 0 )
by A5, A6, 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 )))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or 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 )))))),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 Element of 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 )))))),s) . (intloc (5 + 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 )))))),(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 ))))),s)) . (intloc (5 + 1))
by A5, Lm5, Th37
.=
(Initialize (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 ))))),s)) . (intloc (5 + 1))
by A7, A8, Th35
.=
(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 ))))),s) . (intloc (5 + 1))
by SCMFSA6C:3
.=
s . (intloc (5 + 1))
by A5, A6, 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or 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 )))))),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 Element of 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 )))))),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 )))))),(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 ))))),s)) . (intloc (2 + 1))
by A5, Lm5, Th37
.=
(Initialize (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 ))))),s)) . (intloc (2 + 1))
by A7, A8, Th35
.=
(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 ))))),s) . (intloc (2 + 1))
by SCMFSA6C:3
.=
s . (intloc (2 + 1))
by A5, A6, Lm16
;
:: thesis: ( k + 1 = 0 or 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 )))))),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 Element of 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)) ) ) ) )A9:
(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 )))))),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 )))))),(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 ))))),s)) . (intloc (3 + 1))
by A5, Lm5, Th37
.=
(Initialize (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 ))))),s)) . (intloc (3 + 1))
by A7, A8, Th35
.=
s . (intloc (3 + 1))
by A7, A8, SCMFSA6C:3
;
now 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 )))))),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 Element of 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 )))))),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 Element of 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 )))))),s) . (intloc (3 + 1))) - (s . (intloc (3 + 1)))
by A9;
:: 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 Element of 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 Element of 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 A5, A7, A8, XREAL_1:21;
:: thesis: for i being Element of 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
Element of
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:20;
:: thesis: verum end; hence
(
k + 1
= 0 or 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 )))))),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
Element of
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 A10:
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 )))))),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 )))))),b1) . (intloc (5 + 1)) = b1 . (intloc (5 + 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 )))))),b1) . (intloc (2 + 1)) = b1 . (intloc (2 + 1)) & ( k + 1 = 0 or ex n being Element of 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 )))))),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 Element of 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)) ) ) ) ) )A11:
(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 ))))),s) . (fsloc 0 ) = s . (fsloc 0 )
by A5, A6, Lm16;
(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 ))))),s) . (intloc (1 + 1)) < k + 1
by A5, A7, XREAL_1:31;
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 ))))),s) . (intloc (1 + 1)) <= len (s . (fsloc 0 ))
by A5, 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 ))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 1))
by A5, A6, 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 )))))),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 )))))),(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 ))))),s)) . (fsloc 0 )
by A5, Lm5, Th36
.=
s . (fsloc 0 )
by A4, A5, A7, A10, A11, 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 )))))),s) . (intloc (5 + 1)) = s . (intloc (5 + 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or 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 )))))),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 Element of 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 )))))),s) . (intloc (5 + 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 )))))),(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 ))))),s)) . (intloc (5 + 1))
by A5, Lm5, Th37
.=
s . (intloc (5 + 1))
by A4, A5, A7, A10, A11, A12, A13
;
:: 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 )))))),s) . (intloc (2 + 1)) = s . (intloc (2 + 1)) & ( k + 1 = 0 or 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 )))))),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 Element of 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 )))))),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 )))))),(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 ))))),s)) . (intloc (2 + 1))
by A5, Lm5, Th37
.=
(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 ))))),s) . (intloc (2 + 1))
by A4, A5, A7, A10, A11, A12
.=
s . (intloc (2 + 1))
by A5, A6, Lm16
;
:: thesis: ( k + 1 = 0 or 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 )))))),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 Element of 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 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 )))))),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 Element of 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
Element of
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 )))))),(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 ))))),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 ))))),s) . (intloc (3 + 1))) &
n <= k & (
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 ))))),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 ))))),s) . (intloc (5 + 1)) ) ) & ( for
i being
Element of
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 ))))),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 ))))),s) . (intloc (5 + 1)) ) ) )
by A4, A5, A7, A10, A11, A12;
A15:
(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 )))))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + (1 + n)
by A5, A7, A10, A14, Lm5, Th37;
now 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 )))))),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 Element of 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 )))))),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 Element of 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 )))))),s) . (intloc (3 + 1))) - (s . (intloc (3 + 1)))
by A15;
:: thesis: ( n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0 )) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Element of 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 A14, XREAL_1:8;
:: thesis: ( ( (k + 1) - n1 >= 1 implies ( y1 = (s . (fsloc 0 )) . ((k + 1) - n1) & y1 >= s . (intloc (5 + 1)) ) ) & ( for i being Element of 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 A5, A6, A14, Lm16;
:: thesis: for i being Element of 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 let i be
Element of
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 A16:
(
i > (k + 1) - n1 &
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 A18:
i <> k + 1
;
:: thesis: ex x2 being Integer st
( b2 = (s . (fsloc 0 )) . x2 & b2 <= s . (intloc (5 + 1)) )
i <= k + 1
by A16, INT_1:20;
then
i < k + 1
by A18, XXREAL_0:1;
then consider y2 being
Integer such that A19:
(
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 ))))),s) . (fsloc 0 )) . i &
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 ))))),s) . (intloc (5 + 1)) )
by A14, A16;
take x2 =
y2;
:: thesis: ( x2 = (s . (fsloc 0 )) . i & x2 <= s . (intloc (5 + 1)) )thus
x2 = (s . (fsloc 0 )) . i
by A5, A6, A19, Lm16;
:: thesis: x2 <= s . (intloc (5 + 1))thus
x2 <= s . (intloc (5 + 1))
by A5, A6, A19, Lm16;
:: thesis: verum end; end; hence
for
i being
Element of
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
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 )))))),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
Element of
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 A20:
k = 0
;
:: thesis: ( k + 1 = 0 or 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 )))))),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 Element of 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)) ) ) ) )A21:
(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 )))))),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 )))))),(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 ))))),s)) . (intloc (3 + 1))
by A5, Lm5, Th37
.=
(Initialize (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 ))))),s)) . (intloc (3 + 1))
by A5, A7, A20, Th35
.=
(s . (intloc (3 + 1))) + 1
by A7, A10, SCMFSA6C:3
;
now 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 )))))),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 Element of 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 )))))),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 Element of 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 )))))),s) . (intloc (3 + 1))) - (s . (intloc (3 + 1)))
by A21;
:: thesis: ( n1 <= k + 1 & ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0 )) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Element of 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 A20;
:: thesis: ( ( (k + 1) - n1 >= 1 implies ( x1 = (s . (fsloc 0 )) . ((k + 1) - n1) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Element of 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 A20;
:: thesis: for i being Element of 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)) ) end; hence
(
k + 1
= 0 or 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 )))))),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
Element of
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; hence
S1[
k + 1]
;
:: thesis: verum end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A1, A3);
hence
for k being Element of 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 )))))),s) . (fsloc 0 ) & s . (intloc (5 + 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 )))))),s) . (intloc (5 + 1)) & 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 )))))),s) . (intloc (2 + 1)) & ( k = 0 or 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 )))))),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 Element of 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