Proof Step: c_0_191

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

Proof State Overview

proof_step c_0_45 ⊕ times_times_real X17 times_times_real X6 X18 = times_times_real X6 times_times_real X17 X18 c_0_191 ⊕ times_times_real X2321 times_times_real X2322 X2323 = times_times_real X2322 times_times_real X2321 X2323 c_0_45->c_0_191 c_0_224 ⊕ times_times_real X2 times_times_real X4 X6 = times_times_real X4 times_times_real X2 X6 c_0_191->c_0_224

Input Dependencies

c_0_45

Assumptions

c_0_45

Conclusion

c_0_191

Dependents

c_0_224

Formula

! [X2321: real,X2322: real,X2323: real] :
  ( ( times_times_real @ X2321 @ ( times_times_real @ X2322 @ X2323 ) )
  = ( times_times_real @ X2322 @ ( times_times_real @ X2321 @ X2323 ) ) )

Source

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