let g be FinSeq-Location ; for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c := (g,a)),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
let a, c be Int-Location; for s being State of SCM+FSA holds
( (Exec ((c := (g,a)),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
let s be State of SCM+FSA; ( (Exec ((c := (g,a)),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;
reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = c := (g,a) as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 9 as Element of Segm 13 by NAT_1:44;
InsCode I = 9
;
then consider i being Integer, k being Nat such that
A1:
k = |.(S . (I int_addr2)).|
and
A2:
i = (S . (I coll_addr1)) /. k
and
A3:
SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr1),i)),((IC S) + 1))
by SCMFSA_1:def 16;
set S1 = SCM+FSA-Chg (S,(I int_addr1),i);
A4:
Exec ((c := (g,a)),s) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr1),i)),((IC S) + 1))
by A3, SCMFSA_1:def 17;
hence
(Exec ((c := (g,a)),s)) . (IC ) = (IC s) + 1
by Th1, SCMFSA_1:19; ( ex k being Nat st
( k = |.(s . a).| & (Exec ((c := (g,a)),s)) . c = (s . g) /. k ) & ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
A5:
( I = [J,{},<*ml,p,mk*>] & I `3_3 = <*ml,p,mk*> )
;
then A6:
I int_addr1 = ml
by SCMFSA_I:def 3;
A7:
I coll_addr1 = p
by A5, SCMFSA_I:def 5;
hereby ( ( for b being Int-Location st b <> c holds
(Exec ((c := (g,a)),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f ) )
reconsider k =
k as
Nat ;
take k =
k;
( k = |.(s . a).| & (Exec ((c := (g,a)),s)) . c = (s . g) /. k )thus
k = |.(s . a).|
by A5, A1, SCMFSA_I:def 4;
(Exec ((c := (g,a)),s)) . c = (s . g) /. kthus (Exec ((c := (g,a)),s)) . c =
(SCM+FSA-Chg (S,(I int_addr1),i)) . ml
by A4, SCMFSA_1:20
.=
(s . g) /. k
by A2, A6, A7, SCMFSA_1:24
;
verum
end;
hereby for f being FinSeq-Location holds (Exec ((c := (g,a)),s)) . f = s . f
let b be
Int-Location;
( b <> c implies (Exec ((c := (g,a)),s)) . b = s . b )reconsider mn =
b as
Element of
SCM-Data-Loc by AMI_2:def 16;
assume A8:
b <> c
;
(Exec ((c := (g,a)),s)) . b = s . bthus (Exec ((c := (g,a)),s)) . b =
(SCM+FSA-Chg (S,(I int_addr1),i)) . mn
by A4, SCMFSA_1:20
.=
s . b
by A6, A8, SCMFSA_1:25
;
verum
end;
let f be FinSeq-Location ; (Exec ((c := (g,a)),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;
thus (Exec ((c := (g,a)),s)) . f =
(SCM+FSA-Chg (S,(I int_addr1),i)) . q
by A4, SCMFSA_1:21
.=
s . f
by SCMFSA_1:26
; verum