Proof Step: c_0_60

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

Proof State Overview

proof_step c_0_4 ⊖ zero_zero_real = numeral_numeral_real X11 c_0_60 ⊖ zero_zero_real = numeral_numeral_real X2193 c_0_4->c_0_60 c_0_69 ⊖ zero_zero_real = numeral_numeral_real X8 c_0_60->c_0_69

Input Dependencies

c_0_4

Assumptions

c_0_4

Conclusion

c_0_60

Dependents

c_0_69

Formula

! [X2193: num] :
  ( zero_zero_real
 != ( numeral_numeral_real @ X2193 ) )

Source

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