let g be FinSeq-Location ; :: thesis: for c being Int-Location
for s being State of SCM+FSA holds
( (Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next & ex k being Element of NAT st
( k = abs (s . c) & (Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )
let c be Int-Location ; :: thesis: for s being State of SCM+FSA holds
( (Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next & ex k being Element of NAT st
( k = abs (s . c) & (Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )
let s be State of SCM+FSA ; :: thesis: ( (Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next & ex k being Element of NAT st
( k = abs (s . c) & (Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )
reconsider ml = c as Element of SCM+FSA-Data-Loc by Def4;
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider I = g :=<0,...,0> c as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State ;
reconsider J = 12 as Element of Segm 13 by GR_CY_1:10;
A1: I = [J,<*ml,p*>] ;
A2: InsCode I = 12 by MCART_1:7;
A3: I `2 = <*ml,p*> by MCART_1:7;
consider F being FinSequence of INT , k being Element of NAT such that
A4: k = abs (S . (I int_addr3 )) and
A5: F = k |-> 0 and
A6: SCM+FSA-Exec-Res I,S = SCM+FSA-Chg (SCM+FSA-Chg S,(I coll_addr2 ),F),(succ (IC S)) by A2, SCMFSA_1:def 17;
set S1 = SCM+FSA-Chg S,(I coll_addr2 ),F;
A8: Exec (g :=<0,...,0> c),s = SCM+FSA-Chg (SCM+FSA-Chg S,(I coll_addr2 ),F),(succ (IC S)) by A6, SCMFSA_1:def 18;
hence (Exec (g :=<0,...,0> c),s) . (IC SCM+FSA ) = Next by Th7, SCMFSA_1:20; :: thesis: ( ex k being Element of NAT st
( k = abs (s . c) & (Exec (g :=<0,...,0> c),s) . g = k |-> 0 ) & ( for b being Int-Location holds (Exec (g :=<0,...,0> c),s) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (g :=<0,...,0> c),s) . f = s . f ) )
A9: I coll_addr2 = p by A1, A3, SCMFSA_1:def 14;

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

take k = k; :: thesis: ( k = abs (s . c) & (Exec (g :=<0,...,0> c),s) . g = k |-> 0 )
thus k = abs (s . c) by A1, A3, A4, SCMFSA_1:def 13; :: thesis: (Exec (g :=<0,...,0> c),s) . g = k |-> 0
thus (Exec (g :=<0,...,0> c),s) . g = (SCM+FSA-Chg S,(I coll_addr2 ),F) . p by A8, SCMFSA_1:22
.= k |-> 0 by A5, A9, SCMFSA_1:29 ; :: thesis: verum

end;

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

let b be Int-Location ; :: thesis: (Exec (g :=<0,...,0> c),s) . b = s . b
reconsider mn = b as Element of SCM+FSA-Data-Loc by Def4;
thus (Exec (g :=<0,...,0> c),s) . b = (SCM+FSA-Chg S,(I coll_addr2 ),F) . mn by A8, SCMFSA_1:21
.= s . b by SCMFSA_1:31 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: ( f <> g implies (Exec (g :=<0,...,0> c),s) . f = s . f )
assume A10: f <> g ; :: thesis: (Exec (g :=<0,...,0> c),s) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec (g :=<0,...,0> c),s) . f = (SCM+FSA-Chg S,(I coll_addr2 ),F) . q by A8, SCMFSA_1:22
.= s . f by A9, A10, SCMFSA_1:30 ; :: thesis: verum