let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for p being FinPartState of
for d being data-only FinPartState of st IC S in dom p holds
IC (p +* d) = IC p
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for p being FinPartState of
for d being data-only FinPartState of st IC S in dom p holds
IC (p +* d) = IC p
let p be FinPartState of ; :: thesis: for d being data-only FinPartState of st IC S in dom p holds
IC (p +* d) = IC p
let d be data-only FinPartState of ; :: thesis: ( IC S in dom p implies IC (p +* d) = IC p )
assume A1: IC S in dom p ; :: thesis: IC (p +* d) = IC p
A2: not IC S in dom d by Th22;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then IC S in dom (p +* d) by A1, XBOOLE_0:def 3;
hence IC (p +* d) = (p +* d) . (IC S) by AMI_1:def 43
.= p . (IC S) by A2, FUNCT_4:12
.= IC p by A1, AMI_1:def 43 ;
:: thesis: verum