let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for p being autonomic FinPartState of S st IC in dom p holds
IC p in dom p
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N; :: thesis: ( S is CurIns-recognized implies for p being autonomic FinPartState of S st IC in dom p holds
IC p in dom p )
assume A1: S is CurIns-recognized ; :: thesis: for p being autonomic FinPartState of S st IC in dom p holds
IC p in dom p
let p be autonomic FinPartState of S; :: thesis: ( IC in dom p implies IC p in dom p )
assume A2: IC in dom p ; :: thesis: IC p in dom p
not dom p c= NAT by A2, COMPOS_1:def 12;
then A3: not p is NAT -defined by RELAT_1:def 18;
consider s being State of S such that
A4: p c= s by PBOOLE:156;
B4: NPP p c= s by A4, XBOOLE_1:1;
set P = the the Instructions of S -valued ManySortedSet of NAT +* (ProgramPart p);
A5: ProgramPart p c= the the Instructions of S -valued ManySortedSet of NAT +* (ProgramPart p) by FUNCT_4:26;
ProgramPart p c= p by RELAT_1:88;
then A6: dom (ProgramPart p) c= dom p by RELAT_1:25;
IC (Comput (( the the Instructions of S -valued ManySortedSet of NAT +* (ProgramPart p)),s,0)) in dom (ProgramPart p) by A5, A3, A1, Def4, B4;
then IC s in dom (ProgramPart p) by EXTPRO_1:3;
then IC s in dom p by A6;
hence IC p in dom p by A4, A2, GRFUNC_1:8; :: thesis: verum