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 = UsedI*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 ; UsedI*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 = UsedI*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: UsedI*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))) =
(UsedI*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
.=
(UsedI*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
.=
((UsedI*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
.=
((UsedI*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
.=
(((UsedI*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
.=
(((UsedI*Loc ((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 2))))) \/ {f}) \/ {f}) \/ {f}
by SF_MASTR:33
.=
((((UsedI*Loc (((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ (UsedInt*Loc ((intloc 5) := (f,(intloc 2))))) \/ {f}) \/ {f}) \/ {f}
by SF_MASTR:46
.=
((((UsedI*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 = UsedI*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: UsedI*Loc (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))) =
(UsedI*Loc (Macro (SubFrom ((intloc 2),(intloc 2))))) \/ (UsedI*Loc ((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))
by SCMFSA9A:10
.=
(UsedInt*Loc (SubFrom ((intloc 2),(intloc 2)))) \/ (UsedI*Loc ((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))
by SF_MASTR:44
.=
{} \/ (UsedI*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: UsedI*Loc ((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) =
(UsedI*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
.=
(UsedI*Loc (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0)))) \/ {}
by SF_MASTR:32
.=
(UsedI*Loc ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0)))) \/ (UsedInt*Loc ((intloc 5) := (intloc 0)))
by SF_MASTR:46
.=
(UsedI*Loc ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0)))) \/ {}
by SF_MASTR:32
.=
(UsedI*Loc (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0)))) \/ (UsedInt*Loc ((intloc 4) := (intloc 0)))
by SF_MASTR:46
.=
(UsedI*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 = UsedI*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 = UsedI*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: UsedI*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)))) =
(UsedI*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
.=
(UsedI*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
.=
((UsedI*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
.=
((UsedI*Loc (((((intloc 2) :=len f) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0))))) \/ {f}) \/ {}
by SF_MASTR:33
.=
(((UsedI*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
.=
(((UsedI*Loc ((((intloc 2) :=len f) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2)))) \/ {}) \/ {f}) \/ {}
by SF_MASTR:32
.=
((((UsedI*Loc (((intloc 2) :=len f) ";" (SubFrom ((intloc 2),(intloc 1))))) \/ (UsedInt*Loc ((intloc 3) := (intloc 2)))) \/ {}) \/ {f}) \/ {}
by SF_MASTR:46
.=
((((UsedI*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: UsedI*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))))))) =
(UsedI*Loc (((intloc 5) := (f,(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6))))) \/ (UsedI*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))))) \/ (UsedI*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))))) \/ (UsedI*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: UsedI*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)))))) =
(UsedI*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))))))))))) \/ (UsedI*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
.=
(UsedI*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, SCMFSA9A:45
.=
((UsedI*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))))) \/ (UsedI*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 UsedI*Loc (insert-sort f) =
(UsedI*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))))) \/ (UsedI*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
.=
(UsedI*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, SCMFSA9A:45
.=
((UsedI*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
.=
((UsedI*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
.=
(((UsedI*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}
; verum