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 ) = (IC s) + 1 & (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 ) = (IC s) + 1 & (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 ) = (IC s) + 1 & (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 Def3;
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-Data-Loc by AMI_2:def 16;
A1: InsCode I = 11 ;
A2: Exec ((c :=len g),s) = SCM+FSA-Exec-Res (I,S) by SCMFSA_1:def 17
.= SCM+FSA-Chg ((SCM+FSA-Chg (S,(I int_addr3),(len (S . (I coll_addr2))))),((IC S) + 1)) by A1, SCMFSA_1:def 16 ;
hence (Exec ((c :=len g),s)) . (IC ) = (IC s) + 1 by Th1, 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*> ) ;
then A4: I int_addr3 = ml by SCMFSA_I:def 7;
A5: I coll_addr2 = p by A3, SCMFSA_I:def 8;
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-Data-Loc by AMI_2:def 16;
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 Def3;
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