let s be State of SCM+FSA ; ( s . (intloc (1 + 1)) >= 0 & s . (intloc (1 + 1)) < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0 )) implies ex k being Element of NAT st
( k <= s . (intloc (2 + 1)) & k >= (s . (intloc (2 + 1))) - (s . (intloc (1 + 1))) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),s) . (fsloc 0 )) . k = (s . (fsloc 0 )) . (s . (intloc (2 + 1))) ) )
assume that
A1:
s . (intloc (1 + 1)) >= 0
and
A2:
s . (intloc (1 + 1)) < s . (intloc (2 + 1))
and
A3:
s . (intloc (2 + 1)) <= len (s . (fsloc 0 ))
; ex k being Element of NAT st
( k <= s . (intloc (2 + 1)) & k >= (s . (intloc (2 + 1))) - (s . (intloc (1 + 1))) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),s) . (fsloc 0 )) . k = (s . (fsloc 0 )) . (s . (intloc (2 + 1))) )
defpred S1[ Nat] means for t being State of SCM+FSA st t . (intloc (1 + 1)) = $1 & t . (intloc (1 + 1)) < t . (intloc (2 + 1)) & t . (intloc (2 + 1)) <= len (t . (fsloc 0 )) holds
( ( for m being Element of NAT st m > t . (intloc (2 + 1)) & m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m ) & ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - $1 & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) ) );
A4:
S1[ 0 ]
proof
let t be
State of
SCM+FSA ;
( t . (intloc (1 + 1)) = 0 & t . (intloc (1 + 1)) < t . (intloc (2 + 1)) & t . (intloc (2 + 1)) <= len (t . (fsloc 0 )) implies ( ( for m being Element of NAT st m > t . (intloc (2 + 1)) & m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m ) & ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - 0 & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) ) ) )
assume that A5:
t . (intloc (1 + 1)) = 0
and A6:
t . (intloc (1 + 1)) < t . (intloc (2 + 1))
and
t . (intloc (2 + 1)) <= len (t . (fsloc 0 ))
;
( ( for m being Element of NAT st m > t . (intloc (2 + 1)) & m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m ) & ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - 0 & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) ) )
set If0 =
(IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 );
thus
for
m being
Element of
NAT st
m > t . (intloc (2 + 1)) &
m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m
by A5, SCM_HALT:80;
ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - 0 & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )
reconsider n =
t . (intloc (2 + 1)) as
Element of
NAT by A5, A6, INT_1:16;
take
n
;
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - 0 & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )
thus
n <= t . (intloc (2 + 1))
;
( n >= (t . (intloc (2 + 1))) - 0 & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )
thus
n >= (t . (intloc (2 + 1))) - 0
;
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1)))
thus
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1)))
by A5, SCM_HALT:80;
verum
end;
set sb2 = SubFrom (intloc (1 + 1)),(intloc 0 );
A7:
now let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )assume A8:
S1[
k]
;
S1[k + 1]now let t be
State of
SCM+FSA ;
( t . (intloc (1 + 1)) = k + 1 & t . (intloc (1 + 1)) < t . (intloc (2 + 1)) & t . (intloc (2 + 1)) <= len (t . (fsloc 0 )) implies ( ( for m being Element of NAT st m > t . (intloc (2 + 1)) & m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m ) & ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) ) ) )assume that A9:
t . (intloc (1 + 1)) = k + 1
and A10:
t . (intloc (1 + 1)) < t . (intloc (2 + 1))
and A11:
t . (intloc (2 + 1)) <= len (t . (fsloc 0 ))
;
( ( for m being Element of NAT st m > t . (intloc (2 + 1)) & m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m ) & ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) ) )set t1 =
IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),
t;
set IB =
IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),
t;
set t2 =
IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t);
A12:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (1 + 1)) =
(Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t)) . (intloc (1 + 1))
by SCM_HALT:33
.=
((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (intloc (1 + 1))) - ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (intloc 0 ))
by SCMFSA_2:91
.=
((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (intloc (1 + 1))) - 1
by SCM_HALT:17
.=
((Initialize t) . (intloc (1 + 1))) - 1
by Lm22, SCM_HALT:63
.=
(t . (intloc (1 + 1))) - 1
by SCMFSA6C:3
;
A13:
2
<= k + 2
by NAT_1:11;
(k + 1) + 1
<= t . (intloc (2 + 1))
by A9, A10, INT_1:20;
then A14:
2
<= t . (intloc (2 + 1))
by A13, XXREAL_0:2;
A15:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1)) =
(Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t)) . (intloc (2 + 1))
by SCM_HALT:33
.=
(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (intloc (2 + 1))
by Lm10, SCMFSA_2:91
.=
(t . (intloc (2 + 1))) - 1
by A11, A14, Lm29
;
A16:
(t . (intloc (1 + 1))) - 1
< (t . (intloc (2 + 1))) - 1
by A10, XREAL_1:11;
A17:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (1 + 1)) < (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1))
by A10, A12, A15, XREAL_1:11;
A18:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 ) =
(Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t)) . (fsloc 0 )
by SCM_HALT:34
.=
(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 )
by SCMFSA_2:91
;
A19:
t . (fsloc 0 ),
(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 ) are_fiberwise_equipotent
by A11, A14, Lm29;
then A20:
len (t . (fsloc 0 )) = len ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 ))
by A18, RFINSEQ:16;
then A21:
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1)) <= len ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 ))
by A11, A15, XREAL_1:148, XXREAL_0:2;
A22:
(IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 ) = (IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t)) . (fsloc 0 )
by A9, Lm22, SCM_HALT:82;
A23:
(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 ) =
(Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t)) . (fsloc 0 )
by SCMFSA_2:91
.=
(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 )
by SCM_HALT:34
;
thus
for
m being
Element of
NAT st
m > t . (intloc (2 + 1)) &
m <= len (t . (fsloc 0 )) holds
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m
ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )proof
let m be
Element of
NAT ;
( m > t . (intloc (2 + 1)) & m <= len (t . (fsloc 0 )) implies (t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m )
assume that A24:
m > t . (intloc (2 + 1))
and A25:
m <= len (t . (fsloc 0 ))
;
(t . (fsloc 0 )) . m = ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m
A26:
t . (intloc (2 + 1)) > (t . (intloc (2 + 1))) - 1
by XREAL_1:148;
A27:
m > (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1))
by A15, A24, XREAL_1:148, XXREAL_0:2;
A28:
m <= len ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 ))
by A18, A19, A25, RFINSEQ:16;
m >= 2
by A14, A24, XXREAL_0:2;
then
m >= 1
by XXREAL_0:2;
then
m in dom (t . (fsloc 0 ))
by A25, FINSEQ_3:27;
hence (t . (fsloc 0 )) . m =
((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . m
by A11, A14, A23, A24, A26, Lm29
.=
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m
by A8, A9, A12, A17, A21, A22, A27, A28
;
verum
end; hereby verum
reconsider n =
t . (intloc (2 + 1)) as
Element of
NAT by A9, A10, INT_1:16;
per cases
( (t . (fsloc 0 )) . (t . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 )) . (t . (intloc (2 + 1))) or (t . (fsloc 0 )) . (t . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 )) . ((t . (intloc (2 + 1))) - 1) )
by A11, A14, Lm29;
suppose A29:
(t . (fsloc 0 )) . (t . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 )) . (t . (intloc (2 + 1)))
;
ex n being Element of NAT st
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )take n =
n;
( n <= t . (intloc (2 + 1)) & n >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )thus
n <= t . (intloc (2 + 1))
;
( n >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )
n <= n + (k + 1)
by NAT_1:11;
hence
n >= (t . (intloc (2 + 1))) - (k + 1)
by XREAL_1:22;
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1)))thus
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . n = (t . (fsloc 0 )) . (t . (intloc (2 + 1)))
by A8, A9, A11, A12, A15, A16, A20, A21, A22, A23, A29, XREAL_1:148;
verum end; suppose A30:
(t . (fsloc 0 )) . (t . (intloc (2 + 1))) = ((IExec (((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))),t) . (fsloc 0 )) . ((t . (intloc (2 + 1))) - 1)
;
ex m being Element of NAT st
( m <= t . (intloc (2 + 1)) & m >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )consider m being
Element of
NAT such that A31:
m <= (IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1))
and A32:
m >= ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1))) - k
and A33:
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),(IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t)) . (fsloc 0 )) . m = ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . ((IExec ((((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA ))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),t) . (intloc (2 + 1)))
by A8, A9, A12, A17, A21;
take m =
m;
( m <= t . (intloc (2 + 1)) & m >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )thus
m <= t . (intloc (2 + 1))
by A15, A31, XREAL_1:148, XXREAL_0:2;
( m >= (t . (intloc (2 + 1))) - (k + 1) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m = (t . (fsloc 0 )) . (t . (intloc (2 + 1))) )thus
m >= (t . (intloc (2 + 1))) - (k + 1)
by A15, A32;
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m = (t . (fsloc 0 )) . (t . (intloc (2 + 1)))thus
((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),t) . (fsloc 0 )) . m = (t . (fsloc 0 )) . (t . (intloc (2 + 1)))
by A9, A15, A23, A30, A33, Lm22, SCM_HALT:82;
verum end;
end; end; hence
S1[
k + 1]
;
verum end;
A34:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A4, A7);
reconsider i = s . (intloc (1 + 1)) as Element of NAT by A1, INT_1:16;
S1[i]
by A34;
hence
ex k being Element of NAT st
( k <= s . (intloc (2 + 1)) & k >= (s . (intloc (2 + 1))) - (s . (intloc (1 + 1))) & ((IExec (Times (intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)))) ';' (SubFrom (intloc (5 + 1)),(intloc (4 + 1)))) ';' (if>0 (intloc (5 + 1)),((((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)))),(Stop SCM+FSA )))),s) . (fsloc 0 )) . k = (s . (fsloc 0 )) . (s . (intloc (2 + 1))) )
by A2, A3; verum