reconsider R = (Result f,h) | (dom p) as FinPartState of S by AMI_1:62;
take R ; :: thesis: for p' being State of S st p c= p' holds
R = (Result f,p') | (dom p)
let p' be State of S; :: thesis: ( p c= p' implies R = (Result f,p') | (dom p) )
assume A4: p c= p' ; :: thesis: R = (Result f,p') | (dom p)
f halts_on h by A1, A10, Def9;
then consider k1 being Element of NAT such that
A5: ( Result f,h = Comput f,h,k1 & CurInstr f,(Result f,h) = halt S ) by Def10;
f halts_on p' by A1, A4, Def9;
then consider k2 being Element of NAT such that
A6: ( Result f,p' = Comput f,p',k2 & CurInstr f,(Result f,p') = halt S ) by Def10;

now

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

suppose k1 <= k2 ; :: thesis: R = (Result f,p') | (dom p)

then Result f,h = Comput f,h,k2 by A5, Th7;
hence R = (Result f,p') | (dom p) by A10, A4, A6, Def7; :: thesis: verum

end;

suppose k1 >= k2 ; :: thesis: R = (Result f,p') | (dom p)

then Result f,p' = Comput f,p',k1 by A6, Th7;
hence R = (Result f,p') | (dom p) by A10, A4, A5, Def7; :: thesis: verum

end;

end;

end;

hence R = (Result f,p') | (dom p) ; :: thesis: verum