Proof Step: c_0_97

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

Proof State Overview

proof_step c_0_6 ⊕ times_times_real = ? c_0_90 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_6->c_0_90 c_0_97 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_90->c_0_97 c_0_105 ⊕ times_times_real esk1_0 numeral_numeral_real bit0 one = pi c_0_97->c_0_105 c_0_229 ⊕ X1 = zero_zero_real ⊖ times_times_real pi X1 = zero_zero_real c_0_97->c_0_229

Input Dependencies

c_0_6

Assumptions

c_0_90

Conclusion

c_0_97

Dependents

c_0_105 c_0_229

Formula

! [X5: real,X1: real] :
  ( ( times_times_real @ X1 @ X5 )
  = ( times_times_real @ X5 @ X1 ) )

Source

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