set m1 = Macro (SubFrom (intloc 2),(intloc 2));
set m2 = AddTo (intloc 4),(intloc 0 );
set m3 = SubFrom (intloc 2),(intloc 0 );
set IF = if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )));
let f be FinSeq-Location ; card (insert-sort f) = 82
set i1 = (intloc 2) := (intloc 3);
set i2 = SubFrom (intloc 3),(intloc 0 );
set i3 = (intloc 5) := f,(intloc 2);
set i4 = (intloc 6) := f,(intloc 3);
set i5 = f,(intloc 2) := (intloc 6);
set i6 = f,(intloc 3) := (intloc 5);
set body3 = ((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5));
A1: card (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) =
((card (Macro (SubFrom (intloc 2),(intloc 2)))) + (card ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))) + 4
by SCMFSA8B:15
.=
(2 + (card ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))) + 4
by SCMFSA7B:6
.=
(2 + ((card (Macro (AddTo (intloc 4),(intloc 0 )))) + (card (Macro (SubFrom (intloc 2),(intloc 0 )))))) + 4
by SCMFSA6A:61
.=
(2 + (2 + (card (Macro (SubFrom (intloc 2),(intloc 0 )))))) + 4
by SCMFSA7B:6
.=
(2 + (2 + 2)) + 4
by SCMFSA7B:6
.=
10
;
set n1 = (intloc 5) := f,(intloc 2);
set n2 = SubFrom (intloc 5),(intloc 6);
set body2 = (((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))));
A2: card ((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))) =
(card (((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6)))) + (card (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SCMFSA6A:61
.=
((card (Macro ((intloc 5) := f,(intloc 2)))) + (card (Macro (SubFrom (intloc 5),(intloc 6))))) + (card (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SCMFSA6A:61
.=
(2 + (card (Macro (SubFrom (intloc 5),(intloc 6))))) + (card (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SCMFSA7B:6
.=
(2 + 2) + 10
by A1, SCMFSA7B:6
.=
14
;
set WM = (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ));
set j1 = (intloc 1) :=len f;
set j2 = SubFrom (intloc 1),(intloc 0 );
set T3 = Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)));
set t1 = (intloc 2) :=len f;
set t2 = SubFrom (intloc 2),(intloc 1);
set t3 = (intloc 3) := (intloc 2);
set t4 = AddTo (intloc 3),(intloc 0 );
set t5 = (intloc 6) := f,(intloc 3);
set t6 = SubFrom (intloc 4),(intloc 4);
set Wg = while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))));
set t16 = ((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4));
set body1 = ((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))))) ';' (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5))));
A3: card (((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5))) =
(card ((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6)))) + (card (Macro (f,(intloc 3) := (intloc 5))))
by SCMFSA6A:61
.=
10 + (card (Macro (f,(intloc 3) := (intloc 5))))
by Th41
.=
10 + 2
by SCMFSA7B:6
.=
12
;
A4: card (((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))))) ';' (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5))))) =
(card ((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))))) + (card (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))
by SCMFSA6A:61
.=
((card (((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4)))) + (card (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))))) + (card (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))
by SCMFSA6A:61
.=
(((card ((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3)))) + (card (Macro (SubFrom (intloc 4),(intloc 4))))) + (card (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))))) + (card (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))
by SCMFSA6A:61
.=
((10 + (card (Macro (SubFrom (intloc 4),(intloc 4))))) + (card (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))))) + (card (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))
by Th41
.=
((10 + 2) + (card (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))))) + (card (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))
by SCMFSA7B:6
.=
((10 + 2) + (14 + 6)) + (card (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))
by A2, SCMFSA_9:5
.=
((10 + 2) + (14 + 6)) + (12 + 12)
by A3, SCMBSORT:44
.=
56
;
thus card (insert-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)) ';' (SubFrom (intloc 1),(intloc 0 )))) + (card (Times (intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))))) ';' (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))))
by SCMFSA6A:61
.=
(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)) ';' (SubFrom (intloc 1),(intloc 0 )))) + (56 + 12)
by A4, SCMBSORT:44
.=
((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 (Macro (SubFrom (intloc 1),(intloc 0 ))))) + (56 + 12)
by SCMFSA6A:61
.=
((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))) + 2) + (56 + 12)
by SCMFSA7B:6
.=
(((card ((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 )))) + (card (Macro ((intloc 1) :=len f)))) + 2) + (56 + 12)
by SCMFSA6A:61
.=
(((card ((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 )))) + 2) + 2) + (56 + 12)
by SCMFSA7B:6
.=
((10 + 2) + 2) + 68
by Th41
.=
82
; verum