let f be FinSeq-Location ; UsedILoc (bubble-sort f) = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
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 = UsedILoc (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: UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))) =
({(intloc 6)} \/ (UsedILoc ((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))))) \/ {}
by SCMFSA9A:3, SCMFSA9A:43
.=
{(intloc 6)} \/ ((UsedILoc (((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6)))) \/ (UsedIntLoc ((f,(intloc 4)) := (intloc 5))))
by SF_MASTR:30
.=
{(intloc 6)} \/ ((UsedILoc (((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6)))) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:17
.=
{(intloc 6)} \/ (((UsedIntLoc ((intloc 6) := (f,(intloc 4)))) \/ (UsedIntLoc ((f,(intloc 3)) := (intloc 6)))) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:31
.=
{(intloc 6)} \/ (((UsedIntLoc ((intloc 6) := (f,(intloc 4)))) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:17
.=
{(intloc 6)} \/ (({(intloc 4),(intloc 6)} \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:17
.=
{(intloc 6)} \/ ({(intloc 4),(intloc 6),(intloc 3),(intloc 6)} \/ {(intloc 4),(intloc 5)})
by ENUMSET1:5
.=
{(intloc 6)} \/ ({(intloc 6),(intloc 6),(intloc 3),(intloc 4)} \/ {(intloc 4),(intloc 5)})
by ENUMSET1:75
.=
({(intloc 6)} \/ {(intloc 6),(intloc 6),(intloc 3),(intloc 4)}) \/ {(intloc 4),(intloc 5)}
by XBOOLE_1:4
.=
{(intloc 6),(intloc 6),(intloc 6),(intloc 3),(intloc 4)} \/ {(intloc 4),(intloc 5)}
by ENUMSET1:7
.=
{(intloc 6),(intloc 3),(intloc 4)} \/ {(intloc 4),(intloc 5)}
by ENUMSET1:38
.=
({(intloc 6),(intloc 3)} \/ {(intloc 4)}) \/ {(intloc 4),(intloc 5)}
by ENUMSET1:3
.=
{(intloc 6),(intloc 3)} \/ ({(intloc 4)} \/ {(intloc 4),(intloc 5)})
by XBOOLE_1:4
.=
{(intloc 6),(intloc 3)} \/ {(intloc 4),(intloc 4),(intloc 5)}
by ENUMSET1:2
.=
{(intloc 4),(intloc 5)} \/ {(intloc 6),(intloc 3)}
by ENUMSET1:30
.=
{(intloc 4),(intloc 5),(intloc 6),(intloc 3)}
by ENUMSET1:5
.=
{(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:64
;
set ui12 = UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))));
A2: UsedILoc (((((((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)))) =
(UsedILoc ((((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4)))) ";" (SubFrom ((intloc 6),(intloc 5))))) \/ (UsedILoc (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:27
.=
((UsedILoc (((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4))))) \/ (UsedIntLoc (SubFrom ((intloc 6),(intloc 5))))) \/ (UsedILoc (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:30
.=
((UsedILoc (((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4))))) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (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:14
.=
(((UsedILoc ((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3))))) \/ (UsedIntLoc ((intloc 6) := (f,(intloc 4))))) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (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:30
.=
(((UsedILoc ((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3))))) \/ {(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (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:17
.=
((((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ (UsedIntLoc ((intloc 5) := (f,(intloc 3))))) \/ {(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (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:30
.=
((((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 5),(intloc 3)}) \/ {(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (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:17
.=
(((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ ({(intloc 5),(intloc 3)} \/ {(intloc 6),(intloc 4)})) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by XBOOLE_1:4
.=
(((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 5),(intloc 3),(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by ENUMSET1:5
.=
(((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by ENUMSET1:75
.=
(((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by ENUMSET1:5
.=
((((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 4),(intloc 3)}) \/ {(intloc 6),(intloc 5)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by XBOOLE_1:4
.=
(((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 4),(intloc 3)}) \/ ({(intloc 6),(intloc 5)} \/ {(intloc 6),(intloc 5)})) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by XBOOLE_1:4
.=
((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by XBOOLE_1:4
.=
((UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}) \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA))))
by ENUMSET1:5
.=
(UsedILoc (((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0))))) \/ ({(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ (UsedILoc (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))
by XBOOLE_1:4
.=
((UsedIntLoc ((intloc 4) := (intloc 3))) \/ (UsedIntLoc (SubFrom ((intloc 3),(intloc 0))))) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by A1, SF_MASTR:31
.=
((UsedIntLoc ((intloc 4) := (intloc 3))) \/ {(intloc 3),(intloc 0)}) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by SF_MASTR:14
.=
({(intloc 3),(intloc 4)} \/ {(intloc 3),(intloc 0)}) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by SF_MASTR:14
.=
{(intloc 3),(intloc 4),(intloc 3),(intloc 0)} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:5
.=
{(intloc 3),(intloc 3),(intloc 4),(intloc 0)} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:62
.=
{(intloc 3),(intloc 4),(intloc 0)} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:31
.=
{(intloc 0),(intloc 4),(intloc 3)} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:60
.=
({(intloc 0)} \/ {(intloc 4),(intloc 3)}) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:2
.=
({(intloc 0)} \/ {(intloc 4),(intloc 3)}) \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})
by ENUMSET1:5
.=
(({(intloc 0)} \/ {(intloc 4),(intloc 3)}) \/ {(intloc 4),(intloc 3)}) \/ {(intloc 6),(intloc 5)}
by XBOOLE_1:4
.=
({(intloc 0)} \/ ({(intloc 4),(intloc 3)} \/ {(intloc 4),(intloc 3)})) \/ {(intloc 6),(intloc 5)}
by XBOOLE_1:4
.=
{(intloc 0)} \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})
by XBOOLE_1:4
.=
{(intloc 0)} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:5
;
set j1 = (intloc 2) := (intloc 1);
set j2 = SubFrom ((intloc 2),(intloc 0));
set j3 = (intloc 3) :=len f;
set Sfor = UsedILoc (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: UsedILoc (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)))))) =
({(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ {(intloc 0)}) \/ {(intloc 2),(intloc 0)}
by A2, SCMFSA9A:44
.=
{(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ ({(intloc 0)} \/ {(intloc 2),(intloc 0)})
by XBOOLE_1:4
.=
{(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ {(intloc 0),(intloc 0),(intloc 2)}
by ENUMSET1:2
.=
{(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ {(intloc 0),(intloc 2)}
by ENUMSET1:30
.=
{(intloc 4),(intloc 5),(intloc 6),(intloc 3)} \/ {(intloc 0),(intloc 2)}
by ENUMSET1:64
.=
({(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 3)}) \/ {(intloc 0),(intloc 2)}
by ENUMSET1:6
.=
{(intloc 4),(intloc 5),(intloc 6)} \/ ({(intloc 3)} \/ {(intloc 0),(intloc 2)})
by XBOOLE_1:4
.=
{(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 0),(intloc 2),(intloc 3)}
by ENUMSET1:3
;
A4: UsedILoc (((((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))))))) =
(UsedILoc ((((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0)))) ";" ((intloc 3) :=len f))) \/ (UsedILoc (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:27
.=
((UsedILoc (((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0))))) \/ (UsedIntLoc ((intloc 3) :=len f))) \/ (UsedILoc (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:30
.=
((UsedILoc (((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0))))) \/ {(intloc 3)}) \/ (UsedILoc (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:18
.=
(((UsedIntLoc ((intloc 2) := (intloc 1))) \/ (UsedIntLoc (SubFrom ((intloc 2),(intloc 0))))) \/ {(intloc 3)}) \/ (UsedILoc (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:31
.=
(((UsedIntLoc ((intloc 2) := (intloc 1))) \/ {(intloc 2),(intloc 0)}) \/ {(intloc 3)}) \/ (UsedILoc (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:14
.=
(({(intloc 2),(intloc 1)} \/ {(intloc 2),(intloc 0)}) \/ {(intloc 3)}) \/ (UsedILoc (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:14
.=
({(intloc 2),(intloc 1)} \/ ({(intloc 0),(intloc 2)} \/ {(intloc 3)})) \/ (UsedILoc (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 XBOOLE_1:4
.=
({(intloc 2),(intloc 1)} \/ {(intloc 0),(intloc 2),(intloc 3)}) \/ (UsedILoc (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 ENUMSET1:3
.=
(({(intloc 2),(intloc 1)} \/ {(intloc 0),(intloc 2),(intloc 3)}) \/ {(intloc 0),(intloc 2),(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by A3, XBOOLE_1:4
.=
({(intloc 2),(intloc 1)} \/ ({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 0),(intloc 2),(intloc 3)})) \/ {(intloc 4),(intloc 5),(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 2),(intloc 1)} \/ ({(intloc 0),(intloc 2)} \/ {(intloc 3)})) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:3
.=
(({(intloc 2),(intloc 1)} \/ {(intloc 0),(intloc 2)}) \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 2),(intloc 1),(intloc 0),(intloc 2)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:5
.=
({(intloc 2),(intloc 2),(intloc 0),(intloc 1)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:64
.=
({(intloc 2),(intloc 0),(intloc 1)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:31
.=
({(intloc 0),(intloc 1),(intloc 2)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:59
.=
{(intloc 0),(intloc 1),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:6
.=
{(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:19
;
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: UsedILoc ((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) =
(UsedILoc (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0)))) \/ (UsedIntLoc ((intloc 6) := (intloc 0)))
by SF_MASTR:30
.=
(UsedILoc (((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0)))) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:14
.=
((UsedILoc ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0)))) \/ (UsedIntLoc ((intloc 5) := (intloc 0)))) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:30
.=
((UsedILoc ((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0)))) \/ {(intloc 5),(intloc 0)}) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:14
.=
(((UsedILoc (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0)))) \/ (UsedIntLoc ((intloc 4) := (intloc 0)))) \/ {(intloc 5),(intloc 0)}) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:30
.=
(((UsedILoc (((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0)))) \/ {(intloc 4),(intloc 0)}) \/ {(intloc 5),(intloc 0)}) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:14
.=
((((UsedIntLoc ((intloc 2) := (intloc 0))) \/ (UsedIntLoc ((intloc 3) := (intloc 0)))) \/ {(intloc 4),(intloc 0)}) \/ {(intloc 5),(intloc 0)}) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:31
.=
((((UsedIntLoc ((intloc 2) := (intloc 0))) \/ {(intloc 3),(intloc 0)}) \/ {(intloc 4),(intloc 0)}) \/ {(intloc 5),(intloc 0)}) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:14
.=
((({(intloc 2),(intloc 0)} \/ {(intloc 3),(intloc 0)}) \/ {(intloc 4),(intloc 0)}) \/ {(intloc 5),(intloc 0)}) \/ {(intloc 6),(intloc 0)}
by SF_MASTR:14
.=
(({(intloc 2),(intloc 0)} \/ {(intloc 3),(intloc 0)}) \/ {(intloc 4),(intloc 0)}) \/ ({(intloc 5),(intloc 0)} \/ {(intloc 6),(intloc 0)})
by XBOOLE_1:4
.=
(({(intloc 2),(intloc 0)} \/ {(intloc 3),(intloc 0)}) \/ {(intloc 4),(intloc 0)}) \/ {(intloc 0),(intloc 5),(intloc 6)}
by ENUMSET1:87
.=
({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 0)}) \/ {(intloc 0),(intloc 5),(intloc 6)}
by ENUMSET1:87
.=
({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 0)}) \/ ({(intloc 0)} \/ {(intloc 5),(intloc 6)})
by ENUMSET1:2
.=
(({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 0)}) \/ {(intloc 0)}) \/ {(intloc 5),(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 0),(intloc 2),(intloc 3)} \/ ({(intloc 4),(intloc 0)} \/ {(intloc 0)})) \/ {(intloc 5),(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 0),(intloc 0)}) \/ {(intloc 5),(intloc 6)}
by ENUMSET1:3
.=
({(intloc 0),(intloc 2),(intloc 3)} \/ ({(intloc 0),(intloc 0)} \/ {(intloc 4)})) \/ {(intloc 5),(intloc 6)}
by ENUMSET1:2
.=
(({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 0),(intloc 0)}) \/ {(intloc 4)}) \/ {(intloc 5),(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 0),(intloc 0),(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 4)}) \/ {(intloc 5),(intloc 6)}
by ENUMSET1:8
.=
({(intloc 0),(intloc 2),(intloc 3)} \/ {(intloc 4)}) \/ {(intloc 5),(intloc 6)}
by ENUMSET1:38
.=
{(intloc 0),(intloc 2),(intloc 3),(intloc 4)} \/ {(intloc 5),(intloc 6)}
by ENUMSET1:6
.=
{(intloc 0),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:14
.=
{(intloc 0)} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:11
;
set k7 = (intloc 1) :=len f;
set Ut = UsedILoc (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 UsedILoc (bubble-sort f) =
(UsedILoc (((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" ((intloc 1) :=len f))) \/ (UsedILoc (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:27
.=
((UsedILoc ((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0)))) \/ (UsedIntLoc ((intloc 1) :=len f))) \/ (UsedILoc (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:30
.=
(({(intloc 0)} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}) \/ {(intloc 1)}) \/ (UsedILoc (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:18
.=
(({(intloc 0)} \/ {(intloc 1)}) \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}) \/ (UsedILoc (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 XBOOLE_1:4
.=
({(intloc 0),(intloc 1)} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}) \/ (UsedILoc (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 ENUMSET1:1
.=
{(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ (UsedILoc (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 ENUMSET1:17
.=
{(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ ({(intloc 1),(intloc 0)} \/ {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)})
by A4, SCMFSA9A:44
.=
({(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}) \/ {(intloc 1),(intloc 0)}
by XBOOLE_1:4
.=
({(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 0),(intloc 1)}) \/ {(intloc 0),(intloc 1)}
by ENUMSET1:17
.=
{(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ ({(intloc 0),(intloc 1)} \/ {(intloc 0),(intloc 1)})
by XBOOLE_1:4
.=
{(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:17
; verum