Proof Step: c_0_187

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

Proof State Overview

proof_step c_0_19 ⊕ float_of real_of_float X841 = X841 c_0_153 ⊕ float_of real_of_float X10 = X10 c_0_19->c_0_153 c_0_187 ⊕ float_of real_of_float X10 = X10 c_0_153->c_0_187 c_0_221 ⊕ float2 X1 zero_zero_int = float_of ring_1_of_int_real X1 c_0_187->c_0_221

Input Dependencies

c_0_19

Assumptions

c_0_153

Conclusion

c_0_187

Dependents

c_0_221

Formula

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

Source

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