let s be State of SCM+FSA; :: thesis:
let aa, bb be Int-Location; :: thesis:
let f be FinSeq-Location ; :: thesis:
let p be Instruction-Sequence of SCM+FSA; :: thesis:
set a = aa;
set b = bb;
assume that
A1: 1 <= s . aa and
A2: s . aa <= len (s . f) and
A3: 1 <= s . bb and
A4: s . bb <= len (s . f) and
A5: s . (intloc 0) = 1 ; :: thesis:
set aux1 = 1 -stRWNotIn {aa,bb};
set aux2 = 2 -ndRWNotIn {aa,bb};
set i0 = (1 -stRWNotIn {aa,bb}) := (f,aa);
set i1 = (2 -ndRWNotIn {aa,bb}) := (f,bb);
set i2 = (f,aa) := (2 -ndRWNotIn {aa,bb});
set s0 = Initialized s;
set s1 = Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s));
set s2 = IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s);
A6: ( bb = intloc 0 or bb is read-write ) by SCMFSA_M:def 2;
reconsider sa = s . aa as Element of NAT by A1, INT_1:3;
set s0a = |.((Initialized s) . aa).|;
set s2a = |.((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . aa).|;
A7: ( aa = intloc 0 or aa is read-write ) by SCMFSA_M:def 2;
A8: sa = |.(s . aa).| by ABSVALUE:def 1;
then A9: ( (Initialized s) . f = s . f & sa = |.((Initialized s) . aa).| ) by A5, A7, SCMFSA_M:9, SCMFSA_M:37;
reconsider sb = s . bb as Element of NAT by A3, INT_1:3;
A10: sb = |.(s . bb).| by ABSVALUE:def 1;
set s3 = IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb}))),p,s);
A11: 1 -stRWNotIn {aa,bb} <> 2 -ndRWNotIn {aa,bb} by SCMFSA_M:26;
A12: (IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb}))),p,s)) . (1 -stRWNotIn {aa,bb}) = (Exec (((f,aa) := (2 -ndRWNotIn {aa,bb})),(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)))) . (1 -stRWNotIn {aa,bb}) by SCMFSA6C:6
.= (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . (1 -stRWNotIn {aa,bb}) by SCMFSA_2:73
.= (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . (1 -stRWNotIn {aa,bb}) by SCMFSA6C:8
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . (1 -stRWNotIn {aa,bb}) by A11, SCMFSA_2:72
.= ((Initialized s) . f) /. |.((Initialized s) . aa).| by Th4
.= (s . f) . sa by A1, A2, A9, FINSEQ_4:15 ;
set i3 = (f,bb) := (1 -stRWNotIn {aa,bb});
A13: (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . f = (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . f by SCMFSA6C:9
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . f by SCMFSA_2:72 ;
A14: (IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb}))),p,s)) . f = (Exec (((f,aa) := (2 -ndRWNotIn {aa,bb})),(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)))) . f by SCMFSA6C:7
.= ((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . f) +* (|.((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . aa).|,((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . (2 -ndRWNotIn {aa,bb}))) by Th5 ;
A15: bb in {aa,bb} by TARSKI:def 2;
then A16: bb <> 2 -ndRWNotIn {aa,bb} by SCMFSA_M:25;
bb <> 1 -stRWNotIn {aa,bb} by A15, SCMFSA_M:25;
then A17: (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb = (Initialized s) . bb by SCMFSA_2:72
.= s . bb by A5, A6, SCMFSA_M:9, SCMFSA_M:37 ;
A18: aa in {aa,bb} by TARSKI:def 2;
then A19: aa <> 2 -ndRWNotIn {aa,bb} by SCMFSA_M:25;
A20: aa <> 1 -stRWNotIn {aa,bb} by A18, SCMFSA_M:25;
(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . aa = (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . aa by SCMFSA6C:8
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . aa by A19, SCMFSA_2:72
.= (Initialized s) . aa by A20, SCMFSA_2:72 ;
then A21: sa = |.((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . aa).| by A5, A8, A7, SCMFSA_M:9, SCMFSA_M:37;
set s1b = |.((Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb).|;
A22: (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . f = (Initialized s) . f by SCMFSA_2:72
.= s . f by SCMFSA_M:37 ;
A23: (IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb}))),p,s)) . bb = (Exec (((f,aa) := (2 -ndRWNotIn {aa,bb})),(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)))) . bb by SCMFSA6C:6
.= (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . bb by SCMFSA_2:73
.= (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . bb by SCMFSA6C:8
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb by A16, SCMFSA_2:72 ;
A24: (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))),p,s)) . (2 -ndRWNotIn {aa,bb}) = (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . (2 -ndRWNotIn {aa,bb}) by SCMFSA6C:8
.= ((Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . f) /. |.((Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb).| by Th4
.= (s . f) . sb by A3, A4, A10, A22, A17, FINSEQ_4:15 ;
thus (IExec ((swap (f,aa,bb)),p,s)) . f = (Exec (((f,bb) := (1 -stRWNotIn {aa,bb})),(IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ";" ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ";" ((f,aa) := (2 -ndRWNotIn {aa,bb}))),p,s)))) . f by SCMFSA6C:7
.= ((s . f) +* ((s . aa),((s . f) . (s . bb)))) +* ((s . bb),((s . f) . (s . aa))) by A10, A22, A13, A14, A21, A17, A23, A24, A12, Th5 ; :: thesis: