Proof Step: c_0_94

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

Proof State Overview

proof_step c_0_19 ⊕ float_of real_of_float X841 = X841 c_0_94 ⊕ float_of real_of_float X3500 = X3500 c_0_19->c_0_94 c_0_121 ⊕ float_of real_of_float X10 = X10 c_0_94->c_0_121

Input Dependencies

c_0_19

Assumptions

c_0_19

Conclusion

c_0_94

Dependents

c_0_121

Formula

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

Source

inference(variable_rename,[status(thm)],[c_0_19])