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) = 71
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 Th21
.= 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 Th21
.= ((10 + 2) + (14 + 5)) + (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_X:4
.= ((10 + 2) + (14 + 5)) + (12 + 7) by A3, SCMFSA8C:94
.= 50 ;
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))))) + (50 + 7) by A4, SCMFSA8C:94
.= ((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) + (50 + 7) 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) + (50 + 7) by SCMFSA6A:34
.= ((10 + 2) + 2) + 57 by Th21
.= 71 ; :: thesis: verum