Proof Step: c_0_291

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

Proof State Overview

proof_step c_0_47 ⊕ times_times_real one_one_real X11 = X11 c_0_267 ⊕ times_times_real one_one_real X1 = X1 c_0_47->c_0_267 c_0_291 ⊕ times_times_real one_one_real X1 = X1 c_0_267->c_0_291 c_0_309 ⊕ times_times_real pi divide_divide_real X1 pi = X1 c_0_291->c_0_309

Input Dependencies

c_0_47

Assumptions

c_0_267

Conclusion

c_0_291

Dependents

c_0_309

Formula

! [X1: real] :
  ( ( times_times_real @ one_one_real @ X1 )
  = X1 )

Source

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