let a, b be Int-Location ; :: thesis: UsedInt*Loc (swap (a,b)) = {}
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
thus UsedInt*Loc (swap (a,b)) = (UsedInt*Loc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ (UsedInt*Loc (b := (FirstNotUsed (Macro (a := b))))) by SF_MASTR:46
.= (UsedInt*Loc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ {} by SF_MASTR:32
.= (UsedInt*Loc ((FirstNotUsed (Macro (a := b))) := a)) \/ (UsedInt*Loc (a := b)) by SF_MASTR:47
.= (UsedInt*Loc ((FirstNotUsed (Macro (a := b))) := a)) \/ {} by SF_MASTR:32
.= {} by SF_MASTR:32 ; :: thesis: verum