let s be State of SCM+FSA ; :: thesis: ( s . (fsloc 0 ),(IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2 ) )
set WJ = (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ));
set s0 = Initialize s;
set s1 = Exec ((intloc (1 + 1)) := (intloc 0 )),(Initialize s);
set s2 = IExec (((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))),s;
set s3 = IExec ((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))),s;
set s4 = IExec (((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))),s;
set s5 = IExec ((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))),s;
set s6 = IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s;
set s7 = IExec ((((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),s;
A1: (IExec ((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))),s) . (fsloc 0 ) = (Exec ((intloc (5 + 1)) := (intloc 0 )),(IExec (((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= (IExec (((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))),s) . (fsloc 0 ) by SCMFSA_2:89
.= (Exec ((intloc (4 + 1)) := (intloc 0 )),(IExec ((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= (IExec ((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))),s) . (fsloc 0 ) by SCMFSA_2:89
.= (Exec ((intloc (3 + 1)) := (intloc 0 )),(IExec (((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= (IExec (((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))),s) . (fsloc 0 ) by SCMFSA_2:89
.= (Exec ((intloc (2 + 1)) := (intloc 0 )),(Exec ((intloc (1 + 1)) := (intloc 0 )),(Initialize s))) . (fsloc 0 ) by SCMFSA6C:10
.= (Exec ((intloc (1 + 1)) := (intloc 0 )),(Initialize s)) . (fsloc 0 ) by SCMFSA_2:89
.= (Initialize s) . (fsloc 0 ) by SCMFSA_2:89
.= s . (fsloc 0 ) by SCMFSA6C:3 ;
A2: (IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s) . (fsloc 0 ) = (Exec ((intloc (0 + 1)) :=len (fsloc 0 )),(IExec ((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= s . (fsloc 0 ) by A1, SCMFSA_2:100 ;
A3: (IExec ((((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),s) . (fsloc 0 ) = (Exec (SubFrom (intloc (0 + 1)),(intloc 0 )),(IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s)) . (fsloc 0 ) by SCMFSA6C:8
.= s . (fsloc 0 ) by A2, SCMFSA_2:91 ;
A4: (IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s) . (intloc (0 + 1)) = (Exec ((intloc (0 + 1)) :=len (fsloc 0 )),(IExec ((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))),s)) . (intloc (0 + 1)) by SCMFSA6C:7
.= len ((IExec ((((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),s) . (fsloc 0 )) by A1, A3, SCMFSA_2:100 ;
A5: (IExec ((((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),s) . (intloc (0 + 1)) = (Exec (SubFrom (intloc (0 + 1)),(intloc 0 )),(IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s)) . (intloc (0 + 1)) by SCMFSA6C:7
.= ((IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s) . (intloc (0 + 1))) - ((IExec (((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))),s) . (intloc 0 )) by SCMFSA_2:91
.= (len ((IExec ((((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),s) . (fsloc 0 ))) - 1 by A4, SCM_HALT:17 ;
A6: (IExec (insert-sort (fsloc 0 )),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))))))),(IExec ((((((((intloc (1 + 1)) := (intloc 0 )) ';' ((intloc (2 + 1)) := (intloc 0 ))) ';' ((intloc (3 + 1)) := (intloc 0 ))) ';' ((intloc (4 + 1)) := (intloc 0 ))) ';' ((intloc (5 + 1)) := (intloc 0 ))) ';' ((intloc (0 + 1)) :=len (fsloc 0 ))) ';' (SubFrom (intloc (0 + 1)),(intloc 0 ))),s)) . (fsloc 0 ) by Lm12, SCM_HALT:31;
hence s . (fsloc 0 ),(IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 ) are_fiberwise_equipotent by A3, A5, Lm21; :: thesis: for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2
let i, j be Element of NAT ; :: thesis: ( i >= 1 & j <= len (s . (fsloc 0 )) & i < j implies for x1, x2 being Integer st x1 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2 )
assume ( i >= 1 & j <= len (s . (fsloc 0 )) & i < j ) ; :: thesis: for x1, x2 being Integer st x1 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2
hence for x1, x2 being Integer st x1 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2 by A3, A5, A6, Lm21; :: thesis: verum