Proof Step: c_0_69

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

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 c_0_81 ⊖ numeral_numeral_real X8 = zero_zero_real c_0_69->c_0_81

Input Dependencies

c_0_4

Assumptions

c_0_60

Conclusion

c_0_69

Dependents

c_0_81

Formula

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

Source

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