let s be State of SCM+FSA ; :: thesis: for a, b being read-write Int-Location holds
( (IExec (swap a,b),s) . a = s . b & (IExec (swap a,b),s) . b = s . a )
let a, b be read-write Int-Location ; :: thesis: ( (IExec (swap a,b),s) . a = s . b & (IExec (swap a,b),s) . b = s . a )
set i0 = (FirstNotUsed (Macro (a := b))) := a;
set i1 = a := b;
set i2 = b := (FirstNotUsed (Macro (a := b)));
set i01 = ((FirstNotUsed (Macro (a := b))) := a) ';' (a := b);
UsedIntLoc (Macro (a := b)) = UsedIntLoc (a := b) by SF_MASTR:32;
then UsedIntLoc (Macro (a := b)) = {a,b} by SF_MASTR:18;
then A1: not FirstNotUsed (Macro (a := b)) in {a,b} by SF_MASTR:54;
then A2: FirstNotUsed (Macro (a := b)) <> a by TARSKI:def 2;
A3: FirstNotUsed (Macro (a := b)) <> b by A1, TARSKI:def 2;

hereby :: thesis: (IExec (swap a,b),s) . b = s . a

per cases ( a <> b or a = b ) ;

suppose A4: a <> b ; :: thesis: (IExec (swap a,b),s) . a = s . b

thus (IExec (swap a,b),s) . a = (Exec (b := (FirstNotUsed (Macro (a := b)))),(IExec (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)),s)) . a by Th7
.= (IExec (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)),s) . a by A4, SCMFSA_2:89
.= (Exec (a := b),(Exec ((FirstNotUsed (Macro (a := b))) := a),(Initialize s))) . a by Th9
.= (Exec ((FirstNotUsed (Macro (a := b))) := a),(Initialize s)) . b by SCMFSA_2:89
.= (Initialize s) . b by A3, SCMFSA_2:89
.= s . b by Th3 ; :: thesis: verum

end;

suppose A5: a = b ; :: thesis: (IExec (swap a,b),s) . a = s . b

thus (IExec (swap a,b),s) . a = (Exec (b := (FirstNotUsed (Macro (a := b)))),(IExec (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)),s)) . a by Th7
.= (IExec (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)),s) . (FirstNotUsed (Macro (a := b))) by A5, SCMFSA_2:89
.= (Exec (a := b),(Exec ((FirstNotUsed (Macro (a := b))) := a),(Initialize s))) . (FirstNotUsed (Macro (a := b))) by Th9
.= (Exec ((FirstNotUsed (Macro (a := b))) := a),(Initialize s)) . (FirstNotUsed (Macro (a := b))) by A2, SCMFSA_2:89
.= (Initialize s) . a by SCMFSA_2:89
.= s . b by A5, Th3 ; :: thesis: verum

end;

end;

end;

thus (IExec (swap a,b),s) . b = (Exec (b := (FirstNotUsed (Macro (a := b)))),(IExec (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)),s)) . b by Th7
.= (IExec (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)),s) . (FirstNotUsed (Macro (a := b))) by SCMFSA_2:89
.= (Exec (a := b),(Exec ((FirstNotUsed (Macro (a := b))) := a),(Initialize s))) . (FirstNotUsed (Macro (a := b))) by Th9
.= (Exec ((FirstNotUsed (Macro (a := b))) := a),(Initialize s)) . (FirstNotUsed (Macro (a := b))) by A2, SCMFSA_2:89
.= (Initialize s) . a by SCMFSA_2:89
.= s . a by Th3 ; :: thesis: verum