let f be FinSeq-Location ; :: thesis: UsedIntLoc (insert-sort f) = {(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
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 Ui123 = UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)));
set Ui12 = UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )));
set Ub3 = UsedIntLoc (((((((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:
UsedIntLoc (((((((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))) = {(intloc 3),(intloc 5)} \/ {(intloc 2),(intloc 0 ),(intloc 6)}
proof
thus UsedIntLoc (((((((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))) =
(UsedIntLoc ((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6)))) \/ (UsedIntLoc (f,(intloc 3) := (intloc 5)))
by SF_MASTR:34
.=
(UsedIntLoc ((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6)))) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:21
.=
((UsedIntLoc (((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3)))) \/ (UsedIntLoc (f,(intloc 2) := (intloc 6)))) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:34
.=
((UsedIntLoc (((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3)))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:21
.=
(((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ (UsedIntLoc ((intloc 6) := f,(intloc 3)))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:34
.=
(((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 3)}) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:21
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ ({(intloc 6),(intloc 3)} \/ {(intloc 2),(intloc 6)})) \/ {(intloc 3),(intloc 5)}
by XBOOLE_1:4
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 3),(intloc 2),(intloc 6)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:45
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 6),(intloc 2),(intloc 3)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:107
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 2),(intloc 3)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:71
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ ({(intloc 6),(intloc 2)} \/ {(intloc 3)})) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:43
.=
(((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 2)}) \/ {(intloc 3)}) \/ {(intloc 3),(intloc 5)}
by XBOOLE_1:4
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 2)}) \/ ({(intloc 3)} \/ {(intloc 3),(intloc 5)})
by XBOOLE_1:4
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 2)}) \/ {(intloc 3),(intloc 3),(intloc 5)}
by ENUMSET1:42
.=
((UsedIntLoc ((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 2)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:70
.=
(((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ (UsedIntLoc ((intloc 5) := f,(intloc 2)))) \/ {(intloc 6),(intloc 2)}) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:34
.=
(((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 5),(intloc 2)}) \/ {(intloc 6),(intloc 2)}) \/ {(intloc 3),(intloc 5)}
by SF_MASTR:21
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ ({(intloc 5),(intloc 2)} \/ {(intloc 6),(intloc 2)})) \/ {(intloc 3),(intloc 5)}
by XBOOLE_1:4
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 5),(intloc 2),(intloc 6),(intloc 2)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:45
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 2),(intloc 6),(intloc 5)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:123
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6),(intloc 5)}) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:71
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ ({(intloc 2),(intloc 6)} \/ {(intloc 5)})) \/ {(intloc 3),(intloc 5)}
by ENUMSET1:43
.=
(((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5)}) \/ {(intloc 3),(intloc 5)}
by XBOOLE_1:4
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ ({(intloc 5)} \/ {(intloc 3),(intloc 5)})
by XBOOLE_1:4
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3),(intloc 5)}
by ENUMSET1:43
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 5),(intloc 3)}
by ENUMSET1:98
.=
((UsedIntLoc (((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:70
.=
(((UsedIntLoc ((intloc 2) := (intloc 3))) \/ (UsedIntLoc (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by SF_MASTR:35
.=
(({(intloc 2),(intloc 3)} \/ (UsedIntLoc (SubFrom (intloc 3),(intloc 0 )))) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by SF_MASTR:18
.=
(({(intloc 2),(intloc 3)} \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by SF_MASTR:18
.=
({(intloc 2),(intloc 3),(intloc 3),(intloc 0 )} \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:45
.=
({(intloc 3),(intloc 3),(intloc 2),(intloc 0 )} \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:116
.=
({(intloc 3),(intloc 2),(intloc 0 )} \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:71
.=
(({(intloc 3)} \/ {(intloc 2),(intloc 0 )}) \/ {(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:42
.=
({(intloc 3)} \/ ({(intloc 2),(intloc 0 )} \/ {(intloc 2),(intloc 6)})) \/ {(intloc 5),(intloc 3)}
by XBOOLE_1:4
.=
({(intloc 3)} \/ {(intloc 2),(intloc 0 ),(intloc 2),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:45
.=
({(intloc 3)} \/ {(intloc 2),(intloc 2),(intloc 0 ),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:104
.=
({(intloc 3)} \/ {(intloc 2),(intloc 0 ),(intloc 6)}) \/ {(intloc 5),(intloc 3)}
by ENUMSET1:71
.=
({(intloc 3)} \/ {(intloc 5),(intloc 3)}) \/ {(intloc 2),(intloc 0 ),(intloc 6)}
by XBOOLE_1:4
.=
{(intloc 3),(intloc 5),(intloc 3)} \/ {(intloc 2),(intloc 0 ),(intloc 6)}
by ENUMSET1:43
.=
{(intloc 3),(intloc 3),(intloc 5)} \/ {(intloc 2),(intloc 0 ),(intloc 6)}
by ENUMSET1:98
.=
{(intloc 3),(intloc 5)} \/ {(intloc 2),(intloc 0 ),(intloc 6)}
by ENUMSET1:70
;
:: thesis: verum
end;
set k2 = (intloc 2) := (intloc 0 );
set k3 = (intloc 3) := (intloc 0 );
set k4 = (intloc 4) := (intloc 0 );
set k5 = (intloc 5) := (intloc 0 );
A2:
UsedIntLoc ((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) = {(intloc 0 )} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
proof
thus 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
;
:: thesis: verum
end;
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 = UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))));
A3:
UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) = {(intloc 2),(intloc 5)} \/ {(intloc 4),(intloc 0 )}
proof
thus UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))) =
({(intloc 5)} \/ (UsedIntLoc (Macro (SubFrom (intloc 2),(intloc 2))))) \/ (UsedIntLoc ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))
by SCMBSORT:29
.=
({(intloc 5)} \/ (UsedIntLoc (SubFrom (intloc 2),(intloc 2)))) \/ (UsedIntLoc ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))
by SF_MASTR:32
.=
({(intloc 5)} \/ {(intloc 2),(intloc 2)}) \/ (UsedIntLoc ((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))
by SF_MASTR:18
.=
({(intloc 5)} \/ {(intloc 2),(intloc 2)}) \/ ((UsedIntLoc (AddTo (intloc 4),(intloc 0 ))) \/ (UsedIntLoc (SubFrom (intloc 2),(intloc 0 ))))
by SF_MASTR:35
.=
({(intloc 5)} \/ {(intloc 2),(intloc 2)}) \/ ({(intloc 4),(intloc 0 )} \/ (UsedIntLoc (SubFrom (intloc 2),(intloc 0 ))))
by SF_MASTR:18
.=
({(intloc 5)} \/ {(intloc 2),(intloc 2)}) \/ ({(intloc 4),(intloc 0 )} \/ {(intloc 2),(intloc 0 )})
by SF_MASTR:18
.=
({(intloc 5)} \/ {(intloc 2)}) \/ ({(intloc 4),(intloc 0 )} \/ {(intloc 2),(intloc 0 )})
by ENUMSET1:69
.=
(({(intloc 5)} \/ {(intloc 2)}) \/ {(intloc 2),(intloc 0 )}) \/ {(intloc 4),(intloc 0 )}
by XBOOLE_1:4
.=
({(intloc 2),(intloc 5)} \/ {(intloc 2),(intloc 0 )}) \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:41
.=
{(intloc 2),(intloc 5),(intloc 2),(intloc 0 )} \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:45
.=
{(intloc 2),(intloc 2),(intloc 5),(intloc 0 )} \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:104
.=
{(intloc 2),(intloc 5),(intloc 0 )} \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:71
.=
{(intloc 2),(intloc 5),(intloc 0 ),(intloc 4),(intloc 0 )}
by ENUMSET1:49
.=
{(intloc 2)} \/ {(intloc 5),(intloc 0 ),(intloc 4),(intloc 0 )}
by ENUMSET1:47
.=
{(intloc 2)} \/ {(intloc 0 ),(intloc 0 ),(intloc 4),(intloc 5)}
by ENUMSET1:123
.=
{(intloc 2)} \/ {(intloc 0 ),(intloc 4),(intloc 5)}
by ENUMSET1:71
.=
{(intloc 2),(intloc 0 ),(intloc 4),(intloc 5)}
by ENUMSET1:44
.=
{(intloc 2),(intloc 5),(intloc 4),(intloc 0 )}
by ENUMSET1:107
.=
{(intloc 2),(intloc 5)} \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:45
;
:: thesis: verum
end;
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 = UsedIntLoc ((((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 )))));
A4:
UsedIntLoc ((((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 ))))) = {(intloc 5),(intloc 2),(intloc 6),(intloc 4),(intloc 0 )}
proof
thus UsedIntLoc ((((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 ))))) =
(UsedIntLoc (((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6)))) \/ (UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SF_MASTR:31
.=
((UsedIntLoc ((intloc 5) := f,(intloc 2))) \/ (UsedIntLoc (SubFrom (intloc 5),(intloc 6)))) \/ (UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SF_MASTR:35
.=
({(intloc 2),(intloc 5)} \/ (UsedIntLoc (SubFrom (intloc 5),(intloc 6)))) \/ (UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SF_MASTR:21
.=
({(intloc 2),(intloc 5)} \/ {(intloc 5),(intloc 6)}) \/ (UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by SF_MASTR:18
.=
{(intloc 2),(intloc 5),(intloc 5),(intloc 6)} \/ (UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by ENUMSET1:45
.=
{(intloc 5),(intloc 5),(intloc 2),(intloc 6)} \/ (UsedIntLoc (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 )))))
by ENUMSET1:116
.=
{(intloc 5),(intloc 2),(intloc 6)} \/ ({(intloc 2),(intloc 5)} \/ {(intloc 4),(intloc 0 )})
by A3, ENUMSET1:71
.=
({(intloc 5),(intloc 2),(intloc 6)} \/ {(intloc 2),(intloc 5)}) \/ {(intloc 4),(intloc 0 )}
by XBOOLE_1:4
.=
{(intloc 2),(intloc 5),(intloc 5),(intloc 2),(intloc 6)} \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:48
.=
({(intloc 2),(intloc 5),(intloc 5),(intloc 2)} \/ {(intloc 6)}) \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:50
.=
({(intloc 2),(intloc 2),(intloc 5),(intloc 5)} \/ {(intloc 6)}) \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:107
.=
({(intloc 2),(intloc 5),(intloc 5)} \/ {(intloc 6)}) \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:71
.=
({(intloc 5),(intloc 5),(intloc 2)} \/ {(intloc 6)}) \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:102
.=
({(intloc 5),(intloc 2)} \/ {(intloc 6)}) \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:70
.=
{(intloc 5),(intloc 2),(intloc 6)} \/ {(intloc 4),(intloc 0 )}
by ENUMSET1:43
.=
{(intloc 5),(intloc 2),(intloc 6),(intloc 4),(intloc 0 )}
by ENUMSET1:49
;
:: thesis: verum
end;
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 = UsedIntLoc (((((((((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 = UsedIntLoc (((((((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)));
A5:
UsedIntLoc (((((((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))) = {(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}
proof
thus UsedIntLoc (((((((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))) =
(UsedIntLoc ((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3)))) \/ (UsedIntLoc (SubFrom (intloc 4),(intloc 4)))
by SF_MASTR:34
.=
(UsedIntLoc ((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3)))) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:18
.=
((UsedIntLoc (((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 )))) \/ (UsedIntLoc ((intloc 6) := f,(intloc 3)))) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:34
.=
((UsedIntLoc (((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 )))) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:21
.=
(((UsedIntLoc ((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2)))) \/ (UsedIntLoc (AddTo (intloc 3),(intloc 0 )))) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:34
.=
(((UsedIntLoc ((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2)))) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:18
.=
((((UsedIntLoc (((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1)))) \/ (UsedIntLoc ((intloc 3) := (intloc 2)))) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:34
.=
((((UsedIntLoc (((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1)))) \/ {(intloc 3),(intloc 2)}) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:18
.=
(((((UsedIntLoc ((intloc 2) :=len f)) \/ (UsedIntLoc (SubFrom (intloc 2),(intloc 1)))) \/ {(intloc 3),(intloc 2)}) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:35
.=
(((({(intloc 2)} \/ (UsedIntLoc (SubFrom (intloc 2),(intloc 1)))) \/ {(intloc 3),(intloc 2)}) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:22
.=
(((({(intloc 2)} \/ {(intloc 2),(intloc 1)}) \/ {(intloc 3),(intloc 2)}) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by SF_MASTR:18
.=
((({(intloc 2),(intloc 2),(intloc 1)} \/ {(intloc 3),(intloc 2)}) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:42
.=
((({(intloc 2),(intloc 1)} \/ {(intloc 3),(intloc 2)}) \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:70
.=
(({(intloc 2),(intloc 1),(intloc 3),(intloc 2)} \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:45
.=
(({(intloc 2),(intloc 2),(intloc 3),(intloc 1)} \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:107
.=
(({(intloc 2),(intloc 3),(intloc 1)} \/ {(intloc 3),(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:71
.=
({(intloc 2),(intloc 3),(intloc 1),(intloc 3),(intloc 0 )} \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:49
.=
(({(intloc 2),(intloc 3),(intloc 1),(intloc 3)} \/ {(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:50
.=
(({(intloc 3),(intloc 3),(intloc 1),(intloc 2)} \/ {(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:123
.=
(({(intloc 3),(intloc 1),(intloc 2)} \/ {(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4),(intloc 4)}
by ENUMSET1:71
.=
(({(intloc 3),(intloc 1),(intloc 2)} \/ {(intloc 0 )}) \/ {(intloc 3),(intloc 6)}) \/ {(intloc 4)}
by ENUMSET1:69
.=
(({(intloc 3),(intloc 1),(intloc 2)} \/ {(intloc 3),(intloc 6)}) \/ {(intloc 0 )}) \/ {(intloc 4)}
by XBOOLE_1:4
.=
({(intloc 3),(intloc 1),(intloc 2),(intloc 3),(intloc 6)} \/ {(intloc 0 )}) \/ {(intloc 4)}
by ENUMSET1:49
.=
(({(intloc 3),(intloc 1),(intloc 2),(intloc 3)} \/ {(intloc 6)}) \/ {(intloc 0 )}) \/ {(intloc 4)}
by ENUMSET1:50
.=
(({(intloc 3),(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6)}) \/ {(intloc 0 )}) \/ {(intloc 4)}
by ENUMSET1:107
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6)}) \/ {(intloc 0 )}) \/ {(intloc 4)}
by ENUMSET1:71
.=
({(intloc 3),(intloc 2),(intloc 1)} \/ ({(intloc 6)} \/ {(intloc 0 )})) \/ {(intloc 4)}
by XBOOLE_1:4
.=
({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 0 )}) \/ {(intloc 4)}
by ENUMSET1:41
.=
{(intloc 3),(intloc 2),(intloc 1)} \/ ({(intloc 6),(intloc 0 )} \/ {(intloc 4)})
by XBOOLE_1:4
.=
{(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 0 ),(intloc 4)}
by ENUMSET1:43
.=
{(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}
by ENUMSET1:98
;
:: thesis: verum
end;
A6:
UsedIntLoc (((((((((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))))) = {(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
proof
thus UsedIntLoc (((((((((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))))) =
(UsedIntLoc ((((((((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 )))))))) \/ (UsedIntLoc (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:31
.=
(UsedIntLoc ((((((((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 )))))))) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by SCMBSORT:31
.=
((UsedIntLoc (((((((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)))) \/ (UsedIntLoc (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 )))))))) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by SF_MASTR:31
.=
((UsedIntLoc (((((((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)))) \/ ({(intloc 5),(intloc 2),(intloc 6),(intloc 4),(intloc 0 )} \/ {(intloc 2)})) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by A4, SCMFSA9A:30
.=
((UsedIntLoc (((((((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)))) \/ {(intloc 2),(intloc 5),(intloc 2),(intloc 6),(intloc 4),(intloc 0 )}) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by ENUMSET1:51
.=
((UsedIntLoc (((((((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)))) \/ ({(intloc 2),(intloc 5),(intloc 2),(intloc 6)} \/ {(intloc 4),(intloc 0 )})) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by ENUMSET1:54
.=
((UsedIntLoc (((((((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)))) \/ ({(intloc 2),(intloc 2),(intloc 5),(intloc 6)} \/ {(intloc 4),(intloc 0 )})) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by ENUMSET1:104
.=
((UsedIntLoc (((((((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)))) \/ ({(intloc 2),(intloc 5),(intloc 6)} \/ {(intloc 4),(intloc 0 )})) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by ENUMSET1:71
.=
((UsedIntLoc (((((((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)))) \/ {(intloc 2),(intloc 5),(intloc 6),(intloc 4),(intloc 0 )}) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by ENUMSET1:49
.=
((UsedIntLoc (((((((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)))) \/ ({(intloc 6),(intloc 4),(intloc 0 )} \/ {(intloc 2),(intloc 5)})) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by ENUMSET1:48
.=
((({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by A5, XBOOLE_1:4
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ ({(intloc 6),(intloc 4),(intloc 0 )} \/ {(intloc 6),(intloc 4),(intloc 0 )})) \/ {(intloc 2),(intloc 5)}) \/ ((UsedIntLoc (((((((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)))) \/ {(intloc 4),(intloc 0 )})
by XBOOLE_1:4
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ({(intloc 3),(intloc 5)} \/ ({(intloc 2),(intloc 0 ),(intloc 6)} \/ {(intloc 4),(intloc 0 )}))
by A1, XBOOLE_1:4
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ({(intloc 3),(intloc 5)} \/ {(intloc 2),(intloc 0 ),(intloc 6),(intloc 4),(intloc 0 )})
by ENUMSET1:49
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ({(intloc 3),(intloc 5)} \/ ({(intloc 2)} \/ {(intloc 0 ),(intloc 6),(intloc 4),(intloc 0 )}))
by ENUMSET1:47
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ({(intloc 3),(intloc 5)} \/ ({(intloc 2)} \/ {(intloc 0 ),(intloc 0 ),(intloc 4),(intloc 6)}))
by ENUMSET1:107
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ({(intloc 3),(intloc 5)} \/ ({(intloc 2)} \/ {(intloc 0 ),(intloc 4),(intloc 6)}))
by ENUMSET1:71
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ ({(intloc 3),(intloc 5)} \/ {(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)})
by ENUMSET1:44
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 6),(intloc 4),(intloc 0 )}) \/ {(intloc 2),(intloc 5)}) \/ {(intloc 3),(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}
by ENUMSET1:52
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 5),(intloc 2)}) \/ {(intloc 3),(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}
by ENUMSET1:102
.=
({(intloc 3),(intloc 2),(intloc 1)} \/ ({(intloc 0 ),(intloc 4),(intloc 6)} \/ {(intloc 5),(intloc 2)})) \/ {(intloc 3),(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3),(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}
by ENUMSET1:48
.=
({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}) \/ ({(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)} \/ {(intloc 3)})
by ENUMSET1:51
.=
(({(intloc 3),(intloc 2),(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by XBOOLE_1:4
.=
({(intloc 3),(intloc 2),(intloc 1)} \/ ({(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)} \/ {(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)})) \/ {(intloc 3)}
by XBOOLE_1:4
.=
{(intloc 3),(intloc 2),(intloc 1),(intloc 5),(intloc 2),(intloc 0 ),(intloc 4),(intloc 6)} \/ {(intloc 3)}
by ENUMSET1:64
.=
({(intloc 3),(intloc 2),(intloc 1),(intloc 5),(intloc 2)} \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:66
.=
(({(intloc 3)} \/ {(intloc 2),(intloc 1),(intloc 5),(intloc 2)}) \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:47
.=
(({(intloc 3)} \/ {(intloc 2),(intloc 2),(intloc 5),(intloc 1)}) \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:107
.=
(({(intloc 3)} \/ {(intloc 2),(intloc 5),(intloc 1)}) \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:71
.=
({(intloc 3),(intloc 2),(intloc 5),(intloc 1)} \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:44
.=
({(intloc 1),(intloc 5),(intloc 2),(intloc 3)} \/ {(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:125
.=
{(intloc 1),(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4),(intloc 6)} \/ {(intloc 3)}
by ENUMSET1:59
.=
({(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4),(intloc 6)}) \/ {(intloc 3)}
by ENUMSET1:56
.=
({(intloc 1)} \/ ({(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4)} \/ {(intloc 6)})) \/ {(intloc 3)}
by ENUMSET1:55
.=
(({(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4)}) \/ {(intloc 6)}) \/ {(intloc 3)}
by XBOOLE_1:4
.=
(({(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4)}) \/ {(intloc 3)}) \/ {(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 1)} \/ ({(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4)} \/ {(intloc 3)})) \/ {(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 0 ),(intloc 4),(intloc 3)}) \/ {(intloc 6)}
by ENUMSET1:55
.=
({(intloc 1)} \/ ({(intloc 5),(intloc 2)} \/ {(intloc 3),(intloc 0 ),(intloc 4),(intloc 3)})) \/ {(intloc 6)}
by ENUMSET1:52
.=
({(intloc 1)} \/ ({(intloc 5),(intloc 2)} \/ {(intloc 3),(intloc 3),(intloc 4),(intloc 0 )})) \/ {(intloc 6)}
by ENUMSET1:107
.=
({(intloc 1)} \/ ({(intloc 5),(intloc 2)} \/ {(intloc 3),(intloc 4),(intloc 0 )})) \/ {(intloc 6)}
by ENUMSET1:71
.=
({(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 4),(intloc 0 )}) \/ {(intloc 6)}
by ENUMSET1:48
.=
({(intloc 1)} \/ ({(intloc 0 )} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 4)})) \/ {(intloc 6)}
by ENUMSET1:50
.=
(({(intloc 1)} \/ {(intloc 0 )}) \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 4)}) \/ {(intloc 6)}
by XBOOLE_1:4
.=
({(intloc 0 ),(intloc 1)} \/ {(intloc 5),(intloc 2),(intloc 3),(intloc 4)}) \/ {(intloc 6)}
by ENUMSET1:41
.=
({(intloc 0 ),(intloc 1)} \/ {(intloc 2),(intloc 3),(intloc 4),(intloc 5)}) \/ {(intloc 6)}
by ENUMSET1:111
.=
{(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5)} \/ {(intloc 6)}
by ENUMSET1:52
.=
{(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
by ENUMSET1:61
;
:: thesis: verum
end;
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 );
set Uj1 = 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));
thus UsedIntLoc (insert-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)) ';' (SubFrom (intloc 1),(intloc 0 )))) \/ (UsedIntLoc (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:31
.=
(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)) ';' (SubFrom (intloc 1),(intloc 0 )))) \/ ((UsedIntLoc (((((((((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)))))) \/ {(intloc 1),(intloc 0 )})
by SCMBSORT:31
.=
((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 (SubFrom (intloc 1),(intloc 0 )))) \/ ((UsedIntLoc (((((((((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)))))) \/ {(intloc 1),(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 ))) ';' ((intloc 1) :=len f))) \/ {(intloc 1),(intloc 0 )}) \/ ((UsedIntLoc (((((((((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)))))) \/ {(intloc 1),(intloc 0 )})
by SF_MASTR:18
.=
(((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))) \/ {(intloc 1),(intloc 0 )}) \/ {(intloc 1),(intloc 0 )}) \/ (UsedIntLoc (((((((((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 XBOOLE_1:4
.=
((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))) \/ ({(intloc 1),(intloc 0 )} \/ {(intloc 1),(intloc 0 )})) \/ (UsedIntLoc (((((((((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 XBOOLE_1:4
.=
(((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))) \/ {(intloc 1),(intloc 0 )}) \/ (UsedIntLoc (((((((((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:34
.=
((({(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 0 )}) \/ {(intloc 1)}) \/ {(intloc 1),(intloc 0 )}) \/ (UsedIntLoc (((((((((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 A2, SF_MASTR:22
.=
(({(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ ({(intloc 0 )} \/ {(intloc 1)})) \/ {(intloc 1),(intloc 0 )}) \/ (UsedIntLoc (((((((((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 XBOOLE_1:4
.=
(({(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ {(intloc 1),(intloc 0 )}) \/ {(intloc 1),(intloc 0 )}) \/ (UsedIntLoc (((((((((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 ENUMSET1:41
.=
({(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} \/ ({(intloc 1),(intloc 0 )} \/ {(intloc 1),(intloc 0 )})) \/ (UsedIntLoc (((((((((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 XBOOLE_1:4
.=
{(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)}
by A6, ENUMSET1:57
.=
{(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
; :: thesis: verum