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 InitHalting good Program of SCM+FSA ;
reconsider t16 = (t14 ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1)))) as good 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 InitHalting good Program of SCM+FSA by Lm4, Th11;
let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA st s . (intloc (0 + 1)) = (len (s . (fsloc 0))) - 1 holds
( 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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
let P be Instruction-Sequence of SCM+FSA; ( 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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) ) )
assume A1:
s . (intloc (0 + 1)) = (len (s . (fsloc 0))) - 1
; ( 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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
A2:
t16 ";" Wt is good Program of SCM+FSA
;
per cases
( len (s . (fsloc 0)) <= 1 or len (s . (fsloc 0)) > 1 )
;
suppose A3:
len (s . (fsloc 0)) <= 1
;
( 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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent
by A1, Lm11, SCM_HALT:67, XREAL_1:47;
for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2hence
for
i,
j being
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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2
;
verum end; suppose
len (s . (fsloc 0)) > 1
;
( 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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )then
1
- 1
< (len (s . (fsloc 0))) - 1
by XREAL_1:9;
then reconsider m =
(len (s . (fsloc 0))) - 1 as
Element of
NAT by INT_1:3;
defpred S1[
Nat]
means for
t being
State of
SCM+FSA for
Q being
Instruction-Sequence of
SCM+FSA st
t . (intloc (0 + 1)) = $1 &
t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1 & ( for
i,
j being
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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for
i,
j being
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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) );
A7:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A8:
S1[
k]
;
S1[k + 1]now for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA st t . (intloc (0 + 1)) = k + 1 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1 & ( for i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) )let t be
State of
SCM+FSA;
for Q being Instruction-Sequence of SCM+FSA st t . (intloc (0 + 1)) = k + 1 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1 & ( for i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) )let Q be
Instruction-Sequence of
SCM+FSA;
( t . (intloc (0 + 1)) = k + 1 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1 & ( for i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) ) )assume that A9:
t . (intloc (0 + 1)) = k + 1
and A10:
t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1
;
( ( for i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) ) )
len (t . (fsloc 0)) < (len (t . (fsloc 0))) + (t . (intloc (0 + 1)))
by A9, XREAL_1:29;
then A11:
(len (t . (fsloc 0))) - (t . (intloc (0 + 1))) < ((len (t . (fsloc 0))) + (t . (intloc (0 + 1)))) - (t . (intloc (0 + 1)))
by XREAL_1:9;
then A12:
((len (t . (fsloc 0))) - (t . (intloc (0 + 1)))) + 1
<= len (t . (fsloc 0))
by INT_1:7;
- ((len (t . (fsloc 0))) - 1) <= - (t . (intloc (0 + 1)))
by A10, XREAL_1:24;
then A13:
(len (t . (fsloc 0))) + (- ((len (t . (fsloc 0))) - 1)) <= (len (t . (fsloc 0))) + (- (t . (intloc (0 + 1))))
by XREAL_1:6;
then reconsider k1 =
(len (t . (fsloc 0))) - (t . (intloc (0 + 1))) as
Element of
NAT by INT_1:3;
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)))))))))),
Q,
t);
set ts =
IExec (
t16,
Q,
t);
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)))),
Q,
t);
A14:
(IExec (t16,Q,t)) . (fsloc 0) = t . (fsloc 0)
by Lm20;
A15:
(IExec (t16,Q,t)) . (intloc (1 + 1)) = (len (t . (fsloc 0))) - (t . (intloc (0 + 1)))
by Lm20;
then
(IExec (t16,Q,t)) . (intloc (1 + 1)) <= len ((IExec (t16,Q,t)) . (fsloc 0))
by A11, Lm20;
then consider n being
Nat,
x1 being
Integer such that A16:
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))))))))),Q,(IExec (t16,Q,t)))) . (intloc (3 + 1))) - ((IExec (t16,Q,t)) . (intloc (3 + 1)))
and A17:
n <= k1
and A18:
(
k1 - n >= 1 implies (
x1 = ((IExec (t16,Q,t)) . (fsloc 0)) . (k1 - n) &
x1 >= (IExec (t16,Q,t)) . (intloc (5 + 1)) ) )
and A19:
for
i being
Nat st
i > k1 - n &
i < k1 + 1 holds
ex
x2 being
Integer st
(
x2 = ((IExec (t16,Q,t)) . (fsloc 0)) . i &
x2 <= (IExec (t16,Q,t)) . (intloc (5 + 1)) )
by A15, A13, Lm17;
A20:
k1 < k1 + 1
by XREAL_1:29;
then A21:
n < k1 + 1
by A17, XXREAL_0:2;
then A22:
n - n < (k1 + 1) - n
by XREAL_1:9;
reconsider n3 =
(t . (fsloc 0)) . (k1 + 1) as
Integer ;
A23:
1
+ 0 <= k1 + 1
by INT_1:7;
A24:
(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)))),Q,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))))))),Q,t)))) . (fsloc 0)
by Lm11, SCM_HALT:24
.=
(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))))))),Q,t)) . (fsloc 0)
by SCMFSA_2:65
.=
(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)))))),Q,(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)))))))))),Q,t)))) . (fsloc 0)
by A2, Lm10, SCM_HALT:21
;
set mm =
(k1 + 1) - n;
|.(k1 + 1).| = k1 + 1
by ABSVALUE:def 1;
then A25:
(IExec (t16,Q,t)) . (intloc (5 + 1)) =
(t . (fsloc 0)) /. (k1 + 1)
by Lm20
.=
n3
by A12, A23, FINSEQ_4:15
;
then A26:
(
k1 - n >= 1 implies (
x1 = (t . (fsloc 0)) . (k1 - n) &
x1 >= n3 ) )
by A18, Lm20;
A27:
(IExec (t16,Q,t)) . (intloc (1 + 1)) = k1
by Lm20;
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)))))))))),Q,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))))))))),Q,(IExec (t16,Q,t)))) . (fsloc 0)
by Lm5, SCM_HALT:21
.=
t . (fsloc 0)
by A14, A11, A27, Lm17
;
A29:
(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)))))))))),Q,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))))))))),Q,(IExec (t16,Q,t)))) . (intloc (2 + 1))
by Lm5, SCM_HALT:20
.=
(IExec (t16,Q,t)) . (intloc (2 + 1))
by A14, A11, A27, Lm17
.=
k1 + 1
by Lm20
;
then A30:
(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)))))))))),Q,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)))))))))),Q,t)) . (fsloc 0))
by A11, A28, INT_1:7;
A31:
(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)))))))))),Q,t)) . (intloc (3 + 1)) =
n + ((IExec (t16,Q,t)) . (intloc (3 + 1)))
by A16, Lm5, SCM_HALT:20
.=
n + 0
by Lm20
.=
n
;
then A32:
(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)))))))))),Q,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)))))),Q,(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)))))))))),Q,t)))) . (fsloc 0) are_fiberwise_equipotent
by A28, A29, A21, A12, Lm19;
A33:
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)))))))))),Q,t)) . (intloc (2 + 1))
by A17, A29, A20, XXREAL_0:2;
then
(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)))))))))),Q,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)))),Q,t)) . (fsloc 0) are_fiberwise_equipotent
by A28, A24, A31, A29, A12, Lm19;
then A34:
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)))),Q,t)) . (fsloc 0)) = len (t . (fsloc 0))
by A28, RFINSEQ:3;
A35:
(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)))),Q,t)) . (intloc (0 + 1)) =
(k + 1) - 1
by A9, Lm9, Lm11, SCM_HALT:66
.=
k
;
then
(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)))),Q,t)) . (intloc (0 + 1)) < t . (intloc (0 + 1))
by A9, XREAL_1:29;
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)))),Q,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)))),Q,t)) . (fsloc 0))) - 1
by A10, A34, XXREAL_0:2;
A37:
((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)))))),Q,(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)))))))))),Q,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)))))))))),Q,t)) . (fsloc 0)) . (k1 + 1)
by A28, A31, A29, A21, A12, Lm19;
hereby verum
A38:
(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))))))))),Q,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))))))))),Q,(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)))),Q,t)))) . (fsloc 0)
by A9, Lm9, Lm11, SCM_HALT:69;
assume A39:
for
i,
j being
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
;
( 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) )A40:
now for i, j being 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)))),Q,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)))),Q,t)) . (intloc (0 + 1))) & i < j holds
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)))),Q,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)))),Q,t)) . (fsloc 0)) . j holds
y1 >= y2A41:
(k1 + 1) - n <= (k1 + 1) - 0
by XREAL_1:13;
then
(k1 - n) + 1
<= k1 + 1
;
then A42:
k1 - n <= k1
by XREAL_1:6;
let i,
j be
Nat;
( 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)))),Q,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)))),Q,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)))),Q,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)))),Q,t)) . (fsloc 0)) . j holds
b5 >= b6 )assume that A43:
i >= 1
and A44:
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)))),Q,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)))),Q,t)) . (intloc (0 + 1)))
and A45:
i < j
;
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)))),Q,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)))),Q,t)) . (fsloc 0)) . j holds
b5 >= b6A46:
1
<= j
by A43, A45, XXREAL_0:2;
(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)))),Q,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)))),Q,t)) . (intloc (0 + 1))) = k1 + 1
by A9, A35, A34;
then A47:
j - 1
<= k1
by A44, XREAL_1:20;
A48:
1
- 1
<= i - 1
by A43, XREAL_1:9;
then reconsider i1 =
i - 1 as
Element of
NAT by INT_1:3;
A49:
i - 1
< j - 1
by A45, XREAL_1:9;
then reconsider j1 =
j - 1 as
Element of
NAT by A48, INT_1:3;
let y1,
y2 be
Integer;
( 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)))),Q,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)))),Q,t)) . (fsloc 0)) . j implies b3 >= b4 )assume that A50:
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)))),Q,t)) . (fsloc 0)) . i
and A51:
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)))),Q,t)) . (fsloc 0)) . j
;
b3 >= b4per cases
( i < (k1 + 1) - n or i > (k1 + 1) - n or i = (k1 + 1) - n )
by XXREAL_0:1;
suppose A52:
i < (k1 + 1) - n
;
b3 >= b4then A53:
y1 = (t . (fsloc 0)) . i
by A28, A24, A31, A29, A21, A30, A43, A50, Lm19;
hereby verum
per cases
( j < (k1 + 1) - n or j > (k1 + 1) - n or j = (k1 + 1) - n )
by XXREAL_0:1;
suppose A54:
j < (k1 + 1) - n
;
y1 >= y2then
j < k1 + 1
by A41, XXREAL_0:2;
then A55:
j <= k1
by INT_1:7;
y2 = (t . (fsloc 0)) . j
by A28, A24, A31, A29, A21, A30, A51, A46, A54, Lm19;
hence
y1 >= y2
by A39, A43, A45, A53, A55;
verum end; suppose A56:
j > (k1 + 1) - n
;
y1 >= y2then
((k1 + 1) - n) + 1
<= j
by INT_1:7;
then
(k1 + 1) - n <= j1
by XREAL_1:19;
then A57:
i < j1
by A52, XXREAL_0:2;
y2 = (t . (fsloc 0)) . j1
by A9, A35, A28, A24, A31, A29, A21, A30, A34, A44, A51, A56, Lm19;
hence
y1 >= y2
by A39, A43, A47, A53, A57;
verum end; suppose A58:
j = (k1 + 1) - n
;
y1 >= y2A59:
i < (k1 - n) + 1
by A52;
then A60:
i <= k1 - n
by INT_1:7;
A61:
y2 = (t . (fsloc 0)) . (k1 + 1)
by A28, A24, A31, A29, A33, A12, A51, A58, Lm19;
hereby verum
reconsider kn =
k1 - n as
Element of
NAT by A59, INT_1:3, INT_1:7;
A62:
(t . (fsloc 0)) . kn = x1
by A18, A43, A60, Lm20, XXREAL_0:2;
per cases
( i = kn or i <> kn )
;
suppose
i = kn
;
y1 >= y2hence
y1 >= y2
by A18, A28, A24, A31, A29, A21, A12, A25, A43, A50, A52, A61, A62, Lm19;
verum end; suppose
i <> kn
;
y1 >= y2then
i < kn
by A60, XXREAL_0:1;
then
y1 >= x1
by A26, A39, A43, A42, A53, XXREAL_0:2;
hence
y1 >= y2
by A18, A28, A24, A25, A37, A43, A51, A58, A60, XXREAL_0:2;
verum end;
end; end; end; suppose A63:
i > (k1 + 1) - n
;
b3 >= b4then
((k1 + 1) - n) + 1
<= i
by INT_1:7;
then
0 < i1
by A22, XREAL_1:19;
then A64:
1
+ 0 <= i1
by INT_1:7;
(k1 + 1) - n < j
by A45, A63, XXREAL_0:2;
then A65:
y2 = (t . (fsloc 0)) . j1
by A9, A35, A28, A24, A31, A29, A21, A30, A34, A44, A51, Lm19;
i <= k1 + 1
by A9, A35, A34, A44, A45, XXREAL_0:2;
then
y1 = (t . (fsloc 0)) . i1
by A28, A24, A31, A29, A21, A30, A50, A63, Lm19;
hence
y1 >= y2
by A39, A47, A49, A65, A64;
verum end; suppose A66:
i = (k1 + 1) - n
;
b3 >= b4
k1 < k1 + 1
by XREAL_1:29;
then A67:
j1 < k1 + 1
by A47, XXREAL_0:2;
((k1 + 1) - n) - 1
< j1
by A45, A66, XREAL_1:9;
then A68:
ex
yy being
Integer st
(
yy = (t . (fsloc 0)) . j1 &
yy <= n3 )
by A14, A19, A25, A67;
y2 = (t . (fsloc 0)) . j1
by A9, A35, A28, A24, A31, A29, A33, A30, A34, A44, A45, A51, A66, Lm19;
hence
y1 >= y2
by A28, A24, A31, A29, A33, A30, A50, A66, A68, Lm19;
verum end; end; then
(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)))),Q,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))))))))),Q,(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)))),Q,t)))) . (fsloc 0) are_fiberwise_equipotent
by A8, A35, A36;
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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent
by A28, A24, A32, A38, CLASSES1:76;
for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2let i,
j be
Nat;
( 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 )assume that A69:
i >= 1
and A70:
j <= len (t . (fsloc 0))
and A71:
i < j
;
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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2let x1,
x2 be
Integer;
( 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j implies x1 >= x2 )assume that A72:
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))))))))),Q,t)) . (fsloc 0)) . i
and A73:
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))))))))),Q,t)) . (fsloc 0)) . j
;
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)))),Q,t)) . (fsloc 0))
by A28, A24, A32, A70, RFINSEQ:3;
hence
x1 >= x2
by A8, A35, A36, A40, A38, A69, A71, A72, A73;
verum
end; end; hence
S1[
k + 1]
;
verum end; A74:
S1[
0 ]
proof
let t be
State of
SCM+FSA;
for Q being Instruction-Sequence of SCM+FSA st t . (intloc (0 + 1)) = 0 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1 & ( for i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) )let Q be
Instruction-Sequence of
SCM+FSA;
( t . (intloc (0 + 1)) = 0 & t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1 & ( for i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) ) )
assume that A75:
t . (intloc (0 + 1)) = 0
and
t . (intloc (0 + 1)) <= (len (t . (fsloc 0))) - 1
;
( ex i, j being 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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for i, j being 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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= 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))))))))),Q,t)) . (fsloc 0) = t . (fsloc 0)
by A75, Lm11, SCM_HALT:67;
hence
( ex
i,
j being
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))))))))),Q,t)) . (fsloc 0) are_fiberwise_equipotent & ( for
i,
j being
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))))))))),Q,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))))))))),Q,t)) . (fsloc 0)) . j holds
x1 >= x2 ) ) )
by A75;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A74, A7);
then A76:
S1[
m]
;
then
( ( for
i,
j being
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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent & ( for
i,
j being
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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) ) )
by A1;
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))))))))),P,s)) . (fsloc 0) are_fiberwise_equipotent
by A1, XXREAL_0:2;
for i, j being 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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2
for
i,
j being
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;
hence
for
i,
j being
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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds
x1 >= x2
by A1, A76;
verum end;