Proof Step: c_0_62

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

Proof State Overview

proof_step c_0_6 ⊕ powr_real powr_real X4 X6 X17 = powr_real X4 times_times_real X6 X17 c_0_62 ⊕ powr_real powr_real X2485 X2486 X2487 = powr_real X2485 times_times_real X2486 X2487 c_0_6->c_0_62 c_0_71 ⊕ powr_real powr_real X2 X4 X6 = powr_real X2 times_times_real X4 X6 c_0_62->c_0_71

Input Dependencies

c_0_6

Assumptions

c_0_6

Conclusion

c_0_62

Dependents

c_0_71

Formula

! [X2485: real,X2486: real,X2487: real] :
  ( ( powr_real @ ( powr_real @ X2485 @ X2486 ) @ X2487 )
  = ( powr_real @ X2485 @ ( times_times_real @ X2486 @ X2487 ) ) )

Source

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