Proof Step: c_0_237

name: c_0_237 syntax: thf role: plain inference: split_conjunct

Proof State Overview

proof_step c_0_27 ⊕ ord_less_float = ? c_0_146 c_0_146 c_0_27->c_0_146 c_0_237 ⊕ ord_less_real real_of_float X10 real_of_float X15 ⊖ ord_less_float X10 X15 c_0_146->c_0_237 c_0_262 ⊕ ord_less_real real_of_float X10 real_of_float X15 ⊖ ord_less_float X10 X15 c_0_237->c_0_262

Input Dependencies

c_0_27

Assumptions

c_0_146

Conclusion

c_0_237

Dependents

c_0_262

Formula

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

Source

inference(split_conjunct,[status(thm)],[c_0_146])