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:50
.= (UsedInt*Loc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ {} by SF_MASTR:36
.= (UsedInt*Loc ((FirstNotUsed (Macro (a := b))) := a)) \/ (UsedInt*Loc (a := b)) by SF_MASTR:51
.= (UsedInt*Loc ((FirstNotUsed (Macro (a := b))) := a)) \/ {} by SF_MASTR:36
.= {} by SF_MASTR:36 ; :: thesis: verum