let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite realistic Exec-preserving AMI-Struct of NAT ,N
for s being State of S
for i being Instruction of S
for p being programmed FinPartState of S holds Exec i,(s +* p) = (Exec i,s) +* p
let S be non empty stored-program IC-Ins-separated steady-programmed definite realistic Exec-preserving AMI-Struct of NAT ,N; :: thesis: for s being State of S
for i being Instruction of S
for p being programmed FinPartState of S holds Exec i,(s +* p) = (Exec i,s) +* p
let s be State of S; :: thesis: for i being Instruction of S
for p being programmed FinPartState of S holds Exec i,(s +* p) = (Exec i,s) +* p
let i be Instruction of S; :: thesis: for p being programmed FinPartState of S holds Exec i,(s +* p) = (Exec i,s) +* p
let p be programmed FinPartState of S; :: thesis: Exec i,(s +* p) = (Exec i,s) +* p
set C = the carrier of S;
set I = NAT ;
set D = the carrier of S \ ({(IC S)} \/ NAT );
A1: dom p c= NAT by AMI_1:def 40;
A2: dom s = the carrier of S by AMI_1:79;
A3: dom (s +* p) = the carrier of S by AMI_1:79;
A4: dom (Exec i,s) = the carrier of S by AMI_1:79;
A5: dom (Exec i,(s +* p)) = the carrier of S by AMI_1:79;
the carrier of S \ ({(IC S)} \/ NAT ) = (the carrier of S \ NAT ) \ {(IC S)} by XBOOLE_1:41;
then A6: (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} = (the carrier of S \ NAT ) \/ {(IC S)} by XBOOLE_1:39;
X: {(IC S)} c= the carrier of S by ZFMISC_1:37;
{(IC S)} c= the carrier of S \ NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(IC S)} or x in the carrier of S \ NAT )
assume A7: x in {(IC S)} ; :: thesis: x in the carrier of S \ NAT
then A8: x = IC S by TARSKI:def 1;

now

assume x in NAT ; :: thesis: contradiction
then reconsider l = x as Instruction-Location of S by AMI_1:def 4;
l = x ;
hence contradiction by A8, AMI_1:48; :: thesis: verum

end;

hence x in the carrier of S \ NAT by A7, X, XBOOLE_0:def 5; :: thesis: verum

end;

then A9: the carrier of S \ NAT = (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} by A6, XBOOLE_1:12;
NAT c= the carrier of S \ {(IC S)} by Lm5;
then A10: the carrier of S = ({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT ))) \/ NAT by Lm4, X;
(the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} misses NAT

proof

assume not (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} misses NAT ; :: thesis: contradiction
then consider o being set such that
A11: o in (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} and
A12: o in NAT by XBOOLE_0:3;
reconsider l = o as Instruction-Location of S by A12, AMI_1:def 4;
A13: ( o in the carrier of S \ ({(IC S)} \/ NAT ) or o in {(IC S)} ) by A11, XBOOLE_0:def 3;

per cases ( o in the carrier of S \ ({(IC S)} \/ NAT ) or o = IC S ) by A13, TARSKI:def 1;

suppose o in the carrier of S \ ({(IC S)} \/ NAT ) ; :: thesis: contradiction

then not o in {(IC S)} \/ NAT by XBOOLE_0:def 5;
hence contradiction by A12, XBOOLE_0:def 3; :: thesis: verum

end;

suppose o = IC S ; :: thesis: contradiction

then l = IC S ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

end;

end;

then A14: (the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)} misses dom p by A1, XBOOLE_1:63;
s,s +* p equal_outside NAT

proof

thus s | ((dom s) \ NAT ) = (s +* p) | ((dom (s +* p)) \ NAT ) by A2, A3, A9, A14, FUNCT_4:76; :: according to FUNCT_7:def 2 :: thesis: verum

end;

then A15: Exec i,s, Exec i,(s +* p) equal_outside NAT by Def19;
A16: ((Exec i,s) +* p) | ((the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)}) = (Exec i,s) | ((the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)}) by A14, FUNCT_4:76
.= (Exec i,(s +* p)) | ((the carrier of S \ ({(IC S)} \/ NAT )) \/ {(IC S)}) by A4, A5, A9, A15, FUNCT_7:def 2 ;
A17: (Exec i,(s +* p)) | NAT = (s +* p) | NAT by AMI_1:117
.= (s | NAT ) +* (p | NAT ) by FUNCT_4:75
.= ((Exec i,s) | NAT ) +* (p | NAT ) by AMI_1:117
.= ((Exec i,s) +* p) | NAT by FUNCT_4:75 ;
thus Exec i,(s +* p) = (Exec i,(s +* p)) | (({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT ))) \/ NAT ) by A5, A10, RELAT_1:98
.= (((Exec i,s) +* p) | ({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT )))) +* (((Exec i,s) +* p) | NAT ) by A16, A17, FUNCT_4:83
.= ((Exec i,s) +* p) | (({(IC S)} \/ (the carrier of S \ ({(IC S)} \/ NAT ))) \/ NAT ) by FUNCT_4:83
.= ((Exec i,s) +* p) | (dom ((Exec i,s) +* p)) by A10, AMI_1:79
.= (Exec i,s) +* p by RELAT_1:98 ; :: thesis: verum