Proof Step: c_0_103

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

Proof State Overview

proof_step c_0_14 ⊕ times_times_real X15 times_times_real X11 X40 = times_times_real X11 times_times_real X15 X40 c_0_103 ⊕ times_times_real X2391 times_times_real X2392 X2393 = times_times_real X2392 times_times_real X2391 X2393 c_0_14->c_0_103 c_0_116 ⊕ times_times_real X1 times_times_real X5 X6 = times_times_real X5 times_times_real X1 X6 c_0_103->c_0_116

Input Dependencies

c_0_14

Assumptions

c_0_14

Conclusion

c_0_103

Dependents

c_0_116

Formula

! [X2391: real,X2392: real,X2393: real] :
  ( ( times_times_real @ X2391 @ ( times_times_real @ X2392 @ X2393 ) )
  = ( times_times_real @ X2392 @ ( times_times_real @ X2391 @ X2393 ) ) )

Source

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