Proof Step: c_0_236

name: c_0_236 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_32 c_0_32 c_0_204 ⊕ X1 = zero_zero_real ⊕ divide_divide_real X1 X1 = one_one_real c_0_32->c_0_204 c_0_236 ⊕ X1 = zero_zero_real ⊕ divide_divide_real X1 X1 = one_one_real c_0_204->c_0_236 c_0_265 ⊕ divide_divide_real X1 X1 = one_one_real ⊕ X1 = zero_zero_real c_0_236->c_0_265

Input Dependencies

c_0_32

Assumptions

c_0_204

Conclusion

c_0_236

Dependents

c_0_265

Formula

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

Source

inference(evalgc,[status(thm)],[c_0_204])