Proof Step: c_0_125

name: c_0_125 syntax: thf role: plain inference: split_conjunct

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 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_125->c_0_145

Input Dependencies

c_0_16

Assumptions

c_0_110

Conclusion

c_0_125

Dependents

c_0_145

Formula

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

Source

inference(split_conjunct,[status(thm)],[c_0_110])