let s be State of SCM+FSA ; :: thesis: ( s . (intloc (0 + 1)) = (len (s . (fsloc 0 ))) - 1 implies ( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 ) ) )
assume A1: s . (intloc (0 + 1)) = (len (s . (fsloc 0 ))) - 1 ; :: thesis: ( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 ) )
reconsider t14 = ((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 )) as good InitHalting Program of SCM+FSA ;
reconsider t16 = (t14 ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1))) as good InitHalting Program of SCM+FSA ;
reconsider Wt = while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))) as good InitHalting Program of SCM+FSA by Lm4, Th30;
A2: t16 ';' Wt is good InitHalting Program of SCM+FSA ;

per cases ( len (s . (fsloc 0 )) <= 1 or len (s . (fsloc 0 )) > 1 ) ;

suppose A3: len (s . (fsloc 0 )) <= 1 ; :: thesis: ( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 ) )

then (len (s . (fsloc 0 ))) - 1 <= 0 by XREAL_1:49;
hence s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 A1, Lm11, SCM_HALT:80; :: thesis: for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2

now

let i, j be Element of NAT ; :: thesis: ( i >= 1 & j <= len (s . (fsloc 0 )) implies not i < j )
assume A4: ( i >= 1 & j <= len (s . (fsloc 0 )) & i < j ) ; :: thesis: contradiction
then ( j <= 1 & i < j ) by A3, XXREAL_0:2;
hence contradiction by A4, XXREAL_0:2; :: thesis: verum

end;

hence for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 ; :: thesis: verum

end;

suppose A5: len (s . (fsloc 0 )) > 1 ; :: thesis: ( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 ) )

defpred S₁[ Element of NAT ] means for t being State of SCM+FSA st t . (intloc (0 + 1)) = $1 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0 ))) - 1 & ( for i, j being Element of NAT st i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j holds
x1 >= x2 ) holds
( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) );
A6: S₁[ 0 ]

proof

let t be State of SCM+FSA ; :: thesis: ( t . (intloc (0 + 1)) = 0 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0 ))) - 1 & ( for i, j being Element of NAT st i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j holds
x1 >= x2 ) implies ( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) ) )
assume A7: ( t . (intloc (0 + 1)) = 0 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0 ))) - 1 ) ; :: thesis: ( ex i, j being Element of NAT st
( i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j & ex x1, x2 being Integer st
( x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j & not x1 >= x2 ) ) or ( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) ) )
then (IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) = t . (fsloc 0 ) by Lm11, SCM_HALT:80;
hence ( ex i, j being Element of NAT st
( i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j & ex x1, x2 being Integer st
( x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j & not x1 >= x2 ) ) or ( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) ) ) by A7; :: thesis: verum

end;

A8: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A9: S₁[k] ; :: thesis: S₁[k + 1]

now

let t be State of SCM+FSA ; :: thesis: ( t . (intloc (0 + 1)) = k + 1 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0 ))) - 1 & ( for i, j being Element of NAT st i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j holds
x1 >= x2 ) implies ( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) ) )
assume A10: ( t . (intloc (0 + 1)) = k + 1 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0 ))) - 1 ) ; :: thesis: ( ( for i, j being Element of NAT st i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j holds
x1 >= x2 ) implies ( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) ) )
set B1 = SubFrom (intloc (0 + 1)),(intloc 0 );
set IB = IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t;
A11: (IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (intloc (0 + 1)) = (k + 1) - 1 by A10, Lm9, Lm11, SCM_HALT:79
.= k ;
set IW = IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t;
set ts = IExec t16,t;
A12: (IExec t16,t) . (fsloc 0 ) = t . (fsloc 0 ) by Lm20;
A13: (IExec t16,t) . (intloc (1 + 1)) = (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) by Lm20;
len (t . (fsloc 0 )) < (len (t . (fsloc 0 ))) + (t . (intloc (0 + 1))) by A10, XREAL_1:31;
then A14: (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) < ((len (t . (fsloc 0 ))) + (t . (intloc (0 + 1)))) - (t . (intloc (0 + 1))) by XREAL_1:11;
then A15: (IExec t16,t) . (intloc (1 + 1)) <= len ((IExec t16,t) . (fsloc 0 )) by A13, Lm20;
- ((len (t . (fsloc 0 ))) - 1) <= - (t . (intloc (0 + 1))) by A10, XREAL_1:26;
then A16: (len (t . (fsloc 0 ))) + (- ((len (t . (fsloc 0 ))) - 1)) <= (len (t . (fsloc 0 ))) + (- (t . (intloc (0 + 1)))) by XREAL_1:8;
then reconsider k1 = (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) as Element of NAT by INT_1:16;
A17: (IExec t16,t) . (intloc (1 + 1)) = k1 by Lm20;
consider n being Element of NAT , x1 being Integer such that
A18: ( n = ((IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),(IExec t16,t)) . (intloc (3 + 1))) - ((IExec t16,t) . (intloc (3 + 1))) & n <= k1 & ( k1 - n >= 1 implies ( x1 = ((IExec t16,t) . (fsloc 0 )) . (k1 - n) & x1 >= (IExec t16,t) . (intloc (5 + 1)) ) ) & ( for i being Element of NAT st i > k1 - n & i < k1 + 1 holds
ex x2 being Integer st
( x2 = ((IExec t16,t) . (fsloc 0 )) . i & x2 <= (IExec t16,t) . (intloc (5 + 1)) ) ) ) by A13, A15, A16, Lm17;
A19: (IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (fsloc 0 ) = (IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),(IExec t16,t)) . (fsloc 0 ) by Lm5, SCM_HALT:31
.= t . (fsloc 0 ) by A12, A14, A17, Lm17 ;
A20: (IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ) = (Exec (SubFrom (intloc (0 + 1)),(intloc 0 )),(IExec (((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))),t)) . (fsloc 0 ) by Lm11, SCM_HALT:34
.= (IExec (((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))),t) . (fsloc 0 ) by SCMFSA_2:91
.= (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 (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t)) . (fsloc 0 ) by A2, Lm10, SCM_HALT:31 ;
A21: (IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (intloc (3 + 1)) = n + ((IExec t16,t) . (intloc (3 + 1))) by A18, Lm5, SCM_HALT:30
.= n + 0 by Lm20
.= n ;
A22: (IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (intloc (2 + 1)) = (IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),(IExec t16,t)) . (intloc (2 + 1)) by Lm5, SCM_HALT:30
.= (IExec t16,t) . (intloc (2 + 1)) by A12, A14, A17, Lm17
.= k1 + 1 by Lm20 ;
A23: k1 < k1 + 1 by XREAL_1:31;
then A24: n < k1 + 1 by A18, XXREAL_0:2;
A25: n < (IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (intloc (2 + 1)) by A18, A22, A23, XXREAL_0:2;
A26: n - n < (k1 + 1) - n by A24, XREAL_1:11;
A27: ((len (t . (fsloc 0 ))) - (t . (intloc (0 + 1)))) + 1 <= len (t . (fsloc 0 )) by A14, INT_1:20;
A28: (IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (intloc (2 + 1)) <= len ((IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (fsloc 0 )) by A14, A19, A22, INT_1:20;
A29: 1 + 0 <= k1 + 1 by INT_1:20;
A30: abs (k1 + 1) = k1 + 1 by ABSVALUE:def 1;
reconsider n3 = (t . (fsloc 0 )) . (k1 + 1) as Integer ;
A31: (IExec t16,t) . (intloc (5 + 1)) = (t . (fsloc 0 )) /. (k1 + 1) by A30, Lm20
.= n3 by A27, A29, FINSEQ_4:24 ;
then A32: ( k1 - n >= 1 implies ( x1 = (t . (fsloc 0 )) . (k1 - n) & x1 >= n3 ) ) by A18, Lm20;
set mm = (k1 + 1) - n;
A33: ((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 (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t)) . (fsloc 0 )) . ((k1 + 1) - n) = ((IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (fsloc 0 )) . (k1 + 1) by A19, A21, A22, A24, A27, Lm19;
A34: (IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (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 (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t)) . (fsloc 0 ) are_fiberwise_equipotent by A19, A21, A22, A24, A27, Lm19;
(IExec (t16 ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))),t) . (fsloc 0 ),(IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ) are_fiberwise_equipotent by A19, A20, A21, A22, A25, A27, Lm19;
then A35: len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) = len (t . (fsloc 0 )) by A19, RFINSEQ:16;
(IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (intloc (0 + 1)) < t . (intloc (0 + 1)) by A10, A11, XREAL_1:31;
then A36: (IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (intloc (0 + 1)) <= (len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ))) - 1 by A10, A35, XXREAL_0:2;

hereby :: thesis: verum

assume A37: for i, j being Element of NAT st i >= 1 & j <= (len (t . (fsloc 0 ))) - (t . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (t . (fsloc 0 )) . i & x2 = (t . (fsloc 0 )) . j holds
x1 >= x2 ; :: thesis: ( t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 ) )

A38: now

let i, j be Element of NAT ; :: thesis: ( i >= 1 & j <= (len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ))) - ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (intloc (0 + 1))) & i < j implies for y1, y2 being Integer st y1 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . i & y2 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . j holds
b₅ >= b₆ )
assume A39: ( i >= 1 & j <= (len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ))) - ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (intloc (0 + 1))) & i < j ) ; :: thesis: for y1, y2 being Integer st y1 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . i & y2 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . j holds
b₅ >= b₆
let y1, y2 be Integer; :: thesis: ( y1 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . i & y2 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . j implies b₃ >= b₄ )
assume A40: ( y1 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . i & y2 = ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) . j ) ; :: thesis: b₃ >= b₄
(len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ))) - ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (intloc (0 + 1))) = k1 + 1 by A10, A11, A35;
then A41: j - 1 <= k1 by A39, XREAL_1:22;
A42: 1 <= j by A39, XXREAL_0:2;
A43: (k1 + 1) - n <= (k1 + 1) - 0 by XREAL_1:15;
then (k1 - n) + 1 <= k1 + 1 ;
then A44: k1 - n <= k1 by XREAL_1:8;
A45: 1 - 1 <= i - 1 by A39, XREAL_1:11;
then reconsider i1 = i - 1 as Element of NAT by INT_1:16;
A46: i - 1 < j - 1 by A39, XREAL_1:11;
then reconsider j1 = j - 1 as Element of NAT by A45, INT_1:16;

per cases ( i < (k1 + 1) - n or i > (k1 + 1) - n or i = (k1 + 1) - n ) by XXREAL_0:1;

suppose A47: i < (k1 + 1) - n ; :: thesis: b₃ >= b₄

then A48: y1 = (t . (fsloc 0 )) . i by A19, A20, A21, A22, A24, A28, A39, A40, Lm19;

hereby :: thesis: verum

per cases ( j < (k1 + 1) - n or j > (k1 + 1) - n or j = (k1 + 1) - n ) by XXREAL_0:1;

suppose A49: j < (k1 + 1) - n ; :: thesis: y1 >= y2

then j < k1 + 1 by A43, XXREAL_0:2;
then A50: j <= k1 by INT_1:20;
y2 = (t . (fsloc 0 )) . j by A19, A20, A21, A22, A24, A28, A40, A42, A49, Lm19;
hence y1 >= y2 by A37, A39, A48, A50; :: thesis: verum

end;

suppose A51: j > (k1 + 1) - n ; :: thesis: y1 >= y2

then ((k1 + 1) - n) + 1 <= j by INT_1:20;
then (k1 + 1) - n <= j1 by XREAL_1:21;
then A52: i < j1 by A47, XXREAL_0:2;
y2 = (t . (fsloc 0 )) . j1 by A10, A11, A19, A20, A21, A22, A24, A28, A35, A39, A40, A51, Lm19;
hence y1 >= y2 by A37, A39, A41, A48, A52; :: thesis: verum

end;

suppose A53: j = (k1 + 1) - n ; :: thesis: y1 >= y2

then A54: y2 = (t . (fsloc 0 )) . (k1 + 1) by A19, A20, A21, A22, A25, A27, A40, Lm19;
A55: i < (k1 - n) + 1 by A47;
then A56: i <= k1 - n by INT_1:20;

hereby :: thesis: verum

reconsider kn = k1 - n as Element of NAT by A55, INT_1:16, INT_1:20;
A57: (t . (fsloc 0 )) . kn = x1 by A18, A39, A56, Lm20, XXREAL_0:2;

per cases ( i = kn or i <> kn ) ;

suppose i = kn ; :: thesis: y1 >= y2

hence y1 >= y2 by A18, A19, A20, A21, A22, A24, A27, A31, A39, A40, A47, A54, A57, Lm19; :: thesis: verum

end;

suppose i <> kn ; :: thesis: y1 >= y2

then i < kn by A56, XXREAL_0:1;
then y1 >= x1 by A32, A37, A39, A44, A48, XXREAL_0:2;
hence y1 >= y2 by A18, A19, A20, A31, A33, A39, A40, A53, A56, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A58: i > (k1 + 1) - n ; :: thesis: b₃ >= b₄

i <= k1 + 1 by A10, A11, A35, A39, XXREAL_0:2;
then A59: y1 = (t . (fsloc 0 )) . i1 by A19, A20, A21, A22, A24, A28, A40, A58, Lm19;
(k1 + 1) - n < j by A39, A58, XXREAL_0:2;
then A60: y2 = (t . (fsloc 0 )) . j1 by A10, A11, A19, A20, A21, A22, A24, A28, A35, A39, A40, Lm19;
((k1 + 1) - n) + 1 <= i by A58, INT_1:20;
then 0 < i1 by A26, XREAL_1:21;
then 1 + 0 <= i1 by INT_1:20;
hence y1 >= y2 by A37, A41, A46, A59, A60; :: thesis: verum

end;

suppose A61: i = (k1 + 1) - n ; :: thesis: b₃ >= b₄

then A62: y2 = (t . (fsloc 0 )) . j1 by A10, A11, A19, A20, A21, A22, A25, A28, A35, A39, A40, Lm19;
k1 < k1 + 1 by XREAL_1:31;
then A63: j1 < k1 + 1 by A41, XXREAL_0:2;
((k1 + 1) - n) - 1 < j1 by A39, A61, XREAL_1:11;
then consider yy being Integer such that
A64: ( yy = (t . (fsloc 0 )) . j1 & yy <= n3 ) by A12, A18, A31, A63;
thus y1 >= y2 by A19, A20, A21, A22, A25, A28, A40, A61, A62, A64, Lm19; :: thesis: verum

end;

end;

end;

then A65: ( (IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t)) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t)) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t)) . (fsloc 0 )) . j holds
x1 >= x2 ) ) by A9, A11, A36;
A66: (IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) = (IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t)) . (fsloc 0 ) by A10, Lm9, Lm11, SCM_HALT:82;
hence t . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 ) are_fiberwise_equipotent by A19, A20, A34, A65, CLASSES1:84; :: thesis: for i, j being Element of NAT st i >= 1 & j <= len (t . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2
let i, j be Element of NAT ; :: thesis: ( i >= 1 & j <= len (t . (fsloc 0 )) & i < j implies for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2 )
assume A67: ( i >= 1 & j <= len (t . (fsloc 0 )) & i < j ) ; :: thesis: for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j holds
x1 >= x2
let x1, x2 be Integer; :: thesis: ( x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j implies x1 >= x2 )
assume A68: ( x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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))))))),t) . (fsloc 0 )) . j ) ; :: thesis: x1 >= x2
j <= len ((IExec ((((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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)))))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),t) . (fsloc 0 )) by A19, A20, A34, A67, RFINSEQ:16;
hence x1 >= x2 by A9, A11, A36, A38, A66, A67, A68; :: thesis: verum

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

1 - 1 < (len (s . (fsloc 0 ))) - 1 by A5, XREAL_1:11;
then reconsider m = (len (s . (fsloc 0 ))) - 1 as Element of NAT by INT_1:16;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A6, A8);
then A69: S₁[m] ;
then A70: ( ( for i, j being Element of NAT st i >= 1 & j <= (len (s . (fsloc 0 ))) - (s . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (s . (fsloc 0 )) . i & x2 = (s . (fsloc 0 )) . j holds
x1 >= x2 ) implies ( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 ) ) ) by A1;
A71: for i, j being Element of NAT st i >= 1 & j <= (len (s . (fsloc 0 ))) - (s . (intloc (0 + 1))) & i < j holds
for x1, x2 being Integer st x1 = (s . (fsloc 0 )) . i & x2 = (s . (fsloc 0 )) . j holds
x1 >= x2 by A1, XXREAL_0:2;
thus s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 A1, A70, XXREAL_0:2; :: thesis: for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2
thus for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (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 )) . j holds
x1 >= x2 by A1, A69, A71; :: thesis: verum

end;

end;