Proof Step: c_0_118

name: c_0_118 syntax: thf role: plain inference: fof_simplification

Proof State Overview

proof_step c_0_27 ⊕ ord_less_float = ? c_0_118 c_0_118 c_0_27->c_0_118 c_0_146 c_0_146 c_0_118->c_0_146

Input Dependencies

c_0_27

Assumptions

c_0_27

Conclusion

c_0_118

Dependents

c_0_146

Formula

! [X2174: float,X2175: float] :
  ( ( ord_less_float @ X2174 @ X2175 )
<=> ( ord_less_real @ ( real_of_float @ X2174 ) @ ( real_of_float @ X2175 ) ) )

Source

inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_27])])