let f be FinSeq-Location ; :: thesis: 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} ; :: thesis: verum