let g be FinSeq-Location ; :: thesis: for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec (((g,a) := c),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
let a, c be Int-Location; :: thesis: for s being State of SCM+FSA holds
( (Exec (((g,a) := c),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
let s be State of SCM+FSA; :: thesis: ( (Exec (((g,a) := c),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),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 = (g,a) := c as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 10 as Element of Segm 13 by NAT_1:44;
InsCode I = 10 ;
then consider F being FinSequence of INT , k being Nat such that
A1: k = |.(S . (I int_addr2)).| and
A2: F = (S . (I coll_addr1)) +* (k,(S . (I int_addr1))) and
A3: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr1),F)),((IC S) + 1)) by SCMFSA_1:def 16;
set S1 = SCM+FSA-Chg (S,(I coll_addr1),F);
A4: Exec (((g,a) := c),s) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I coll_addr1),F)),((IC S) + 1)) by A3, SCMFSA_1:def 17;
hence (Exec (((g,a) := c),s)) . (IC ) = (IC s) + 1 by Th1, SCMFSA_1:19; :: thesis: ( ex k being Nat st
( k = |.(s . a).| & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
A5: ( I = [J,{},<*ml,p,mk*>] & I `3_3 = <*ml,p,mk*> ) ;
then A6: I coll_addr1 = p by SCMFSA_I:def 5;
A7: I int_addr1 = ml by A5, SCMFSA_I:def 3;

hereby :: thesis: ( ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )

reconsider k = k as Nat ;
take k = k; :: thesis: ( k = |.(s . a).| & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) )
thus k = |.(s . a).| by A5, A1, SCMFSA_I:def 4; :: thesis: (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c))
thus (Exec (((g,a) := c),s)) . g = (SCM+FSA-Chg (S,(I coll_addr1),F)) . p by A4, SCMFSA_1:21
.= (s . g) +* (k,(s . c)) by A2, A7, A6, SCMFSA_1:27 ; :: thesis: verum

end;

hereby :: thesis: for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f

let b be Int-Location; :: thesis: (Exec (((g,a) := c),s)) . b = s . b
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
thus (Exec (((g,a) := c),s)) . b = (SCM+FSA-Chg (S,(I coll_addr1),F)) . mn by A4, SCMFSA_1:20
.= s . b by SCMFSA_1:29 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: ( f <> g implies (Exec (((g,a) := c),s)) . f = s . f )
assume A8: f <> g ; :: thesis: (Exec (((g,a) := c),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;
thus (Exec (((g,a) := c),s)) . f = (SCM+FSA-Chg (S,(I coll_addr1),F)) . q by A4, SCMFSA_1:21
.= s . f by A6, A8, SCMFSA_1:28 ; :: thesis: verum