Proof Step: c_0_190

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

Proof State Overview

proof_step c_0_44 ⊕ times_times_real times_times_real X6 X17 X18 = times_times_real X6 times_times_real X17 X18 c_0_190 ⊕ times_times_real times_times_real X2342 X2343 X2344 = times_times_real X2342 times_times_real X2343 X2344 c_0_44->c_0_190 c_0_223 ⊕ times_times_real times_times_real X2 X4 X6 = times_times_real X2 times_times_real X4 X6 c_0_190->c_0_223

Input Dependencies

c_0_44

Assumptions

c_0_44

Conclusion

c_0_190

Dependents

c_0_223

Formula

! [X2342: real,X2343: real,X2344: real] :
  ( ( times_times_real @ ( times_times_real @ X2342 @ X2343 ) @ X2344 )
  = ( times_times_real @ X2342 @ ( times_times_real @ X2343 @ X2344 ) ) )

Source

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