Proof Step: c_0_287

name: c_0_287 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_27 ⊕ ord_less_float = ? c_0_262 ⊕ ord_less_real real_of_float X10 real_of_float X15 ⊖ ord_less_float X10 X15 c_0_27->c_0_262 c_0_287 ⊕ ord_less_real real_of_float X10 real_of_float X15 ⊖ ord_less_float X10 X15 c_0_262->c_0_287 c_0_307 ⊕ ord_less_real zero_zero_real real_of_float X10 ⊖ ord_less_float zero_zero_float X10 c_0_287->c_0_307

Input Dependencies

c_0_27

Assumptions

c_0_262

Conclusion

c_0_287

Dependents

c_0_307

Formula

! [X10: float,X15: float] :
  ( ( ord_less_real @ ( real_of_float @ X10 ) @ ( real_of_float @ X15 ) )
  | ~ ( ord_less_float @ X10 @ X15 ) )

Source

inference(evalgc,[status(thm)],[c_0_262])