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

proof

assume A1: S is IC-recognized ; :: thesis: 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
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being q -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p
let p be q -autonomic FinPartState of S; :: thesis: ( DataPart p <> {} implies IC in dom p )
assume DataPart p <> {} ; :: thesis: IC in dom p
then not p is empty ;
hence IC in dom p by A1; :: thesis: verum

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

per cases ( IC in dom p or not IC in dom p ) ;

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

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

end;

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

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: verum

end;

end;