Proof Step: c_0_175

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

Proof State Overview

proof_step c_0_39 ⊕ times_times_real uminus_uminus_real X6 X17 = uminus_uminus_real times_times_real X6 X17 c_0_175 ⊕ times_times_real uminus_uminus_real X2395 X2396 = uminus_uminus_real times_times_real X2395 X2396 c_0_39->c_0_175 c_0_210 ⊕ times_times_real uminus_uminus_real X2 X4 = uminus_uminus_real times_times_real X2 X4 c_0_175->c_0_210

Input Dependencies

c_0_39

Assumptions

c_0_39

Conclusion

c_0_175

Dependents

c_0_210

Formula

! [X2395: real,X2396: real] :
  ( ( times_times_real @ ( uminus_uminus_real @ X2395 ) @ X2396 )
  = ( uminus_uminus_real @ ( times_times_real @ X2395 @ X2396 ) ) )

Source

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