Proof Step: c_0_177

name: c_0_177 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_177 ⊕ ord_less_float X10 X15 ⊖ ord_less_real real_of_float X10 real_of_float X15 c_0_146->c_0_177 c_0_212 ⊕ ord_less_float X10 X15 ⊖ ord_less_real real_of_float X10 real_of_float X15 c_0_177->c_0_212

Input Dependencies

c_0_27

Assumptions

c_0_146

Conclusion

c_0_177

Dependents

c_0_212

Formula

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

Source

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