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;

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;