let N be with_zero set ; :: thesis:
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis:
thus ( S is IC-recognized implies for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b₁ -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ) :: thesis:

proof

assume A1: S is IC-recognized ; :: thesis:
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis:
let p be q -autonomic FinPartState of S; :: thesis:
assume DataPart p <> {} ; :: thesis:
then not p is empty ;
hence IC in dom p by A1; :: thesis:

end;

assume A2: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b₁ -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ; :: thesis:
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: according to AMISTD_5:def 3 :: thesis:
let p be q -autonomic FinPartState of S; :: thesis:
A3: dom p c= {(IC )} \/ (dom (DataPart p)) by MEMSTR_0:32;
assume A4: not p is empty ; :: thesis:

per cases ;

suppose A5: IC in dom p ; :: thesis:

thus IC in dom p by A5; :: thesis:

end;

suppose not IC in dom p ; :: thesis:

then {(IC )} misses dom p by ZFMISC_1:50;
then not dom (DataPart p) is empty by A4, A3, XBOOLE_1:3, XBOOLE_1:73;
then not DataPart p is empty ;
hence IC in dom p by A2; :: thesis:

end;

end;