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))))));
set k2 = (intloc 2) := (intloc 0);
set k3 = (intloc 3) := (intloc 0);
set k4 = (intloc 4) := (intloc 0);
set k5 = (intloc 5) := (intloc 0);
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))) = (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:46
.= (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:33
.= ((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:46
.= ((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:33
.= (((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:46
.= (((UsedInt*Loc ((((intloc 2) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 2))))) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:33
.= ((((UsedInt*Loc (((intloc 2) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0))))) \/ (UsedInt*Loc ((intloc 5) := (f,(intloc 2))))) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:46
.= ((((UsedInt*Loc (((intloc 2) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0))))) \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:33
.= (((((UsedInt*Loc ((intloc 2) := (intloc 3))) \/ (UsedInt*Loc (SubFrom ((intloc 3),(intloc 0))))) \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:47
.= (((({} \/ (UsedInt*Loc (SubFrom ((intloc 3),(intloc 0))))) \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:32
.= ((({} \/ {f}) \/ {f}) \/ {f}) \/ {f} by SF_MASTR:32
.= {f} ;
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)))))));
A2: 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 SCMFSA9A:10
.= (UsedInt*Loc (SubFrom ((intloc 2),(intloc 2)))) \/ (UsedInt*Loc ((AddTo ((intloc 4),(intloc 0))) ';' (SubFrom ((intloc 2),(intloc 0))))) by SF_MASTR:44
.= {} \/ (UsedInt*Loc ((AddTo ((intloc 4),(intloc 0))) ';' (SubFrom ((intloc 2),(intloc 0))))) by SF_MASTR:32
.= {} \/ ((UsedInt*Loc (AddTo ((intloc 4),(intloc 0)))) \/ (UsedInt*Loc (SubFrom ((intloc 2),(intloc 0))))) by SF_MASTR:47
.= {} \/ ({} \/ (UsedInt*Loc (SubFrom ((intloc 2),(intloc 0))))) by SF_MASTR:32
.= {} by SF_MASTR:32 ;
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));
A3: 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:46
.= (UsedInt*Loc (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0)))) \/ {} by SF_MASTR:32
.= (UsedInt*Loc ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0)))) \/ (UsedInt*Loc ((intloc 5) := (intloc 0))) by SF_MASTR:46
.= (UsedInt*Loc ((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0)))) \/ {} by SF_MASTR:32
.= (UsedInt*Loc (((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0)))) \/ (UsedInt*Loc ((intloc 4) := (intloc 0))) by SF_MASTR:46
.= (UsedInt*Loc (((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0)))) \/ {} by SF_MASTR:32
.= (UsedInt*Loc ((intloc 2) := (intloc 0))) \/ (UsedInt*Loc ((intloc 3) := (intloc 0))) by SF_MASTR:47
.= (UsedInt*Loc ((intloc 2) := (intloc 0))) \/ {} by SF_MASTR:32
.= {} by SF_MASTR:32 ;
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))));
A4: 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:46
.= (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:32
.= ((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:46
.= ((UsedInt*Loc (((((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1)))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo ((intloc 3),(intloc 0))))) \/ {f}) \/ {} by SF_MASTR:33
.= (((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:46
.= (((UsedInt*Loc ((((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1)))) ';' ((intloc 3) := (intloc 2)))) \/ {}) \/ {f}) \/ {} by SF_MASTR:32
.= ((((UsedInt*Loc (((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1))))) \/ (UsedInt*Loc ((intloc 3) := (intloc 2)))) \/ {}) \/ {f}) \/ {} by SF_MASTR:46
.= ((((UsedInt*Loc (((intloc 2) :=len f) ';' (SubFrom ((intloc 2),(intloc 1))))) \/ {}) \/ {}) \/ {f}) \/ {} by SF_MASTR:32
.= (((((UsedInt*Loc ((intloc 2) :=len f)) \/ (UsedInt*Loc (SubFrom ((intloc 2),(intloc 1))))) \/ {}) \/ {}) \/ {f}) \/ {} by SF_MASTR:47
.= (((({f} \/ (UsedInt*Loc (SubFrom ((intloc 2),(intloc 1))))) \/ {}) \/ {}) \/ {f}) \/ {} by SF_MASTR:34
.= ({f} \/ {f}) \/ {} by SF_MASTR:32
.= {f} ;
A5: 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:43
.= ((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:47
.= ({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:33
.= {f} \/ {} by A2, SF_MASTR:32
.= {f} ;
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)))))) = (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:43
.= (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:20
.= ((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:43
.= {f} \/ {f} by A5, A4, SCMFSA9A:25
.= {f} ;
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:43
.= (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:20
.= ((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:46
.= ((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:32
.= (((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:46
.= {f} \/ {f} by A3, SF_MASTR:34
.= {f} ; :: thesis: verum