let f be FinSeq-Location ; UsedInt*Loc (bubble-sort f) = {f}
set i1 = (intloc 4) := (intloc 3);
set i2 = SubFrom ((intloc 3),(intloc 0));
set i3 = (intloc 5) := (f,(intloc 3));
set i4 = (intloc 6) := (f,(intloc 4));
set i5 = SubFrom ((intloc 6),(intloc 5));
set i6 = (f,(intloc 3)) := (intloc 6);
set i7 = (f,(intloc 4)) := (intloc 5);
set ifc = if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA));
set Sif = UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)));
set body2 = ((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)));
A1: UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))) =
(UsedInt*Loc ((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5)))) \/ {}
by SCMFSA9A:10, SCMFSA9A:16
.=
(UsedInt*Loc (((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6)))) \/ (UsedInt*Loc ((f,(intloc 4)) := (intloc 5)))
by SF_MASTR:50
.=
(UsedInt*Loc (((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6)))) \/ {f}
by SF_MASTR:37
.=
((UsedInt*Loc ((intloc 6) := (f,(intloc 4)))) \/ (UsedInt*Loc ((f,(intloc 3)) := (intloc 6)))) \/ {f}
by SF_MASTR:51
.=
((UsedInt*Loc ((intloc 6) := (f,(intloc 4)))) \/ {f}) \/ {f}
by SF_MASTR:37
.=
({f} \/ {f}) \/ {f}
by SF_MASTR:37
.=
{f}
;
A2: UsedInt*Loc (((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))) =
(UsedInt*Loc ((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5))))) \/ (UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SF_MASTR:47
.=
((UsedInt*Loc (((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4))))) \/ (UsedInt*Loc (SubFrom ((intloc 6),(intloc 5))))) \/ (UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SF_MASTR:50
.=
((UsedInt*Loc (((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4))))) \/ {}) \/ (UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SF_MASTR:36
.=
((UsedInt*Loc ((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3))))) \/ (UsedInt*Loc ((intloc 6) := (f,(intloc 4))))) \/ (UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SF_MASTR:50
.=
((UsedInt*Loc ((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3))))) \/ {f}) \/ (UsedInt*Loc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by SF_MASTR:37
.=
(UsedInt*Loc ((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3))))) \/ ({f} \/ {f})
by A1, XBOOLE_1:4
.=
((UsedInt*Loc (((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0))))) \/ (UsedInt*Loc ((intloc 5) := (f,(intloc 3))))) \/ {f}
by SF_MASTR:50
.=
((UsedInt*Loc (((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0))))) \/ {f}) \/ {f}
by SF_MASTR:37
.=
(((UsedInt*Loc ((intloc 4) := (intloc 3))) \/ (UsedInt*Loc (SubFrom ((intloc 3),(intloc 0))))) \/ {f}) \/ {f}
by SF_MASTR:51
.=
(((UsedInt*Loc ((intloc 4) := (intloc 3))) \/ {}) \/ {f}) \/ {f}
by SF_MASTR:36
.=
(({} \/ {}) \/ {f}) \/ {f}
by SF_MASTR:36
.=
{f}
;
set j1 = (intloc 2) := (intloc 1);
set j2 = SubFrom ((intloc 2),(intloc 0));
set j3 = (intloc 3) :=len f;
set Sfor = UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))));
set body1 = ((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))));
A3:
UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))) = {f}
by A2, Th37;
A4: UsedInt*Loc (((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))) =
(UsedInt*Loc ((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f))) \/ (UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SF_MASTR:47
.=
((UsedInt*Loc (((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0))))) \/ (UsedInt*Loc ((intloc 3) :=len f))) \/ (UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SF_MASTR:50
.=
((UsedInt*Loc (((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0))))) \/ {f}) \/ (UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SF_MASTR:38
.=
(((UsedInt*Loc ((intloc 2) := (intloc 1))) \/ (UsedInt*Loc (SubFrom ((intloc 2),(intloc 0))))) \/ {f}) \/ (UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SF_MASTR:51
.=
(({} \/ (UsedInt*Loc (SubFrom ((intloc 2),(intloc 0))))) \/ {f}) \/ (UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SF_MASTR:36
.=
(({} \/ {}) \/ {f}) \/ (UsedInt*Loc (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))
by SF_MASTR:36
.=
{f}
by A3
;
set k2 = (intloc 2) := (intloc 0);
set k3 = (intloc 3) := (intloc 0);
set k4 = (intloc 4) := (intloc 0);
set k5 = (intloc 5) := (intloc 0);
A5: 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 k7 = (intloc 1) :=len f;
set Ut = UsedInt*Loc (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))));
thus UsedInt*Loc (bubble-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))) \/ (UsedInt*Loc (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))
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)))) \/ (UsedInt*Loc ((intloc 1) :=len f))) \/ (UsedInt*Loc (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))
by SF_MASTR:50
.=
{f} \/ (UsedInt*Loc (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ';' (SubFrom ((intloc 2),(intloc 0)))) ';' ((intloc 3) :=len f)) ';' (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ';' (SubFrom ((intloc 3),(intloc 0)))) ';' ((intloc 5) := (f,(intloc 3)))) ';' ((intloc 6) := (f,(intloc 4)))) ';' (SubFrom ((intloc 6),(intloc 5)))) ';' (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ';' ((f,(intloc 3)) := (intloc 6))) ';' ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))))))))
by A5, SF_MASTR:38
.=
{f} \/ {f}
by A4, Th37
.=
{f}
; verum