Proof Step: c_0_307

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

Proof State Overview

proof_step c_0_27 ⊕ ord_less_float = ? c_0_287 ⊕ ord_less_real real_of_float X10 real_of_float X15 ⊖ ord_less_float X10 X15 c_0_27->c_0_287 c_0_40 ⊕ real_of_float zero_zero_float = zero_zero_real c_0_243 ⊕ real_of_float zero_zero_float = zero_zero_real c_0_40->c_0_243 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 c_0_243->c_0_307 c_0_320 ⊕ ord_less_real zero_zero_real powr_real numeral_numeral_real bit0 one ring_1_of_int_real X1 ⊖ ord_less_float zero_zero_float float2 one_one_int X1 c_0_307->c_0_320

Input Dependencies

c_0_27 c_0_40

Assumptions

c_0_287 c_0_243

Conclusion

c_0_307

Dependents

c_0_320

Formula

! [X10: float] :
  ( ( ord_less_real @ zero_zero_real @ ( real_of_float @ X10 ) )
  | ~ ( ord_less_float @ zero_zero_float @ X10 ) )

Source

inference(evalgc,[status(thm)],[inference(spm,[status(thm)],[c_0_287,c_0_243])])