Proof Step: c_0_90

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

Proof State Overview

proof_step c_0_6 ⊕ times_times_real = ? c_0_82 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_6->c_0_82 c_0_90 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_82->c_0_90 c_0_97 ⊕ times_times_real X1 X5 = times_times_real X5 X1 c_0_90->c_0_97

Input Dependencies

c_0_6

Assumptions

c_0_82

Conclusion

c_0_90

Dependents

c_0_97

Formula

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

Source

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