let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA holds
( s . (),(IExec ((),P,s)) . () are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . ()) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2 ) )

let s be State of SCM+FSA; :: thesis: ( s . (),(IExec ((),P,s)) . () are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . ()) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2 ) )

set WJ = (((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()));
set s0 = Initialized s;
set s1 = Exec (((intloc (1 + 1)) := ()),());
set s2 = IExec ((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())),P,s);
set s3 = IExec (((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())),P,s);
set s4 = IExec ((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())),P,s);
set s5 = IExec (((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())),P,s);
set s6 = IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s);
set s7 = IExec (((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()))),P,s);
A1: (IExec (((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())),P,s)) . () = (Exec (((intloc (5 + 1)) := ()),(IExec ((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())),P,s)))) . () by SCMFSA6C:7
.= (IExec ((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())),P,s)) . () by SCMFSA_2:63
.= (Exec (((intloc (4 + 1)) := ()),(IExec (((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())),P,s)))) . () by SCMFSA6C:7
.= (IExec (((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())),P,s)) . () by SCMFSA_2:63
.= (Exec (((intloc (3 + 1)) := ()),(IExec ((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())),P,s)))) . () by SCMFSA6C:7
.= (IExec ((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())),P,s)) . () by SCMFSA_2:63
.= (Exec (((intloc (2 + 1)) := ()),(Exec (((intloc (1 + 1)) := ()),())))) . () by SCMFSA6C:9
.= (Exec (((intloc (1 + 1)) := ()),())) . () by SCMFSA_2:63
.= () . () by SCMFSA_2:63
.= s . () by SCMFSA_M:37 ;
A2: (IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s)) . () = (Exec (((intloc (0 + 1)) :=len ()),(IExec (((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())),P,s)))) . () by SCMFSA6C:7
.= s . () by ;
A3: (IExec (((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()))),P,s)) . () = (Exec ((SubFrom ((intloc (0 + 1)),())),(IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s)))) . () by SCMFSA6C:7
.= s . () by ;
A4: (IExec ((),P,s)) . () = (IExec ((Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))))))),P,(IExec (((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()))),P,s)))) . () by ;
A5: (IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s)) . (intloc (0 + 1)) = (Exec (((intloc (0 + 1)) :=len ()),(IExec (((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())),P,s)))) . (intloc (0 + 1)) by SCMFSA6C:6
.= len ((IExec (((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()))),P,s)) . ()) by ;
A6: (IExec (((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()))),P,s)) . (intloc (0 + 1)) = (Exec ((SubFrom ((intloc (0 + 1)),())),(IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s)))) . (intloc (0 + 1)) by SCMFSA6C:6
.= ((IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s)) . (intloc (0 + 1))) - ((IExec ((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())),P,s)) . ()) by SCMFSA_2:65
.= (len ((IExec (((((((((intloc (1 + 1)) := ()) ";" ((intloc (2 + 1)) := ())) ";" ((intloc (3 + 1)) := ())) ";" ((intloc (4 + 1)) := ())) ";" ((intloc (5 + 1)) := ())) ";" ((intloc (0 + 1)) :=len ())) ";" (SubFrom ((intloc (0 + 1)),()))),P,s)) . ())) - 1 by ;
hence s . (),(IExec ((),P,s)) . () are_fiberwise_equipotent by A3, A4, Lm21; :: thesis: for i, j being Nat st i >= 1 & j <= len (s . ()) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2

let i, j be Nat; :: thesis: ( i >= 1 & j <= len (s . ()) & i < j implies for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2 )

assume that
A7: i >= 1 and
A8: j <= len (s . ()) and
A9: i < j ; :: thesis: for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2

thus for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2 by A3, A6, A4, A7, A8, A9, Lm21; :: thesis: verum