let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b1 -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of S holds IC in dom p
let S be non empty with_non-empty_values IC-Ins-separated halting IC-recognized AMI-Struct over N; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of S holds IC in dom p
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of S holds IC in dom p
let p be non empty q -autonomic FinPartState of S; :: thesis: IC in dom p
A1: dom p meets {(IC )} \/ (Data-Locations ) by MEMSTR_0:41;
per cases ( dom p meets {(IC )} or dom p meets Data-Locations ) by A1, XBOOLE_1:70;
suppose dom p meets {(IC )} ; :: thesis: IC in dom p
hence IC in dom p by ZFMISC_1:50; :: thesis: verum
end;
suppose dom p meets Data-Locations ; :: thesis: IC in dom p
then (dom p) /\ (Data-Locations ) <> {} by XBOOLE_0:def 7;
then DataPart p <> {} by RELAT_1:38, RELAT_1:61;
hence IC in dom p by Th3; :: thesis: verum
end;
end;