Proof Step: c_0_95

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

Proof State Overview

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

Input Dependencies

c_0_10

Assumptions

c_0_87

Conclusion

c_0_95

Dependents

c_0_104

Formula

! [X1: real,X5: real,X6: real] :
  ( ( X5 = X6 )
  | ( X1 = zero_zero_real )
  | ( ( times_times_real @ X1 @ X5 )
   != ( times_times_real @ X1 @ X6 ) ) )

Source

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