consider h being State of S such that
A2: d c= h by PBOOLE:156;
B2: NPP d c= h by A2, XBOOLE_1:1;
A3: ProgramPart d c= ProgramPart h by A2, RELAT_1:105;
d +* p = d by A1, FUNCT_4:80;
then A4: ( d is halting & d is autonomic ) by A1, Def11;
then ProgramPart h halts_on h by Def10, A3, B2;
then consider k1 being Element of NAT such that
A5: Result ((ProgramPart h),h) = Comput ((ProgramPart h),h,k1) and
A6: CurInstr ((ProgramPart h),(Result ((ProgramPart h),h))) = halt S by Def8;
reconsider R = (Result ((ProgramPart h),h)) | (dom (NPP d)) as FinPartState of S ;
take R ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT st p c= P holds
for s being State of S st d c= s holds
R = (Result (P,s)) | (dom (NPP d))
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( p c= P implies for s being State of S st d c= s holds
R = (Result (P,s)) | (dom (NPP d)) )
assume ZD: p c= P ; :: thesis: for s being State of S st d c= s holds
R = (Result (P,s)) | (dom (NPP d))
let s be State of S; :: thesis: ( d c= s implies R = (Result (P,s)) | (dom (NPP d)) )
assume A7: d c= s ; :: thesis: R = (Result (P,s)) | (dom (NPP d))
B7: NPP d c= s by A7, XBOOLE_1:1;
then P halts_on s by Def10, A4, A1, ZD;
then consider k2 being Element of NAT such that
A8: Result (P,s) = Comput (P,s,k2) and
A9: CurInstr (P,(Result (P,s))) = halt S by Def8;
A10: ProgramPart d c= ProgramPart h by A2, RELAT_1:105;

per cases ( k1 <= k2 or k1 >= k2 ) ;

suppose k1 <= k2 ; :: thesis: R = (Result (P,s)) | (dom (NPP d))

then Result ((ProgramPart h),h) = Comput ((ProgramPart h),h,k2) by A5, A6, Th6;
hence R = (Result (P,s)) | (dom (NPP d)) by A8, Def9, A4, A10, A1, ZD, B2, B7; :: thesis: verum

end;

suppose k1 >= k2 ; :: thesis: R = (Result (P,s)) | (dom (NPP d))

then Result (P,s) = Comput (P,s,k1) by A8, A9, Th6;
hence R = (Result (P,s)) | (dom (NPP d)) by A5, Def9, A4, A10, A1, ZD, B2, B7; :: thesis: verum

end;

end;