let c be Int-Location ; :: thesis: for s being State of SCM+FSA holds
( (Exec ((c :==1),s)) . (IC ) = succ (IC s) & (Exec ((c :==1),s)) . c = 1 & ( for b being Int-Location st b <> c holds
(Exec ((c :==1),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :==1),s)) . f = s . f ) )
let s be State of SCM+FSA; :: thesis: ( (Exec ((c :==1),s)) . (IC ) = succ (IC s) & (Exec ((c :==1),s)) . c = 1 & ( for b being Int-Location st b <> c holds
(Exec ((c :==1),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :==1),s)) . f = s . f ) )
reconsider d = c as Element of SCM+FSA-Data-Loc by Def4;
reconsider ml = c as Element of SCM+FSA-Data-Loc by Def4;
reconsider I = c :==1 as Element of SCM+FSA-Instr ;
reconsider S = s as SCM+FSA-State by PBOOLE:155;
reconsider J = 13 as Element of Segm 14 by NAT_1:45;
InsCode I = 13 by RECDEF_2:def 1;
then consider C being Integer such that
A2: C = 1 and
A3: SCM+FSA-Exec-Res (I,S) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr),C)),(succ (IC S))) by SCMFSA_1:def 18;
set S1 = SCM+FSA-Chg (S,(I int_addr),C);
A4: Exec ((c :==1),s) = SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr),C)),(succ (IC S))) by A3, SCMFSA_1:def 19;
hence (Exec ((c :==1),s)) . (IC ) = succ (IC s) by Th7, SCMFSA_1:20; :: thesis: ( (Exec ((c :==1),s)) . c = 1 & ( for b being Int-Location st b <> c holds
(Exec ((c :==1),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :==1),s)) . f = s . f ) )
( I = [J,{},<*d*>] & I `3_3 = <*d*> ) by RECDEF_2:def 3;
then A6: I int_addr = d by SCMFSA_1:def 13;

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

thus (Exec ((c :==1),s)) . c = (SCM+FSA-Chg (S,(I int_addr),C)) . d by A4, SCMFSA_1:21
.= 1 by A2, A6, SCMFSA_1:25 ; :: thesis: verum

end;

hereby :: thesis: for f being FinSeq-Location holds (Exec ((c :==1),s)) . f = s . f

let b be Int-Location ; :: thesis: ( b <> c implies (Exec ((c :==1),s)) . b = s . b )
assume Z: b <> c ; :: thesis: (Exec ((c :==1),s)) . b = s . b
reconsider mn = b as Element of SCM+FSA-Data-Loc by Def4;
<*d*> = I `3_3 by RECDEF_2:def 3;
then A: d = I int_addr by SCMFSA_1:def 13;
thus (Exec ((c :==1),s)) . b = (SCM+FSA-Chg (S,(I int_addr),C)) . mn by A4, SCMFSA_1:21
.= s . b by Z, SCMFSA_1:26, A ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec ((c :==1),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec ((c :==1),s)) . f = (SCM+FSA-Chg (S,(I int_addr),C)) . q by A4, SCMFSA_1:22
.= s . f by SCMFSA_1:27 ; :: thesis: verum