let f be FinSeq-Location ; :: thesis: UsedInt*Loc (insert-sort f) = {f}
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));
set Ub3 = UsedInt*Loc (((((((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: UsedInt*Loc (((((((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))) = {f}

proof

thus UsedInt*Loc (((((((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))) = (UsedInt*Loc ((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6)))) \/ (UsedInt*Loc (f,(intloc 3) := (intloc 5))) by SF_MASTR:50
.= (UsedInt*Loc ((((((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} by SF_MASTR:37
.= ((UsedInt*Loc (((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3)))) \/ (UsedInt*Loc (f,(intloc 2) := (intloc 6)))) \/ {f} by SF_MASTR:50
.= ((UsedInt*Loc (((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3)))) \/ {f}) \/ {f} by SF_MASTR:37
.= (((UsedInt*Loc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ (UsedInt*Loc ((intloc 6) := f,(intloc 3)))) \/ {f}) \/ {f} by SF_MASTR:50
.= (((UsedInt*Loc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:37
.= ((((UsedInt*Loc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ (UsedInt*Loc ((intloc 5) := f,(intloc 2)))) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:50
.= ((((UsedInt*Loc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:37
.= (((((UsedInt*Loc ((intloc 2) := (intloc 3))) \/ (UsedInt*Loc (SubFrom (intloc 3),(intloc 0 )))) \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:51
.= (((({} \/ (UsedInt*Loc (SubFrom (intloc 3),(intloc 0 )))) \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:36
.= ((({} \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:36
.= {f} ; :: thesis: verum

end;

set k2 = (intloc 2) := (intloc 0 );
set k3 = (intloc 3) := (intloc 0 );
set k4 = (intloc 4) := (intloc 0 );
set k5 = (intloc 5) := (intloc 0 );
A2: UsedInt*Loc ((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) = (UsedInt*Loc (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 )))) \/ (UsedInt*Loc ((intloc 6) := (intloc 0 ))) by SF_MASTR:50
.= (UsedInt*Loc (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 )))) \/ {} by SF_MASTR:36
.= (UsedInt*Loc ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 )))) \/ (UsedInt*Loc ((intloc 5) := (intloc 0 ))) by SF_MASTR:50
.= (UsedInt*Loc ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 )))) \/ {} by SF_MASTR:36
.= (UsedInt*Loc (((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 )))) \/ (UsedInt*Loc ((intloc 4) := (intloc 0 ))) by SF_MASTR:50
.= (UsedInt*Loc (((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 )))) \/ {} by SF_MASTR:36
.= (UsedInt*Loc ((intloc 2) := (intloc 0 ))) \/ (UsedInt*Loc ((intloc 3) := (intloc 0 ))) by SF_MASTR:51
.= (UsedInt*Loc ((intloc 2) := (intloc 0 ))) \/ {} by SF_MASTR:36
.= {} by SF_MASTR:36 ;
set m0 = SubFrom (intloc 2),(intloc 2);
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 )));
set UIF = UsedInt*Loc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))));
A3: UsedInt*Loc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) = {}

proof

thus UsedInt*Loc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) = (UsedInt*Loc (Macro (SubFrom (intloc 2),(intloc 2)))) \/ (UsedInt*Loc ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) by SCMBSORT:35
.= (UsedInt*Loc (SubFrom (intloc 2),(intloc 2))) \/ (UsedInt*Loc ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) by SF_MASTR:48
.= {} \/ (UsedInt*Loc ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) by SF_MASTR:36
.= {} \/ ((UsedInt*Loc (AddTo (intloc 4),(intloc 0 ))) \/ (UsedInt*Loc (SubFrom (intloc 2),(intloc 0 )))) by SF_MASTR:51
.= {} \/ ({} \/ (UsedInt*Loc (SubFrom (intloc 2),(intloc 0 )))) by SF_MASTR:36
.= {} by SF_MASTR:36 ; :: thesis: verum

end;

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 ))));
set Ub2 = UsedInt*Loc ((((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 )))));
A4: UsedInt*Loc ((((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 ))))) = {f}

proof

thus UsedInt*Loc ((((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 ))))) = (UsedInt*Loc (((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6)))) \/ (UsedInt*Loc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))) by SF_MASTR:47
.= ((UsedInt*Loc ((intloc 5) := f,(intloc 2))) \/ (UsedInt*Loc (SubFrom (intloc 5),(intloc 6)))) \/ (UsedInt*Loc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))) by SF_MASTR:51
.= ({f} \/ (UsedInt*Loc (SubFrom (intloc 5),(intloc 6)))) \/ (UsedInt*Loc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))) by SF_MASTR:37
.= {f} \/ {} by A3, SF_MASTR:36
.= {f} ; :: thesis: verum

end;

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))));
set Ub1 = UsedInt*Loc (((((((((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)))));
set Ut16 = UsedInt*Loc (((((((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)));
A5: UsedInt*Loc (((((((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))) = {f}

proof

thus UsedInt*Loc (((((((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))) = (UsedInt*Loc ((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3)))) \/ (UsedInt*Loc (SubFrom (intloc 4),(intloc 4))) by SF_MASTR:50
.= (UsedInt*Loc ((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3)))) \/ {} by SF_MASTR:36
.= ((UsedInt*Loc (((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 )))) \/ (UsedInt*Loc ((intloc 6) := f,(intloc 3)))) \/ {} by SF_MASTR:50
.= ((UsedInt*Loc (((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 )))) \/ {f}) \/ {} by SF_MASTR:37
.= (((UsedInt*Loc ((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2)))) \/ (UsedInt*Loc (AddTo (intloc 3),(intloc 0 )))) \/ {f}) \/ {} by SF_MASTR:50
.= (((UsedInt*Loc ((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2)))) \/ {} ) \/ {f}) \/ {} by SF_MASTR:36
.= ((((UsedInt*Loc (((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1)))) \/ (UsedInt*Loc ((intloc 3) := (intloc 2)))) \/ {} ) \/ {f}) \/ {} by SF_MASTR:50
.= ((((UsedInt*Loc (((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1)))) \/ {} ) \/ {} ) \/ {f}) \/ {} by SF_MASTR:36
.= (((((UsedInt*Loc ((intloc 2) :=len f)) \/ (UsedInt*Loc (SubFrom (intloc 2),(intloc 1)))) \/ {} ) \/ {} ) \/ {f}) \/ {} by SF_MASTR:51
.= (((({f} \/ (UsedInt*Loc (SubFrom (intloc 2),(intloc 1)))) \/ {} ) \/ {} ) \/ {f}) \/ {} by SF_MASTR:38
.= ({f} \/ {f}) \/ {} by SF_MASTR:36
.= {f} ; :: thesis: verum

end;

A6: UsedInt*Loc (((((((((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))))) = {f}

proof

thus UsedInt*Loc (((((((((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))))) = (UsedInt*Loc ((((((((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 )))))))) \/ (UsedInt*Loc (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 SF_MASTR:47
.= (UsedInt*Loc ((((((((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 )))))))) \/ {f} by A1, SCMBSORT:37
.= ((UsedInt*Loc (((((((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)))) \/ (UsedInt*Loc (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 )))))))) \/ {f} by SF_MASTR:47
.= {f} \/ {f} by A4, A5, SCMFSA9A:31
.= {f} ; :: thesis: verum

end;

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 );
thus UsedInt*Loc (insert-sort f) = (UsedInt*Loc ((((((((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 )))) \/ (UsedInt*Loc (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 SF_MASTR:47
.= (UsedInt*Loc ((((((((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 )))) \/ {f} by A6, SCMBSORT:37
.= ((UsedInt*Loc (((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f))) \/ (UsedInt*Loc (SubFrom (intloc 1),(intloc 0 )))) \/ {f} by SF_MASTR:50
.= ((UsedInt*Loc (((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f))) \/ {} ) \/ {f} by SF_MASTR:36
.= (((UsedInt*Loc ((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 )))) \/ (UsedInt*Loc ((intloc 1) :=len f))) \/ {} ) \/ {f} by SF_MASTR:50
.= {f} \/ {f} by A2, SF_MASTR:38
.= {f} ; :: thesis: verum