let f be FinSeq-Location ; card (bubble-sort f) = 63
set i1 = (intloc 4) := (intloc 3);
set i2 = SubFrom ((intloc 3),(intloc 0));
set i3 = (intloc 5) := (f,(intloc 3));
set i4 = (intloc 6) := (f,(intloc 4));
set i5 = SubFrom ((intloc 6),(intloc 5));
set i6 = (f,(intloc 3)) := (intloc 6);
set i7 = (f,(intloc 4)) := (intloc 5);
set ifc = if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA));
set Cif = card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)));
set body2 = ((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)));
card (Stop SCM+FSA) = 1
by COMPOS_1:4;
then A1: card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))) =
((card ((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5)))) + 1) + 4
by SCMFSA8B:12
.=
(6 + 1) + 4
by Th45
.=
11
;
A2: card (((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))) =
(card ((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5))))) + (card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SCMFSA6A:21
.=
(card (((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' (((intloc 6) := (f,(intloc 4))) ';' (SubFrom ((intloc 6),(intloc 5)))))) + (card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SCMFSA6A:28
.=
((card ((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3))))) + (card (((intloc 6) := (f,(intloc 4))) ';' (SubFrom ((intloc 6),(intloc 5)))))) + (card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SCMFSA6A:21
.=
(6 + (card (((intloc 6) := (f,(intloc 4))) ';' (SubFrom ((intloc 6),(intloc 5)))))) + (card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by Th45
.=
(6 + 4) + (card (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SCMFSA6A:35
.=
21
by A1
;
set j1 = (intloc 2) := (intloc 1);
set j2 = SubFrom ((intloc 2),(intloc 0));
set j3 = (intloc 3) :=len f;
set body1 = ((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))));
A3: card (((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))) =
(card ((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f))) + (card (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SCMFSA6A:21
.=
6 + (card (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by Th45
.=
6 + (21 + 12)
by A2, Th44
.=
39
;
set k2 = (intloc 2) := (intloc 0);
set k3 = (intloc 3) := (intloc 0);
set k4 = (intloc 4) := (intloc 0);
set k5 = (intloc 5) := (intloc 0);
set k6 = (intloc 6) := (intloc 0);
A4: card ((((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0))) =
(card (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0)))) + 2
by SCMFSA6A:34
.=
((card ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0)))) + 2) + 2
by SCMFSA6A:34
.=
(card ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0)))) + 4
.=
6 + 4
by Th45
.=
10
;
set k7 = (intloc 1) :=len f;
set Ct = card (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))));
A5:
card (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))) = 39 + 12
by A3, Th44;
thus card (bubble-sort f) =
(card (((((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0))) ';' ((intloc 1) :=len f))) + (card (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))
by SCMFSA6A:21
.=
(10 + 2) + (card (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))
by A4, SCMFSA6A:34
.=
63
by A5
; verum