let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic Exec-preserving steady-programmed AMI-Struct of N
for s being State of S
for i being Instruction of S
for p being NAT -defined FinPartState of holds Exec (i,(s +* p)) = (Exec (i,s)) +* p
let S be non empty stored-program IC-Ins-separated definite realistic Exec-preserving steady-programmed AMI-Struct of N; :: thesis: for s being State of S
for i being Instruction of S
for p being NAT -defined FinPartState of 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 NAT -defined FinPartState of holds Exec (i,(s +* p)) = (Exec (i,s)) +* p
let i be Instruction of S; :: thesis: for p being NAT -defined FinPartState of holds Exec (i,(s +* p)) = (Exec (i,s)) +* p
let p be NAT -defined FinPartState of ; :: 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 )} \/ NAT);
A1: dom p c= NAT by RELAT_1:def 18;
A2: dom s = the carrier of S by PARTFUN1:def 4;
A3: dom (s +* p) = the carrier of S by PARTFUN1:def 4;
A4: dom (Exec (i,s)) = the carrier of S by PARTFUN1:def 4;
A5: dom (Exec (i,(s +* p))) = the carrier of S by PARTFUN1:def 4;
the carrier of S \ ({(IC )} \/ NAT) = ( the carrier of S \ NAT) \ {(IC )} by XBOOLE_1:41;
then A6: ( the carrier of S \ ({(IC )} \/ NAT)) \/ {(IC )} = ( the carrier of S \ NAT) \/ {(IC )} by XBOOLE_1:39;
A7: {(IC )} c= the carrier of S by ZFMISC_1:37;
{(IC )} c= the carrier of S \ NAT

proof

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

end;

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

proof

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

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

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

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

end;

suppose o = IC ; :: thesis: contradiction

then l = IC ;
hence contradiction by COMPOS_1:3; :: thesis: verum

end;

end;

end;

then A15: ( the carrier of S \ ({(IC )} \/ NAT)) \/ {(IC )} misses dom p by A1, XBOOLE_1:63;
then s | ((dom s) \ NAT) = (s +* p) | ((dom (s +* p)) \ NAT) by A2, A3, A10, FUNCT_4:76;
then NPP s = NPP (s +* p) by COMPOS_1:233;
then A16: NPP (Exec (i,s)) = NPP (Exec (i,(s +* p))) by AMISTD_2:def 20;
A17: ((Exec (i,s)) +* p) | (( the carrier of S \ ({(IC )} \/ NAT)) \/ {(IC )}) = (Exec (i,s)) | (( the carrier of S \ ({(IC )} \/ NAT)) \/ {(IC )}) by A15, FUNCT_4:76
.= (Exec (i,(s +* p))) | (( the carrier of S \ ({(IC )} \/ NAT)) \/ {(IC )}) by A4, A5, A10, A16, COMPOS_1:233 ;
A18: ProgramPart (Exec (i,(s +* p))) = ProgramPart (s +* p) by Lm1
.= (ProgramPart s) +* (ProgramPart p) by FUNCT_4:75
.= (ProgramPart (Exec (i,s))) +* (ProgramPart p) by Lm1
.= ProgramPart ((Exec (i,s)) +* p) by FUNCT_4:75 ;
thus Exec (i,(s +* p)) = (Exec (i,(s +* p))) | (({(IC )} \/ ( the carrier of S \ ({(IC )} \/ NAT))) \/ NAT) by A5, A11, RELAT_1:98
.= (((Exec (i,s)) +* p) | ({(IC )} \/ ( the carrier of S \ ({(IC )} \/ NAT)))) +* (((Exec (i,s)) +* p) | NAT) by A17, A18, FUNCT_4:83
.= ((Exec (i,s)) +* p) | (({(IC )} \/ ( the carrier of S \ ({(IC )} \/ NAT))) \/ NAT) by FUNCT_4:83
.= ((Exec (i,s)) +* p) | (dom ((Exec (i,s)) +* p)) by A11, PARTFUN1:def 4
.= (Exec (i,s)) +* p by RELAT_1:98 ; :: thesis: verum