Proof Step: c_0_175

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

Proof State Overview

proof_step c_0_32 c_0_32 c_0_175 c_0_175 c_0_32->c_0_175 c_0_204 ⊕ X1 = zero_zero_real ⊕ divide_divide_real X1 X1 = one_one_real c_0_175->c_0_204

Input Dependencies

c_0_32

Assumptions

c_0_32

Conclusion

c_0_175

Dependents

c_0_204

Formula

! [X2688: real] :
  ( ( ( X2688 != zero_zero_real )
    | ( ( divide_divide_real @ X2688 @ X2688 )
      = zero_zero_real ) )
  & ( ( X2688 = zero_zero_real )
    | ( ( divide_divide_real @ X2688 @ X2688 )
      = one_one_real ) ) )

Source

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