Proof Step: c_0_156

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

Proof State Overview

proof_step c_0_30 c_0_30 c_0_156 ⊕ X2423 = zero_zero_real ⊕ divide_divide_real times_times_real X2423 X2424 times_times_real X2425 X2423 = divide_divide_real X2424 X2425 c_0_30->c_0_156 c_0_176 ⊕ X1 = zero_zero_real ⊕ divide_divide_real times_times_real X1 X5 times_times_real X6 X1 = divide_divide_real X5 X6 c_0_156->c_0_176

Input Dependencies

c_0_30

Assumptions

c_0_30

Conclusion

c_0_156

Dependents

c_0_176

Formula

! [X2423: real,X2424: real,X2425: real] :
  ( ( X2423 = zero_zero_real )
  | ( ( divide_divide_real @ ( times_times_real @ X2423 @ X2424 ) @ ( times_times_real @ X2425 @ X2423 ) )
    = ( divide_divide_real @ X2424 @ X2425 ) ) )

Source

inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_30])])