let s be State of SCM+FSA; :: thesis:
let aa, bb be Int-Location ; :: thesis:
let f be FinSeq-Location ; :: 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))),s);
A6: ( bb = intloc 0 or not bb is read-only ) by SF_MASTR:def 5;
reconsider sa = s . aa as Element of NAT by A1, INT_1:16;
set s0a = abs ((Initialized s) . aa);
set s2a = abs ((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . aa);
A7: ( aa = intloc 0 or not aa is read-only ) by SF_MASTR:def 5;
A8: sa = abs (s . aa) by ABSVALUE:def 1;
then A9: ( (Initialized s) . f = s . f & sa = abs ((Initialized s) . aa) ) by A5, A7, SCMFSA6C:3;
reconsider sb = s . bb as Element of NAT by A3, INT_1:16;
A10: sb = abs (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}))),s);
A11: 1 -stRWNotIn {aa,bb} <> 2 -ndRWNotIn {aa,bb} by SFMASTR1:22;
A12: (IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ';' ((f,aa) := (2 -ndRWNotIn {aa,bb}))),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))),s)))) . (1 -stRWNotIn {aa,bb}) by SCMFSA6C:7
.= (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . (1 -stRWNotIn {aa,bb}) by SCMFSA_2:99
.= (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . (1 -stRWNotIn {aa,bb}) by SCMFSA6C:9
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . (1 -stRWNotIn {aa,bb}) by A11, SCMFSA_2:98
.= ((Initialized s) . f) /. (abs ((Initialized s) . aa)) by Th11
.= (s . f) . sa by A1, A2, A9, FINSEQ_4:24 ;
set i3 = (f,bb) := (1 -stRWNotIn {aa,bb});
A13: (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . f = (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . f by SCMFSA6C:10
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . f by SCMFSA_2:98 ;
A14: (IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ';' ((f,aa) := (2 -ndRWNotIn {aa,bb}))),s)) . f = (Exec (((f,aa) := (2 -ndRWNotIn {aa,bb})),(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)))) . f by SCMFSA6C:8
.= ((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . f) +* ((abs ((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . aa)),((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . (2 -ndRWNotIn {aa,bb}))) by Th12 ;
A15: bb in {aa,bb} by TARSKI:def 2;
then A16: bb <> 2 -ndRWNotIn {aa,bb} by SFMASTR1:21;
bb <> 1 -stRWNotIn {aa,bb} by A15, SFMASTR1:21;
then A17: (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb = (Initialized s) . bb by SCMFSA_2:98
.= s . bb by A5, A6, SCMFSA6C:3 ;
A18: aa in {aa,bb} by TARSKI:def 2;
then A19: aa <> 2 -ndRWNotIn {aa,bb} by SFMASTR1:21;
A20: aa <> 1 -stRWNotIn {aa,bb} by A18, SFMASTR1:21;
(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . aa = (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . aa by SCMFSA6C:9
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . aa by A19, SCMFSA_2:98
.= (Initialized s) . aa by A20, SCMFSA_2:98 ;
then A21: sa = abs ((IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . aa) by A5, A8, A7, SCMFSA6C:3;
set s1b = abs ((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:98
.= s . f by SCMFSA6C:3 ;
A23: (IExec (((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))) ';' ((f,aa) := (2 -ndRWNotIn {aa,bb}))),s)) . bb = (Exec (((f,aa) := (2 -ndRWNotIn {aa,bb})),(IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)))) . bb by SCMFSA6C:7
.= (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),s)) . bb by SCMFSA_2:99
.= (Exec (((2 -ndRWNotIn {aa,bb}) := (f,bb)),(Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))))) . bb by SCMFSA6C:9
.= (Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb by A16, SCMFSA_2:98 ;
A24: (IExec ((((1 -stRWNotIn {aa,bb}) := (f,aa)) ';' ((2 -ndRWNotIn {aa,bb}) := (f,bb))),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:9
.= ((Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . f) /. (abs ((Exec (((1 -stRWNotIn {aa,bb}) := (f,aa)),(Initialized s))) . bb)) by Th11
.= (s . f) . sb by A3, A4, A10, A22, A17, FINSEQ_4:24 ;
thus (IExec ((swap (f,aa,bb)),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}))),s)))) . f by SCMFSA6C:8
.= ((s . f) +* ((s . aa),((s . f) . (s . bb)))) +* ((s . bb),((s . f) . (s . aa))) by A10, A22, A13, A14, A21, A17, A23, A24, A12, Th12 ; :: thesis: