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 3
.= (UsedIntLoc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ (UsedIntLoc (b := (FirstNotUsed (Macro (a := b))))) by SF_MASTR:30
.= (UsedIntLoc (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b))) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:14
.= ((UsedIntLoc ((FirstNotUsed (Macro (a := b))) := a)) \/ (UsedIntLoc (a := b))) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:31
.= ((UsedIntLoc ((FirstNotUsed (Macro (a := b))) := a)) \/ {a,b}) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:14
.= ({(FirstNotUsed (Macro (a := b))),a} \/ {a,b}) \/ {b,(FirstNotUsed (Macro (a := b)))} by SF_MASTR:14
.= {(FirstNotUsed (Macro (a := b))),a,a,b} \/ {b,(FirstNotUsed (Macro (a := b)))} by ENUMSET1:5
.= {(FirstNotUsed (Macro (a := b))),a,a,b,b,(FirstNotUsed (Macro (a := b)))} by ENUMSET1:14 ;
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