Proof Step: c_0_294

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

Proof State Overview

proof_step c_0_27 ⊕ ord_less_float = ? c_0_270 ⊕ ord_less_float zero_zero_float X10 ⊖ ord_less_real zero_zero_real real_of_float X10 c_0_27->c_0_270 c_0_34 c_0_34 c_0_271 ⊕ ord_less_eq_real X2 X4 ⊕ ord_less_real X4 X2 c_0_34->c_0_271 c_0_40 ⊕ real_of_float zero_zero_float = zero_zero_real c_0_40->c_0_270 c_0_294 ⊕ ord_less_float zero_zero_float X10 ⊕ ord_less_eq_real real_of_float X10 zero_zero_real c_0_270->c_0_294 c_0_271->c_0_294 c_0_313 ⊕ ord_less_eq_real powr_real numeral_numeral_real bit0 one ring_1_of_int_real X1 zero_zero_real ⊕ ord_less_float zero_zero_float float2 one_one_int X1 c_0_294->c_0_313

Input Dependencies

c_0_27 c_0_34 c_0_40

Assumptions

c_0_270 c_0_271

Conclusion

c_0_294

Dependents

c_0_313

Formula

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

Source

inference(evalgc,[status(thm)],[inference(spm,[status(thm)],[c_0_270,c_0_271])])