Proof Step: c_0_121

name: c_0_121 syntax: thf role: plain inference: split_conjunct

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 c_0_153 ⊕ float_of real_of_float X10 = X10 c_0_121->c_0_153

Input Dependencies

c_0_19

Assumptions

c_0_94

Conclusion

c_0_121

Dependents

c_0_153

Formula

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

Source

inference(split_conjunct,[status(thm)],[c_0_94])