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 S)} \/ 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 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;
A7: {(IC S)} c= the carrier of S ;
{(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 A8: x in {(IC S)} ; :: thesis: x in the carrier of S \ NAT
then A9: x = IC S by TARSKI:def 1;
not x in NAT by A9, COMPOS_1:3;
hence x in the carrier of S \ NAT by A8, XBOOLE_0:def 5; :: thesis: verum

end;

then A10: 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 Lm8;
then A11: the carrier of S = ({(IC S)} \/ ( the carrier of S \ ({(IC S)} \/ NAT))) \/ NAT by Lm7;
( 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
A12: o in ( the carrier of S \ ({(IC S)} \/ NAT)) \/ {(IC S)} 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 S)} \/ NAT) or o in {(IC S)} ) by A12, XBOOLE_0:def 3;

per cases ( o in the carrier of S \ ({(IC S)} \/ NAT) or o = IC S ) by A14, 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 A13, XBOOLE_0:def 3; :: thesis: verum

end;

suppose o = IC S ; :: thesis: contradiction

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

end;

end;

end;

then A15: ( the carrier of S \ ({(IC S)} \/ NAT)) \/ {(IC S)} 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 s,s +* p equal_outside NAT by FUNCT_7:def 2;
then A16: Exec (i,s), Exec (i,(s +* p)) equal_outside NAT by AMISTD_2:def 20;
A17: ((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 A15, FUNCT_4:76
.= (Exec (i,(s +* p))) | (( the carrier of S \ ({(IC S)} \/ NAT)) \/ {(IC S)}) by A4, A5, A10, A16, FUNCT_7:def 2 ;
A18: ProgramPart (Exec (i,(s +* p))) = ProgramPart (s +* p) by L117
.= (ProgramPart s) +* (ProgramPart p) by FUNCT_4:75
.= (ProgramPart (Exec (i,s))) +* (ProgramPart p) by L117
.= ProgramPart ((Exec (i,s)) +* p) 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, A11, RELAT_1:98
.= (((Exec (i,s)) +* p) | ({(IC S)} \/ ( the carrier of S \ ({(IC S)} \/ NAT)))) +* (((Exec (i,s)) +* p) | NAT) by A17, A18, 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 A11, PARTFUN1:def 4
.= (Exec (i,s)) +* p by RELAT_1:98 ; :: thesis: verum