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: