let f be FinSeq-Location ; UsedIntLoc (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 = UsedIntLoc (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: UsedIntLoc (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA )) =
({(intloc 6)} \/ (UsedIntLoc ((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))))) \/ {}
by Th29, SCMFSA9A:9
.=
{(intloc 6)} \/ ((UsedIntLoc (((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6)))) \/ (UsedIntLoc (f,(intloc 4) := (intloc 5))))
by SF_MASTR:34
.=
{(intloc 6)} \/ ((UsedIntLoc (((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6)))) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:21
.=
{(intloc 6)} \/ (((UsedIntLoc ((intloc 6) := f,(intloc 4))) \/ (UsedIntLoc (f,(intloc 3) := (intloc 6)))) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:35
.=
{(intloc 6)} \/ (((UsedIntLoc ((intloc 6) := f,(intloc 4))) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:21
.=
{(intloc 6)} \/ (({(intloc 4),(intloc 6)} \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 5)})
by SF_MASTR:21
.=
{(intloc 6)} \/ ({(intloc 4),(intloc 6),(intloc 3),(intloc 6)} \/ {(intloc 4),(intloc 5)})
by ENUMSET1:45
.=
{(intloc 6)} \/ ({(intloc 6),(intloc 6),(intloc 3),(intloc 4)} \/ {(intloc 4),(intloc 5)})
by ENUMSET1:123
.=
({(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:47
.=
{(intloc 6),(intloc 3),(intloc 4)} \/ {(intloc 4),(intloc 5)}
by ENUMSET1:78
.=
({(intloc 6),(intloc 3)} \/ {(intloc 4)}) \/ {(intloc 4),(intloc 5)}
by ENUMSET1:43
.=
{(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:42
.=
{(intloc 4),(intloc 5)} \/ {(intloc 6),(intloc 3)}
by ENUMSET1:70
.=
{(intloc 4),(intloc 5),(intloc 6),(intloc 3)}
by ENUMSET1:45
.=
{(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:107
;
set ui12 = UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )));
A2: UsedIntLoc (((((((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 ))) =
(UsedIntLoc ((((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3))) ';' ((intloc 6) := f,(intloc 4))) ';' (SubFrom (intloc 6),(intloc 5)))) \/ (UsedIntLoc (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 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3))) ';' ((intloc 6) := f,(intloc 4)))) \/ (UsedIntLoc (SubFrom (intloc 6),(intloc 5)))) \/ (UsedIntLoc (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:34
.=
((UsedIntLoc (((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3))) ';' ((intloc 6) := f,(intloc 4)))) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3)))) \/ (UsedIntLoc ((intloc 6) := f,(intloc 4)))) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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:34
.=
(((UsedIntLoc ((((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 3)))) \/ {(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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:21
.=
((((UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ (UsedIntLoc ((intloc 5) := f,(intloc 3)))) \/ {(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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:34
.=
((((UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 5),(intloc 3)}) \/ {(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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:21
.=
(((UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ ({(intloc 5),(intloc 3)} \/ {(intloc 6),(intloc 4)})) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 5),(intloc 3),(intloc 6),(intloc 4)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA )))
by ENUMSET1:45
.=
(((UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA )))
by ENUMSET1:123
.=
(((UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA )))
by ENUMSET1:45
.=
((((UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 4),(intloc 3)}) \/ {(intloc 6),(intloc 5)}) \/ {(intloc 6),(intloc 5)}) \/ (UsedIntLoc (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)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 4),(intloc 3)}) \/ ({(intloc 6),(intloc 5)} \/ {(intloc 6),(intloc 5)})) \/ (UsedIntLoc (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)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})) \/ (UsedIntLoc (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)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}) \/ (UsedIntLoc (if>0 (intloc 6),((((intloc 6) := f,(intloc 4)) ';' (f,(intloc 3) := (intloc 6))) ';' (f,(intloc 4) := (intloc 5))),(Stop SCM+FSA )))
by ENUMSET1:45
.=
(UsedIntLoc (((intloc 4) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ ({(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ (UsedIntLoc (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:35
.=
((UsedIntLoc ((intloc 4) := (intloc 3))) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by SF_MASTR:18
.=
({(intloc 3),(intloc 4)} \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by SF_MASTR:18
.=
{(intloc 3),(intloc 4),(intloc 3),(intloc 0 )} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:45
.=
{(intloc 3),(intloc 3),(intloc 4),(intloc 0 )} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:104
.=
{(intloc 3),(intloc 4),(intloc 0 )} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:71
.=
{(intloc 0 ),(intloc 4),(intloc 3)} \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:102
.=
({(intloc 0 )} \/ {(intloc 4),(intloc 3)}) \/ {(intloc 4),(intloc 3),(intloc 6),(intloc 5)}
by ENUMSET1:42
.=
({(intloc 0 )} \/ {(intloc 4),(intloc 3)}) \/ ({(intloc 4),(intloc 3)} \/ {(intloc 6),(intloc 5)})
by ENUMSET1:45
.=
(({(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:45
;
set j1 = (intloc 2) := (intloc 1);
set j2 = SubFrom (intloc 2),(intloc 0 );
set j3 = (intloc 3) :=len f;
set Sfor = UsedIntLoc (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: UsedIntLoc (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, Th31
.=
{(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:42
.=
{(intloc 4),(intloc 3),(intloc 6),(intloc 5)} \/ {(intloc 0 ),(intloc 2)}
by ENUMSET1:70
.=
{(intloc 4),(intloc 5),(intloc 6),(intloc 3)} \/ {(intloc 0 ),(intloc 2)}
by ENUMSET1:107
.=
({(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 3)}) \/ {(intloc 0 ),(intloc 2)}
by ENUMSET1:46
.=
{(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:43
;
A4: UsedIntLoc (((((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 ))))) =
(UsedIntLoc ((((intloc 2) := (intloc 1)) ';' (SubFrom (intloc 2),(intloc 0 ))) ';' ((intloc 3) :=len f))) \/ (UsedIntLoc (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)) ';' (SubFrom (intloc 2),(intloc 0 )))) \/ (UsedIntLoc ((intloc 3) :=len f))) \/ (UsedIntLoc (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:34
.=
((UsedIntLoc (((intloc 2) := (intloc 1)) ';' (SubFrom (intloc 2),(intloc 0 )))) \/ {(intloc 3)}) \/ (UsedIntLoc (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:22
.=
(((UsedIntLoc ((intloc 2) := (intloc 1))) \/ (UsedIntLoc (SubFrom (intloc 2),(intloc 0 )))) \/ {(intloc 3)}) \/ (UsedIntLoc (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:35
.=
(((UsedIntLoc ((intloc 2) := (intloc 1))) \/ {(intloc 2),(intloc 0 )}) \/ {(intloc 3)}) \/ (UsedIntLoc (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
.=
(({(intloc 2),(intloc 1)} \/ {(intloc 2),(intloc 0 )}) \/ {(intloc 3)}) \/ (UsedIntLoc (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
.=
({(intloc 2),(intloc 1)} \/ ({(intloc 0 ),(intloc 2)} \/ {(intloc 3)})) \/ (UsedIntLoc (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)}) \/ (UsedIntLoc (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:43
.=
(({(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:43
.=
(({(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:45
.=
({(intloc 2),(intloc 2),(intloc 0 ),(intloc 1)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:107
.=
({(intloc 2),(intloc 0 ),(intloc 1)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:71
.=
({(intloc 0 ),(intloc 1),(intloc 2)} \/ {(intloc 3)}) \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:100
.=
{(intloc 0 ),(intloc 1),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:46
.=
{(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:59
;
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: UsedIntLoc ((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) =
(UsedIntLoc (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 )))) \/ (UsedIntLoc ((intloc 6) := (intloc 0 )))
by SF_MASTR:34
.=
(UsedIntLoc (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 )))) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:18
.=
((UsedIntLoc ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 )))) \/ (UsedIntLoc ((intloc 5) := (intloc 0 )))) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:34
.=
((UsedIntLoc ((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 )))) \/ {(intloc 5),(intloc 0 )}) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:18
.=
(((UsedIntLoc (((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 )))) \/ (UsedIntLoc ((intloc 4) := (intloc 0 )))) \/ {(intloc 5),(intloc 0 )}) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:34
.=
(((UsedIntLoc (((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 )))) \/ {(intloc 4),(intloc 0 )}) \/ {(intloc 5),(intloc 0 )}) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:18
.=
((((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:35
.=
((((UsedIntLoc ((intloc 2) := (intloc 0 ))) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 4),(intloc 0 )}) \/ {(intloc 5),(intloc 0 )}) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:18
.=
((({(intloc 2),(intloc 0 )} \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 4),(intloc 0 )}) \/ {(intloc 5),(intloc 0 )}) \/ {(intloc 6),(intloc 0 )}
by SF_MASTR:18
.=
(({(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:137
.=
({(intloc 0 ),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 0 )}) \/ {(intloc 0 ),(intloc 5),(intloc 6)}
by ENUMSET1:137
.=
({(intloc 0 ),(intloc 2),(intloc 3)} \/ {(intloc 4),(intloc 0 )}) \/ ({(intloc 0 )} \/ {(intloc 5),(intloc 6)})
by ENUMSET1:42
.=
(({(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:43
.=
({(intloc 0 ),(intloc 2),(intloc 3)} \/ ({(intloc 0 ),(intloc 0 )} \/ {(intloc 4)})) \/ {(intloc 5),(intloc 6)}
by ENUMSET1:42
.=
(({(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:48
.=
({(intloc 0 ),(intloc 2),(intloc 3)} \/ {(intloc 4)}) \/ {(intloc 5),(intloc 6)}
by ENUMSET1:78
.=
{(intloc 0 ),(intloc 2),(intloc 3),(intloc 4)} \/ {(intloc 5),(intloc 6)}
by ENUMSET1:46
.=
{(intloc 0 ),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:54
.=
{(intloc 0 )} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:51
;
set k7 = (intloc 1) :=len f;
set Ut = UsedIntLoc (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 UsedIntLoc (bubble-sort f) =
(UsedIntLoc (((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f))) \/ (UsedIntLoc (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:31
.=
((UsedIntLoc ((((((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))) \/ (UsedIntLoc (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:34
.=
(({(intloc 0 )} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}) \/ {(intloc 1)}) \/ (UsedIntLoc (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:22
.=
(({(intloc 0 )} \/ {(intloc 1)}) \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}) \/ (UsedIntLoc (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)}) \/ (UsedIntLoc (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:41
.=
{(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ (UsedIntLoc (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:57
.=
{(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, Th31
.=
({(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:57
.=
{(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:57
; verum