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 (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: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: 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 (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 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 )))))),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 (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)) ) ) ) ) )
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 = 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 ))))),s);
A5: s . (intloc (1 + 1)) >= 1 + 0 by A3, INT_1:20;
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 ))))),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)) ) ) 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 ))))),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 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 good InitHalting Program of SCM+FSA by Lm4, Th30;
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 )))))),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 (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 WT,(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 A3, 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, A9, Th34
.= 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 )))))),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 WT,(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 A3, Th37
.= (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 ))))),s)) . (intloc (2 + 1)) by A7, A9, 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 A4, A5, 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)) ) ) ) )
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 )))))),s) . (intloc (3 + 1)) = (IExec WT,(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 A3, Th37
.= (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 ))))),s)) . (intloc (3 + 1)) by A7, A9, Th35
.= s . (intloc (3 + 1)) by A7, A9, 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 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 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 A3, A6, A9, 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 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 )))))),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 (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)) ) ) ) ) )
(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 A3, A7, A8, 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 A3, A4, XXREAL_0:2;
A14: (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 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 )))))),s) . (fsloc 0 ) = (IExec WT,(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 A3, Th36
.= s . (fsloc 0 ) by A2, A3, A8, A11, A14, 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 (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 WT,(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 A3, 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 A2, A3, A8, A11, A14, A12
.= s . (intloc (2 + 1)) by A4, A5, 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
A15: 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))) and
A16: n <= k and
A17: ( 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)) ) ) and
A18: 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 A2, A3, A8, A11, A14, A12;
A19: (IExec WT,s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + (1 + n) by A3, A8, A11, A15, 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 A19; :: 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 A16, 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 A4, A5, A17, 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 that
A20: i > (k + 1) - n1 and
A21: 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 A22: 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, A22; :: thesis: x2 <= s . (intloc (5 + 1))
x2 <= 0 + (s . (intloc (5 + 1))) by A11, XREAL_1:22;
hence x2 <= s . (intloc (5 + 1)) ; :: thesis: verum
end;
suppose A23: i <> k + 1 ; :: thesis: ex x2 being Integer st
( b2 = (s . (fsloc 0 )) . x2 & b2 <= s . (intloc (5 + 1)) )
i <= k + 1 by A21, INT_1:20;
then i < k + 1 by A23, XXREAL_0:1;
then consider y2 being Integer such that
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 ))))),s) . (fsloc 0 )) . i and
A25: 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 A18, A20;
take x2 = y2; :: thesis: ( x2 = (s . (fsloc 0 )) . i & x2 <= s . (intloc (5 + 1)) )
thus x2 = (s . (fsloc 0 )) . i by A4, A5, A24, Lm16; :: thesis: x2 <= s . (intloc (5 + 1))
thus x2 <= s . (intloc (5 + 1)) by A4, A5, A25, Lm16; :: thesis: verum
end;
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 A26: 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)) ) ) ) )
A27: (IExec WT,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 A3, Th37
.= (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 ))))),s)) . (intloc (3 + 1)) by A3, A7, A8, A26, Th35
.= (s . (intloc (3 + 1))) + 1 by A8, A11, 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 A27; :: 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 A26; :: 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 A26; :: 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)) )
hereby :: thesis: verum
let i be Element of 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
A28: i > (k + 1) - n1 and
A29: 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)) )
A30: i >= 0 + 1 by A28, INT_1:20;
i <= 1 by A26, A29, INT_1:20;
hence x2 = (s . (fsloc 0 )) . i by A3, A6, A26, A30, XXREAL_0:1; :: thesis: x2 <= s . (intloc (5 + 1))
x2 <= 0 + (s . (intloc (5 + 1))) by A11, XREAL_1:22;
hence x2 <= s . (intloc (5 + 1)) ; :: thesis: verum
end;
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;
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A31: 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 (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 = Initialized s;
assume that
A32: 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 )))))),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 (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) . (fsloc 0 ) = s . (fsloc 0 ) by A32, 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 (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)) = (Initialized s) . (intloc (2 + 1)) by A32, 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;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A31, A1);
 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 (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