let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for s1, s2 being State of S
for p being PartState of S st NPP s1 = NPP s2 & dom p = NAT holds
s1 +* p = s2 +* p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for s1, s2 being State of S
for p being PartState of S st NPP s1 = NPP s2 & dom p = NAT holds
s1 +* p = s2 +* p
let s1, s2 be State of S; :: thesis: for p being PartState of S st NPP s1 = NPP s2 & dom p = NAT holds
s1 +* p = s2 +* p
let p be PartState of S; :: thesis: ( NPP s1 = NPP s2 & dom p = NAT implies s1 +* p = s2 +* p )
assume that
Z1: NPP s1 = NPP s2 and
Z2: dom p = NAT ; :: thesis: s1 +* p = s2 +* p
D: dom (ProgramPart s2) = NAT by Lm2;
C: dom (ProgramPart s1) = NAT by Lm2;
not IC in NAT by Def12;
then A1: {(IC )} misses NAT by ZFMISC_1:56;
A2: dom (DataPart s1) misses NAT by Th137;
A3: dom (DataPart s2) misses NAT by Th137;
dom (NPP s1) = {(IC )} \/ (dom (DataPart s1)) by Th71;
then A: dom (ProgramPart s1) misses dom (NPP s1) by C, A1, A2, XBOOLE_1:70;
dom (NPP s2) = {(IC )} \/ (dom (DataPart s2)) by Th71;
then B: dom (ProgramPart s2) misses dom (NPP s2) by D, A1, A3, XBOOLE_1:70;
thus s1 +* p = ((ProgramPart s1) +* (NPP s1)) +* p by Th184
.= ((NPP s1) +* (ProgramPart s1)) +* p by A, FUNCT_4:36
.= (NPP s1) +* p by C, Z2, FUNCT_4:78
.= (NPP s2) +* p by Z1
.= ((NPP s2) +* (ProgramPart s2)) +* p by D, Z2, FUNCT_4:78
.= ((ProgramPart s2) +* (NPP s2)) +* p by B, FUNCT_4:36
.= s2 +* p by Th184 ; :: thesis: verum