consider h being State of S such that
A2: d c= h by PBOOLE:141;
consider H being Instruction-Sequence of S such that
A3: p c= H by PBOOLE:145;
A4: ( d is p -halted & d is p -autonomic ) by A1, Def12;
then H halts_on h by A2, A3;
then consider k1 being Nat such that
A5: Result (H,h) = Comput (H,h,k1) and
A6: CurInstr (H,(Result (H,h))) = halt S by Def9;
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 A7: 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 A8: d c= s ; :: thesis: R = (Result (P,s)) | (dom d)
then P halts_on s by A4, A7;
then consider k2 being Nat such that
A9: Result (P,s) = Comput (P,s,k2) and
A10: CurInstr (P,(Result (P,s))) = halt S by Def9;
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, Th5;
hence R = (Result (P,s)) | (dom d) by A9, A4, A3, A7, A8, A2; :: thesis: verum
end;
suppose k1 >= k2 ; :: thesis: R = (Result (P,s)) | (dom d)
then Result (P,s) = Comput (P,s,k1) by A9, A10, Th5;
hence R = (Result (P,s)) | (dom d) by A5, A4, A3, A7, A8, A2; :: thesis: verum
end;
end;