let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N holds
( S is IC-recognized iff for p being autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N; :: thesis: ( S is IC-recognized iff for p being autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )
thus ( S is IC-recognized implies for p being autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ) :: thesis: ( ( for p being 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 p being autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p
let p be autonomic FinPartState of S; :: thesis: ( DataPart p <> {} implies IC in dom p )
assume DataPart p <> {} ; :: thesis: IC in dom p
then not NPP p is empty by COMPOS_1:169, XBOOLE_1:3;
hence IC in dom p by A1, Def3; :: thesis: verum

end;

assume A2: for p being autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p ; :: thesis: S is IC-recognized
let p be autonomic FinPartState of S; :: according to AMISTD_5:def 3 :: thesis: ( not NPP p is empty implies IC in dom p )
A3: dom (NPP p) c= {(IC )} \/ (dom (DataPart p)) by COMPOS_1:171;
assume A4: not NPP p is empty ; :: thesis: IC in dom p

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

suppose A5: IC in dom (NPP p) ; :: thesis: IC in dom p

dom (NPP p) c= dom p by RELAT_1:25;
hence IC in dom p by A5; :: thesis: verum

end;

suppose not IC in dom (NPP p) ; :: thesis: IC in dom p

then {(IC )} misses dom (NPP p) by ZFMISC_1:56;
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;