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 b_{1} -valued finite non halt-free Function

for p being non empty b_{2} -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 b_{1} -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;

for q being NAT -defined the InstructionsF of b

for p being non empty b

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 b

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;

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;then DataPart p <> {} by RELAT_1:38, RELAT_1:61;

hence IC in dom p by Th3; :: thesis: verum