Proof Step: c_0_176

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

Proof State Overview

proof_step c_0_33 ⊕ times_times_real = ? c_0_145 ⊕ times_times_real X2092 X2093 = times_times_real X2093 X2092 c_0_33->c_0_145 c_0_176 ⊕ times_times_real X2244 X2245 = times_times_real X2245 X2244 c_0_145->c_0_176 c_0_211 ⊕ times_times_real X2 X4 = times_times_real X4 X2 c_0_176->c_0_211

Input Dependencies

c_0_33

Assumptions

c_0_145

Conclusion

c_0_176

Dependents

c_0_211

Formula

! [X2244: real,X2245: real] :
  ( ( times_times_real @ X2244 @ X2245 )
  = ( times_times_real @ X2245 @ X2244 ) )

Source

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