defpred S1[ Element of NAT ] means for s being State of SCM+FSA st s . (intloc (3 + 1)) = $1 & $1 < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0)) holds
( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - $1 & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - $1) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - $1 < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - $1 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) );
A1:
now set s4 =
SubFrom (
(intloc (3 + 1)),
(intloc 0));
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )assume A2:
S1[
k]
;
S1[k + 1]now A3:
intloc (3 + 1) <> intloc (2 + 1)
by SCMFSA_2:128;
let s be
State of
SCM+FSA;
( s . (intloc (3 + 1)) = k + 1 & k + 1 < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0)) implies ( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - (k + 1) & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - (k + 1)) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - (k + 1) < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) ) )assume that A4:
s . (intloc (3 + 1)) = k + 1
and A5:
k + 1
< s . (intloc (2 + 1))
and A6:
s . (intloc (2 + 1)) <= len (s . (fsloc 0))
;
( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - (k + 1) & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - (k + 1)) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - (k + 1) < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )A7:
(k + 1) - 1
< (s . (intloc (2 + 1))) - 1
by A5, XREAL_1:11;
then reconsider n =
(s . (intloc (2 + 1))) - 1 as
Element of
NAT by INT_1:16;
A8:
n <= len (s . (fsloc 0))
by A6, XREAL_1:148, XXREAL_0:2;
set b3s =
IExec (
((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),
s);
set bds =
IExec (
(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),
s);
set ff =
s . (fsloc 0);
set gg =
(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0);
A9:
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (3 + 1)) =
(Exec ((SubFrom ((intloc (3 + 1)),(intloc 0))),(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)))) . (intloc (3 + 1))
by SCMFSA6C:7
.=
((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (intloc (3 + 1))) - ((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (intloc 0))
by SCMFSA_2:91
.=
((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (intloc (3 + 1))) - 1
by SCMFSA6B:35
.=
((Initialized s) . (intloc (3 + 1))) - 1
by Lm6, SCMFSA8C:91
.=
(k + 1) - 1
by A4, SCMFSA6C:3
.=
k
;
reconsider m =
s . (intloc (2 + 1)) as
Element of
NAT by A5, INT_1:16;
A10:
0 + 1
<= k + 1
by XREAL_1:8;
then A11:
1
<= m
by A5, XXREAL_0:2;
A12:
abs (s . (intloc (2 + 1))) = m
by ABSVALUE:def 1;
(k + 1) + 1
<= m
by A5, INT_1:20;
then
((k + 1) + 1) - 1
<= n
by XREAL_1:11;
then A13:
1
<= n
by A10, XXREAL_0:2;
A14:
(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) = (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0)
by A4, Lm6, SCM_HALT:82;
A15:
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1)) =
(Exec ((SubFrom ((intloc (3 + 1)),(intloc 0))),(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)))) . (intloc (2 + 1))
by SCMFSA6C:7
.=
(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (intloc (2 + 1))
by A3, SCMFSA_2:91
.=
(s . (intloc (2 + 1))) - 1
by Lm18
;
then A16:
((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1))) - k = (s . (intloc (2 + 1))) - (k + 1)
;
abs ((s . (intloc (2 + 1))) - 1) = n
by ABSVALUE:def 1;
then A17:
(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0) = ((s . (fsloc 0)) +* (m,((s . (fsloc 0)) /. n))) +* (
n,
((s . (fsloc 0)) /. m))
by A12, Lm18;
then A18:
(s . (fsloc 0)) . m = ((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0)) . n
by A6, A11, A13, A8, FUNCT_7:115;
A19:
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (fsloc 0) =
(Exec ((SubFrom ((intloc (3 + 1)),(intloc 0))),(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)))) . (fsloc 0)
by SCMFSA6C:8
.=
(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0)
by SCMFSA_2:91
;
then A20:
s . (fsloc 0),
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (fsloc 0) are_fiberwise_equipotent
by A6, A11, A13, A8, A17, FUNCT_7:115;
then A21:
n <= len ((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (fsloc 0))
by A8, RFINSEQ:16;
then
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (fsloc 0),
(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0) are_fiberwise_equipotent
by A2, A9, A15, A7;
hence
s . (fsloc 0),
(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent
by A20, A14, CLASSES1:84;
( (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - (k + 1) & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - (k + 1)) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - (k + 1) < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
s . (fsloc 0),
(IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0) are_fiberwise_equipotent
by A6, A11, A13, A8, A17, FUNCT_7:115;
then A22:
len (s . (fsloc 0)) = len ((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (fsloc 0))
by A19, RFINSEQ:16;
(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (intloc (2 + 1)) = ((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1))) - k
by A2, A9, A15, A7, A21;
hence
(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - (k + 1)
by A4, A15, Lm6, SCM_HALT:83;
( ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - (k + 1)) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - (k + 1) < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0)) . (((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1))) - k) = ((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (fsloc 0)) . ((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1)))
by A2, A9, A15, A7, A21;
hence
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - (k + 1)) = (s . (fsloc 0)) . (s . (intloc (2 + 1)))
by A4, A15, A19, A18, Lm6, SCM_HALT:82;
( ( for i being Element of NAT st (s . (intloc (2 + 1))) - (k + 1) < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )A23:
(s . (fsloc 0)) . n = ((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0)) . m
by A6, A11, A13, A8, A17, FUNCT_7:115;
hereby ( ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
let i be
Element of
NAT ;
( (s . (intloc (2 + 1))) - (k + 1) < i & i <= s . (intloc (2 + 1)) implies ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . b1 = (s . (fsloc 0)) . (b1 - 1) )assume that A24:
(s . (intloc (2 + 1))) - (k + 1) < i
and A25:
i <= s . (intloc (2 + 1))
;
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . b1 = (s . (fsloc 0)) . (b1 - 1)per cases
( i = s . (intloc (2 + 1)) or i <> s . (intloc (2 + 1)) )
;
suppose A26:
i = s . (intloc (2 + 1))
;
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . b1 = (s . (fsloc 0)) . (b1 - 1)then A27:
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1)) < i
by A15, XREAL_1:148;
thus ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i =
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0)) . i
by A4, Lm6, SCM_HALT:82
.=
(s . (fsloc 0)) . (i - 1)
by A2, A6, A9, A15, A7, A19, A8, A23, A22, A26, A27
;
verum end; suppose
i <> s . (intloc (2 + 1))
;
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . b1 = (s . (fsloc 0)) . (b1 - 1)then
i < s . (intloc (2 + 1))
by A25, XXREAL_0:1;
then A28:
i + 1
<= s . (intloc (2 + 1))
by INT_1:20;
then A29:
i <= (s . (intloc (2 + 1))) - 1
by XREAL_1:21;
A30:
i <= (IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1))
by A15, A28, XREAL_1:21;
((s . (intloc (2 + 1))) - (k + 1)) + 1
<= i
by A24, INT_1:20;
then A31:
(((s . (intloc (2 + 1))) - (k + 1)) + 1) - 1
<= i - 1
by XREAL_1:11;
A32:
(k + 1) - (k + 1) < (s . (intloc (2 + 1))) - (k + 1)
by A5, XREAL_1:11;
then reconsider i1 =
i - 1 as
Element of
NAT by A31, INT_1:16;
i - 1
< s . (intloc (2 + 1))
by A25, XREAL_1:148, XXREAL_0:2;
then A33:
i1 <= len (s . (fsloc 0))
by A6, XXREAL_0:2;
1
+ 0 <= (s . (intloc (2 + 1))) - (k + 1)
by A32, INT_1:20;
then
1
<= i - 1
by A31, XXREAL_0:2;
then A34:
i1 in dom (s . (fsloc 0))
by A33, FINSEQ_3:27;
A35:
i - 1
< i
by XREAL_1:148;
thus ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i =
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0)) . i
by A4, Lm6, SCM_HALT:82
.=
((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0)) . (i - 1)
by A2, A9, A7, A19, A8, A22, A16, A24, A30
.=
(s . (fsloc 0)) . (i - 1)
by A6, A11, A13, A8, A17, A25, A29, A35, A34, FUNCT_7:115
;
verum end;
end; hereby for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i
A36:
1
<= k + 1
by NAT_1:11;
let i be
Element of
NAT ;
( s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) implies ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i )assume that A37:
s . (intloc (2 + 1)) < i
and A38:
i <= len (s . (fsloc 0))
;
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . iA39:
n <> i
by A37, XREAL_1:148;
k + 1
< i
by A5, A37, XXREAL_0:2;
then
1
<= i
by A36, XXREAL_0:2;
then A40:
i in dom (s . (fsloc 0))
by A38, FINSEQ_3:27;
A41:
(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1)) < i
by A15, A37, XREAL_1:148, XXREAL_0:2;
thus ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i =
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0)) . i
by A4, Lm6, SCM_HALT:82
.=
((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0)) . i
by A2, A9, A15, A7, A19, A8, A22, A38, A41
.=
(s . (fsloc 0)) . i
by A6, A11, A13, A8, A17, A37, A39, A40, FUNCT_7:115
;
verum
end; hereby verum
let i be
Element of
NAT ;
( 1 <= i & i < (s . (intloc (2 + 1))) - (k + 1) implies ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i )assume that A42:
1
<= i
and A43:
i < (s . (intloc (2 + 1))) - (k + 1)
;
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . iA44:
((s . (intloc (2 + 1))) - 1) - k <= ((s . (intloc (2 + 1))) - 1) - 0
by XREAL_1:15;
then A45:
i <> m
by A43, XREAL_1:148, XXREAL_0:2;
i < (s . (intloc (2 + 1))) - 1
by A43, A44, XXREAL_0:2;
then
i < s . (intloc (2 + 1))
by XREAL_1:148, XXREAL_0:2;
then
i <= len (s . (fsloc 0))
by A6, XXREAL_0:2;
then A46:
i in dom (s . (fsloc 0))
by A42, FINSEQ_3:27;
A47:
i < ((IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)) . (intloc (2 + 1))) - k
by A15, A43;
thus ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i =
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),(IExec (((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))) ';' (SubFrom ((intloc (3 + 1)),(intloc 0)))),s)))) . (fsloc 0)) . i
by A4, Lm6, SCM_HALT:82
.=
((IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))),s)) . (fsloc 0)) . i
by A2, A9, A15, A7, A19, A8, A22, A42, A47
.=
(s . (fsloc 0)) . i
by A6, A11, A13, A8, A17, A43, A44, A45, A46, FUNCT_7:115
;
verum
end; end; hence
S1[
k + 1]
;
verum end;
A48:
S1[ 0 ]
proof
let s be
State of
SCM+FSA;
( s . (intloc (3 + 1)) = 0 & 0 < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0)) implies ( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 0 & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 0) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - 0 < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) ) )
assume that A49:
s . (intloc (3 + 1)) = 0
and
0 < s . (intloc (2 + 1))
and
s . (intloc (2 + 1)) <= len (s . (fsloc 0))
;
( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 0 & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 0) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - 0 < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
thus
s . (fsloc 0),
(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent
by A49, SCM_HALT:80;
( (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 0 & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 0) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - 0 < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
thus (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) =
(Initialized s) . (intloc (2 + 1))
by A49, SCM_HALT:81
.=
(s . (intloc (2 + 1))) - 0
by SCMFSA6C:3
;
( ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 0) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - 0 < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
thus
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - 0) = (s . (fsloc 0)) . (s . (intloc (2 + 1)))
by A49, SCM_HALT:80;
( ( for i being Element of NAT st (s . (intloc (2 + 1))) - 0 < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
thus
for
i being
Element of
NAT st
(s . (intloc (2 + 1))) - 0 < i &
i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1)
;
( ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
thus
for
i being
Element of
NAT st
s . (intloc (2 + 1)) < i &
i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i
by A49, SCM_HALT:80;
for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i
thus
for
i being
Element of
NAT st 1
<= i &
i < (s . (intloc (2 + 1))) - 0 holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i
by A49, SCM_HALT:80;
verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A48, A1);
hence
for k being Element of NAT
for s being State of SCM+FSA st s . (intloc (3 + 1)) = k & k < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0)) holds
( s . (fsloc 0),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0) are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - k & ((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . ((s . (intloc (2 + 1))) - k) = (s . (fsloc 0)) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - k < i & i <= s . (intloc (2 + 1)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0)) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - k holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))),s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) )
; verum