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 ; :: thesis: 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:12
.= (2 + (card ((AddTo ((intloc 4),(intloc 0))) ';' (SubFrom ((intloc 2),(intloc 0)))))) + 4 by COMPOS_1:56
.= (2 + (2 + 2)) + 4 by SCMFSA6A:35
.= 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:21
.= (2 + 2) + 10 by A1, SCMFSA6A:35
.= 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)))) + 2 by SCMFSA6A:34
.= 10 + 2 by Th41
.= 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:21
.= ((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:21
.= (((card ((((((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1)))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo ((intloc 3),(intloc 0)))) ';' ((intloc 6) := (f,(intloc 3))))) + 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 SCMFSA6A:34
.= ((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 Th41
.= ((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:22
.= 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:21
.= (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:22
.= ((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 SCMFSA6A:34
.= (((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 SCMFSA6A:34
.= ((10 + 2) + 2) + 68 by Th41
.= 82 ; :: thesis: verum