Proof Step: c_0_75

name: c_0_75 syntax: thf role: plain inference: distribute

Proof State Overview

proof_step c_0_10 c_0_10 c_0_75 c_0_75 c_0_10->c_0_75 c_0_87 ⊕ X1 = zero_zero_real ⊕ X5 = X6 ⊖ times_times_real X1 X5 = times_times_real X1 X6 c_0_75->c_0_87

Input Dependencies

c_0_10

Assumptions

c_0_10

Conclusion

c_0_75

Dependents

c_0_87

Formula

! [X2211: real,X2212: real,X2213: real] :
  ( ( ( ( times_times_real @ X2211 @ X2212 )
     != ( times_times_real @ X2211 @ X2213 ) )
    | ( X2211 = zero_zero_real )
    | ( X2212 = X2213 ) )
  & ( ( X2211 != zero_zero_real )
    | ( ( times_times_real @ X2211 @ X2212 )
      = ( times_times_real @ X2211 @ X2213 ) ) )
  & ( ( X2212 != X2213 )
    | ( ( times_times_real @ X2211 @ X2212 )
      = ( times_times_real @ X2211 @ X2213 ) ) ) )

Source

inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])