fpop_result: THEORY
BEGIN
  IMPORTING ieee_embed, inx

  result_correct(result: bvec[64], OVF, UNF, INX: bit)  %% The deliv result
          (RM: rounding_mode, OVFen, UNFen, db: bit) %% The parameters
          (x: real): %%% The exact result
    bool = 
      LET N=IF db THEN 11 ELSE 8 ENDIF,
        P=IF db THEN 53 ELSE 24 ENDIF IN

   %% 1. The value of the result is correct
      IF NOT (OVF[N,P](x, RM) AND NOT OVFen) THEN
        ieee_number?[N,P](bv2ieee_bv[N,P](result)) AND
        value[N](ieeebv2fact[N,P](bv2ieee_bv[N,P](result))) =
          rd_result[N,P](x, RM, OVFen, UNFen)
      ELSE
        IF (RM=to_nearest OR
          RM=to_pos AND x>=0 OR
          RM=to_neg AND x<=0) THEN
          %% Return \pm infinity
          IF x >= 0 THEN p_inf?[N,P](bv2ieee_bv[N,P](result))
                ELSE n_inf?[N,P](bv2ieee_bv[N,P](result)) ENDIF
        ELSE
          %% Return \pm xmax
          ieee_number?[N,P](bv2ieee_bv[N,P](result)) AND
          IF x >= 0 THEN 
               value[N](ieeebv2fact[N,P](bv2ieee_bv[N,P](result))) = Xmax[N,P]
            ELSE value[N](ieeebv2fact[N,P](bv2ieee_bv[N,P](result))) = -Xmax[N,P] ENDIF
        ENDIF
      ENDIF
   %% 2. The exceptions are correct
      AND OVF=OVF[N,P](x, RM)
      AND UNF=UNF[N,P](x, RM, UNFen)
      AND INX=INX[N,P](x, RM, OVFen, UNFen);

  result_correct_equiv: LEMMA 
       FORALL (result: bvec[64], OVF, UNF, INX: bit)  %% The deliv result
          (RM: rounding_mode, OVFen, UNFen, db: bit) %% The parameters
          (x1,x2: nonzero_real):
      LET N=IF db THEN 11 ELSE 8 ENDIF,
        P=IF db THEN 53 ELSE 24 ENDIF IN
        alpha_eq[eta_hat[IF db THEN 11 ELSE 8 ENDIF](x1)`e-P](x1,x2) AND
        result_correct(result,OVF,UNF,INX)(RM,OVFen,UNFen,db)(x1)
      IMPLIES
        result_correct(result,OVF,UNF,INX)(RM,OVFen,UNFen,db)(x2);

  result_correct_0: LEMMA FORALL(s: bit, RM: rounding_mode, OVFen, UNFen, db: bit):
	  result_correct(fill[1](s) o fill[63](FALSE), FALSE, FALSE, FALSE)
					(RM, OVFen, UNFen, db)(0);

END fpop_result