Proof Step: c_0_153

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

Proof State Overview

proof_step c_0_19 ⊕ float_of real_of_float X841 = X841 c_0_121 ⊕ float_of real_of_float X10 = X10 c_0_19->c_0_121 c_0_153 ⊕ float_of real_of_float X10 = X10 c_0_121->c_0_153 c_0_187 ⊕ float_of real_of_float X10 = X10 c_0_153->c_0_187

Input Dependencies

c_0_19

Assumptions

c_0_121

Conclusion

c_0_153

Dependents

c_0_187

Formula

! [X10: float] :
  ( ( float_of @ ( real_of_float @ X10 ) )
  = X10 )

Source

inference(evalgc,[status(thm)],[c_0_121])