consider h being State of S such that
A2: d c= h by PBOOLE:156;
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 A2, Def10, A3;
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 s being State of S st d c= s holds
R = (Result ((ProgramPart s),s)) | (dom (NPP d))
let s be State of S; :: thesis: ( d c= s implies R = (Result ((ProgramPart s),s)) | (dom (NPP d)) )
assume A7: d c= s ; :: thesis: R = (Result ((ProgramPart s),s)) | (dom (NPP d))
ProgramPart d c= ProgramPart s by A7, RELAT_1:105;
then ProgramPart s halts_on s by A7, Def10, A4;
then consider k2 being Element of NAT such that
A8: Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,k2) and
A9: CurInstr ((ProgramPart s),(Result ((ProgramPart s),s))) = halt S by Def8;
A10: ProgramPart d c= ProgramPart h by A2, RELAT_1:105;
A11: ProgramPart d c= ProgramPart s by A7, RELAT_1:105;

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

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

then Result ((ProgramPart h),h) = Comput ((ProgramPart h),h,k2) by A5, A6, Th6;
hence R = (Result ((ProgramPart s),s)) | (dom (NPP d)) by A2, A7, A8, Def9, A4, A10, A11; :: thesis: verum

end;

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

then Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,k1) by A8, A9, Th6;
hence R = (Result ((ProgramPart s),s)) | (dom (NPP d)) by A2, A7, A5, Def9, A4, A10, A11; :: thesis: verum

end;

end;