Proof Step: c_0_146

name: c_0_146 syntax: thf role: plain inference: variable_rename

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 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_237 ⊕ ord_less_real real_of_float X10 real_of_float X15 ⊖ ord_less_float X10 X15 c_0_146->c_0_237

Input Dependencies

c_0_27

Assumptions

c_0_118

Conclusion

c_0_146

Dependents

c_0_177 c_0_237

Formula

! [X3511: float,X3512: float] :
  ( ( ~ ( ord_less_float @ X3511 @ X3512 )
    | ( ord_less_real @ ( real_of_float @ X3511 ) @ ( real_of_float @ X3512 ) ) )
  & ( ~ ( ord_less_real @ ( real_of_float @ X3511 ) @ ( real_of_float @ X3512 ) )
    | ( ord_less_float @ X3511 @ X3512 ) ) )

Source

inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_118])])