consider h being State of S such that
A2: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S such that
B2: p c= H by PBOOLE:145;
C2: d c= h by A2;
A3: p c= H by B2;
A4: ( d is p -halted & d is p -autonomic ) by A1, Def11;
then H halts_on h by Def10, A3, C2;
then consider k1 being Element of NAT such that
A5: Result (H,h) = Comput (H,h,k1) and
A6: CurInstr (H,(Result (H,h))) = halt S by Def8;
reconsider R = (Result (H,h)) | (dom d) as FinPartState of S ;
take R ; :: thesis: for P being Instruction-Sequence of S st p c= P holds
for s being State of S st d c= s holds
R = (Result (P,s)) | (dom d)
let P be Instruction-Sequence of S; :: thesis: ( p c= P implies for s being State of S st d c= s holds
R = (Result (P,s)) | (dom d) )
assume ZD: p c= P ; :: thesis: for s being State of S st d c= s holds
R = (Result (P,s)) | (dom d)
let s be State of S; :: thesis: ( d c= s implies R = (Result (P,s)) | (dom d) )
assume A7: d c= s ; :: thesis: R = (Result (P,s)) | (dom d)
B7: d c= s by A7;
then P halts_on s by Def10, A4, 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: p c= H by B2;

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

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

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

end;

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

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

end;

end;