reconsider R = (Result f,h) | (dom p) as FinPartState of S ;
take R ; :: thesis: for p9 being State of S st p c= p9 holds
R = (Result f,p9) | (dom p)
let p9 be State of S; :: thesis: ( p c= p9 implies R = (Result f,p9) | (dom p) )
assume A3: p c= p9 ; :: thesis: R = (Result f,p9) | (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 p9 by A1, A3, Def9;
then consider k2 being Nat such that
A6: Result f,p9 = Comput f,p9,k2 and
A7: CurInstr f,(Result f,p9) = halt S by Def10;

now

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

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

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

end;

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

then Result f,p9 = Comput f,p9,k1 by A6, A7, Th7;
hence R = (Result f,p9) | (dom p) by A2, A3, A4, Def7; :: thesis: verum

end;

end;

end;

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