Proof Step: c_0_110

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

Proof State Overview

proof_step c_0_16 ⊕ divide_divide_real minus_minus_real X11 X15 X40 = minus_minus_real divide_divide_real X11 X40 divide_divide_real X15 X40 c_0_110 ⊕ divide_divide_real minus_minus_real X2521 X2522 X2523 = minus_minus_real divide_divide_real X2521 X2523 divide_divide_real X2522 X2523 c_0_16->c_0_110 c_0_125 ⊕ divide_divide_real minus_minus_real X1 X5 X6 = minus_minus_real divide_divide_real X1 X6 divide_divide_real X5 X6 c_0_110->c_0_125

Input Dependencies

c_0_16

Assumptions

c_0_16

Conclusion

c_0_110

Dependents

c_0_125

Formula

! [X2521: real,X2522: real,X2523: real] :
  ( ( divide_divide_real @ ( minus_minus_real @ X2521 @ X2522 ) @ X2523 )
  = ( minus_minus_real @ ( divide_divide_real @ X2521 @ X2523 ) @ ( divide_divide_real @ X2522 @ X2523 ) ) )

Source

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