let s be State of SCM+FSA; 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; 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; ( (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 (IExec ((swap (a,b)),P,s)) . b = s . a
per cases
( a <> b or a = b )
;
suppose A4:
a <> b
;
(IExec ((swap (a,b)),P,s)) . a = s . bthus (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
;
verum end; suppose A5:
a = b
;
(IExec ((swap (a,b)),P,s)) . a = s . bthus (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
;
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
; verum