let a, b be Int-Location; :: thesis: UsedI*Loc (swap (a,b)) = {}
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
thus UsedI*Loc (swap (a,b)) = (UsedI*Loc (((FirstNotUsed (Macro (a := b))) := a) ";" (a := b))) \/ (UsedInt*Loc (b := (FirstNotUsed (Macro (a := b))))) by SF_MASTR:46
.= (UsedI*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