consider h being State of S such that
A3: d c= h by PBOOLE:156;
d +* p = d by A1, FUNCT_4:80;
then XX: ( d is halting & d is autonomic ) by A1, Def11;
then ProgramPart h halts_on h by A3, Def10;
then consider k1 being Element of NAT such that
A4: Result ((ProgramPart h),h) = Comput ((ProgramPart h),h,k1) and
A5: CurInstr ((ProgramPart h),(Result ((ProgramPart h),h))) = halt S by Def22;
reconsider R = (Result ((ProgramPart h),h)) | (dom 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 d)
let s be State of S; :: thesis: ( d c= s implies R = (Result ((ProgramPart s),s)) | (dom d) )
assume A6: d c= s ; :: thesis: R = (Result ((ProgramPart s),s)) | (dom d)
ProgramPart s halts_on s by A6, Def10, XX;
then consider k2 being Element of NAT such that
A7: Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,k2) and
A8: CurInstr ((ProgramPart s),(Result ((ProgramPart s),s))) = halt S by Def22;

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

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

then Result ((ProgramPart h),h) = Comput ((ProgramPart h),h,k2) by A4, A5, Th6;
hence R = (Result ((ProgramPart s),s)) | (dom d) by A3, A6, A7, Def25, XX; :: thesis: verum

end;

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

then Result ((ProgramPart s),s) = Comput ((ProgramPart s),s,k1) by A7, A8, Th6;
hence R = (Result ((ProgramPart s),s)) | (dom d) by A3, A6, A4, Def25, XX; :: thesis: verum

end;

end;