Proof Step: c_0_165

name: c_0_165 syntax: thf role: plain inference: evalgc

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_145 ⊕ minus_minus_real divide_divide_real X1 X6 divide_divide_real X5 X6 = divide_divide_real minus_minus_real X1 X5 X6 c_0_16->c_0_145 c_0_165 ⊕ minus_minus_real divide_divide_real X1 X5 divide_divide_real X6 X5 = divide_divide_real minus_minus_real X1 X6 X5 c_0_145->c_0_165 c_0_197 ⊕ uminus_uminus_real divide_divide_real X5 X1 = divide_divide_real uminus_uminus_real X5 X1 c_0_165->c_0_197

Input Dependencies

c_0_16

Assumptions

c_0_145

Conclusion

c_0_165

Dependents

c_0_197

Formula

! [X1: real,X6: real,X5: real] :
  ( ( minus_minus_real @ ( divide_divide_real @ X1 @ X5 ) @ ( divide_divide_real @ X6 @ X5 ) )
  = ( divide_divide_real @ ( minus_minus_real @ X1 @ X6 ) @ X5 ) )

Source

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