let a, b be Int-Location ; :: thesis: ( a in UsedIntLoc (swap a,b) & b in UsedIntLoc (swap a,b) )
set FNU = FirstNotUsed (Macro (a := b));
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
A1: UsedIntLoc (swap a,b) = UsedIntLoc ((((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))))) by SCMFSA6C:def 4
.= (UsedIntLoc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ (UsedIntLoc (b := (FirstNotUsed (Macro (a := b))))) by SF_MASTR:34
.= (UsedIntLoc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:18
.= ((UsedIntLoc ((FirstNotUsed (Macro (a := b))) := a)) \/ (UsedIntLoc (a := b))) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:35
.= ((UsedIntLoc ((FirstNotUsed (Macro (a := b))) := a)) \/ {a,b}) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:18
.= ({(FirstNotUsed (Macro (a := b))),a} \/ {a,b}) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:18
.= {(FirstNotUsed (Macro (a := b))),a,a,b} \/ {b,(FirstNotUsed (Macro (a := b)))} by ENUMSET1:45
.= {(FirstNotUsed (Macro (a := b))),a,a,b,b,(FirstNotUsed (Macro (a := b)))} by ENUMSET1:54 ;
hence a in UsedIntLoc (swap a,b) by ENUMSET1:def 4; :: thesis: b in UsedIntLoc (swap a,b)
thus b in UsedIntLoc (swap a,b) by A1, ENUMSET1:def 4; :: thesis: verum