let g be FinSeq-Location ; :: thesis: for c being Int-Location
for s being State of SCM+FSA holds
( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
let c be Int-Location ; :: thesis: for s being State of SCM+FSA holds
( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
let s be State of SCM+FSA; :: thesis: ( (Exec ((c :=len g),s)) . (IC ) = succ (IC s) & (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def5;
reconsider I = c :=len g as Element of SCM+FSA-Instr ;
set S1 = SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))));
reconsider J = 11 as Element of Segm 13 by NAT_1:44;
reconsider ml = c as Element of SCM+FSA-Data-Loc by Def4;
A1: InsCode I = 11 by RECDEF_2:def 1;
A2: Exec ((c :=len g),s) = SCM+FSA-Exec-Res (I,S) by SCMFSA_1:def 16
.= SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))),(succ (IC S))) by A1, SCMFSA_1:def 15 ;
hence (Exec ((c :=len g),s)) . (IC ) = succ (IC s) by Th7, SCMFSA_1:19; :: thesis: ( (Exec ((c :=len g),s)) . c = len (s . g) & ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )
A3: ( I = [J,{},<*ml,p*>] & I `3_3 = <*ml,p*> ) by RECDEF_2:def 3;
then A4: I int_addr3 = ml by SCMFSA_1:def 12;
A5: I coll_addr2 = p by A3, SCMFSA_1:def 13;
thus (Exec ((c :=len g),s)) . c = (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . ml by A2, SCMFSA_1:20
.= len (s . g) by A4, A5, SCMFSA_1:24 ; :: thesis: ( ( for b being Int-Location st b <> c holds
(Exec ((c :=len g),s)) . b = s . b ) & ( for f being FinSeq-Location holds (Exec ((c :=len g),s)) . f = s . f ) )

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

let b be Int-Location ; :: thesis: ( b <> c implies (Exec ((c :=len g),s)) . b = s . b )
reconsider mn = b as Element of SCM+FSA-Data-Loc by Def4;
assume A6: b <> c ; :: thesis: (Exec ((c :=len g),s)) . b = s . b
thus (Exec ((c :=len g),s)) . b = (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . mn by A2, SCMFSA_1:20
.= s . b by A4, A6, SCMFSA_1:25 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (Exec ((c :=len g),s)) . f = s . f
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def5;
thus (Exec ((c :=len g),s)) . f = (SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))) . q by A2, SCMFSA_1:21
.= s . f by SCMFSA_1:26 ; :: thesis: verum