Proof Step: c_0_204

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

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 c_0_236 ⊕ X1 = zero_zero_real ⊕ divide_divide_real X1 X1 = one_one_real c_0_204->c_0_236

Input Dependencies

c_0_32

Assumptions

c_0_175

Conclusion

c_0_204

Dependents

c_0_236

Formula

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

Source

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