let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )
let P be Instruction-Sequence of SCM+FSA; :: thesis: for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )
let a, b be read-write Int-Location; :: thesis: ( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,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);
UsedILoc (Macro (a := b)) = UsedIntLoc (a := b) by SF_MASTR:28;
then UsedILoc (Macro (a := b)) = {a,b} by SF_MASTR:14;
then A1: not FirstNotUsed (Macro (a := b)) in {a,b} by SF_MASTR:50;
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)),P,s)) . b = s . a
per cases ( a <> b or a = b ) ;
suppose A4: a <> b ; :: thesis: (IExec ((swap (a,b)),P,s)) . a = s . b
thus (IExec ((swap (a,b)),P,s)) . a = (Exec ((b := (FirstNotUsed (Macro (a := b)))),(IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)))) . a by Th5
.= (IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)) . a by A4, SCMFSA_2:63
.= (Exec ((a := b),(Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))))) . a by Th7
.= (Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))) . b by SCMFSA_2:63
.= (Initialized s) . b by A3, SCMFSA_2:63
.= s . b by SCMFSA_M:37 ; :: thesis: verum
end;
suppose A5: a = b ; :: thesis: (IExec ((swap (a,b)),P,s)) . a = s . b
thus (IExec ((swap (a,b)),P,s)) . a = (Exec ((b := (FirstNotUsed (Macro (a := b)))),(IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)))) . a by Th5
.= (IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)) . (FirstNotUsed (Macro (a := b))) by A5, SCMFSA_2:63
.= (Exec ((a := b),(Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))))) . (FirstNotUsed (Macro (a := b))) by Th7
.= (Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))) . (FirstNotUsed (Macro (a := b))) by A2, SCMFSA_2:63
.= (Initialized s) . a by SCMFSA_2:63
.= s . b by A5, SCMFSA_M:37 ; :: thesis: verum
end;
end;
end;
thus (IExec ((swap (a,b)),P,s)) . b = (Exec ((b := (FirstNotUsed (Macro (a := b)))),(IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)))) . b by Th5
.= (IExec ((((FirstNotUsed (Macro (a := b))) := a) ";" (a := b)),P,s)) . (FirstNotUsed (Macro (a := b))) by SCMFSA_2:63
.= (Exec ((a := b),(Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))))) . (FirstNotUsed (Macro (a := b))) by Th7
.= (Exec (((FirstNotUsed (Macro (a := b))) := a),(Initialized s))) . (FirstNotUsed (Macro (a := b))) by A2, SCMFSA_2:63
.= (Initialized s) . a by SCMFSA_2:63
.= s . a by SCMFSA_M:37 ; :: thesis: verum