Proof Step: c_0_56

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_54 c_0_54 c_0_0->c_0_54 c_0_56 ⊕ X2 = zero_zero_real ⊖ powr_real X2 X4 = zero_zero_real c_0_54->c_0_56 c_0_65 ⊕ X2 = zero_zero_real ⊖ powr_real X2 X4 = zero_zero_real c_0_56->c_0_65

Input Dependencies

c_0_0

Assumptions

c_0_54

Conclusion

c_0_56

Dependents

c_0_65

Formula

! [X2: real,X4: real] :
  ( ( X2 = zero_zero_real )
  | ( ( powr_real @ X2 @ X4 )
   != zero_zero_real ) )

Source

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