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 A3: p c= p' ; :: thesis: R = (Result f,p') | (dom p)
f halts_on h by A1, A2, Def9;
then consider k1 being Nat such that
A4: Result f,h = Comput f,h,k1 and
A5: CurInstr f,(Result f,h) = halt S by Def10;
f halts_on p' by A1, A3, Def9;
then consider k2 being Nat such that
A6: Result f,p' = Comput f,p',k2 and
A7: 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 A4, A5, Th7;
hence R = (Result f,p') | (dom p) by A2, A3, 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, A7, Th7;
hence R = (Result f,p') | (dom p) by A2, A3, A4, Def7; :: thesis: verum

end;

end;

end;

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