let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA holds
( s . (fsloc 0),(IExec ((insert-sort (fsloc 0)),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 ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j holds
x1 >= x2 ) )
let s be State of SCM+FSA; ( s . (fsloc 0),(IExec ((insert-sort (fsloc 0)),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 ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,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 = Initialized s;
set s1 = Exec (((intloc (1 + 1)) := (intloc 0)),(Initialized s));
set s2 = IExec ((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))),P,s);
set s3 = IExec (((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))) ";" ((intloc (3 + 1)) := (intloc 0))),P,s);
set s4 = IExec ((((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))) ";" ((intloc (3 + 1)) := (intloc 0))) ";" ((intloc (4 + 1)) := (intloc 0))),P,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))),P,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))),P,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)))),P,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))),P,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))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
(IExec ((((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))) ";" ((intloc (3 + 1)) := (intloc 0))) ";" ((intloc (4 + 1)) := (intloc 0))),P,s)) . (fsloc 0)
by SCMFSA_2:63
.=
(Exec (((intloc (4 + 1)) := (intloc 0)),(IExec (((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))) ";" ((intloc (3 + 1)) := (intloc 0))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
(IExec (((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))) ";" ((intloc (3 + 1)) := (intloc 0))),P,s)) . (fsloc 0)
by SCMFSA_2:63
.=
(Exec (((intloc (3 + 1)) := (intloc 0)),(IExec ((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
(IExec ((((intloc (1 + 1)) := (intloc 0)) ";" ((intloc (2 + 1)) := (intloc 0))),P,s)) . (fsloc 0)
by SCMFSA_2:63
.=
(Exec (((intloc (2 + 1)) := (intloc 0)),(Exec (((intloc (1 + 1)) := (intloc 0)),(Initialized s))))) . (fsloc 0)
by SCMFSA6C:9
.=
(Exec (((intloc (1 + 1)) := (intloc 0)),(Initialized s))) . (fsloc 0)
by SCMFSA_2:63
.=
(Initialized s) . (fsloc 0)
by SCMFSA_2:63
.=
s . (fsloc 0)
by SCMFSA_M:37
;
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))),P,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))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A1, SCMFSA_2:74
;
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)))),P,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))),P,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A2, SCMFSA_2:65
;
A4:
(IExec ((insert-sort (fsloc 0)),P,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,(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)))),P,s)))) . (fsloc 0)
by Lm12, SCM_HALT:21;
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))),P,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))),P,s)))) . (intloc (0 + 1))
by SCMFSA6C:6
.=
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)))),P,s)) . (fsloc 0))
by A1, A3, SCMFSA_2:74
;
A6: (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)))),P,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))),P,s)))) . (intloc (0 + 1))
by SCMFSA6C:6
.=
((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))),P,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))),P,s)) . (intloc 0))
by SCMFSA_2:65
.=
(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)))),P,s)) . (fsloc 0))) - 1
by A5, SCM_HALT:9
;
hence
s . (fsloc 0),(IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0) are_fiberwise_equipotent
by A3, A4, Lm21; for i, j being Nat st i >= 1 & j <= len (s . (fsloc 0)) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j holds
x1 >= x2
let i, j be Nat; ( i >= 1 & j <= len (s . (fsloc 0)) & i < j implies for x1, x2 being Integer st x1 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j holds
x1 >= x2 )
assume that
A7:
i >= 1
and
A8:
j <= len (s . (fsloc 0))
and
A9:
i < j
; for x1, x2 being Integer st x1 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j holds
x1 >= x2
thus
for x1, x2 being Integer st x1 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j holds
x1 >= x2
by A3, A6, A4, A7, A8, A9, Lm21; verum