Proof Step: c_0_138

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

Proof State Overview

proof_step c_0_21 ⊖ zero_zero_real = numeral_numeral_real X54 c_0_119 ⊖ zero_zero_real = numeral_numeral_real X2143 c_0_21->c_0_119 c_0_138 ⊖ zero_zero_real = numeral_numeral_real X3 c_0_119->c_0_138 c_0_159 ⊖ numeral_numeral_real X3 = zero_zero_real c_0_138->c_0_159

Input Dependencies

c_0_21

Assumptions

c_0_119

Conclusion

c_0_138

Dependents

c_0_159

Formula

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

Source

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