Proof Step: c_0_265

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

Proof State Overview

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

Input Dependencies

c_0_32

Assumptions

c_0_236

Conclusion

c_0_265

Dependents

c_0_290

Formula

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

Source

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