Proof Step: c_0_101

name: c_0_101 syntax: thf role: plain inference: variable_rename

Proof State Overview

proof_step c_0_12 ⊕ times_times_real X11 uminus_uminus_real X15 = uminus_uminus_real times_times_real X11 X15 c_0_101 ⊕ times_times_real X2553 uminus_uminus_real X2554 = uminus_uminus_real times_times_real X2553 X2554 c_0_12->c_0_101 c_0_109 ⊕ times_times_real X1 uminus_uminus_real X5 = uminus_uminus_real times_times_real X1 X5 c_0_101->c_0_109

Input Dependencies

c_0_12

Assumptions

c_0_12

Conclusion

c_0_101

Dependents

c_0_109

Formula

! [X2553: real,X2554: real] :
  ( ( times_times_real @ X2553 @ ( uminus_uminus_real @ X2554 ) )
  = ( uminus_uminus_real @ ( times_times_real @ X2553 @ X2554 ) ) )

Source

inference(variable_rename,[status(thm)],[c_0_12])