Proof Step: c_0_104

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

Proof State Overview

proof_step c_0_10 c_0_10 c_0_95 ⊕ X5 = X6 ⊕ X1 = zero_zero_real ⊖ times_times_real X1 X5 = times_times_real X1 X6 c_0_10->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 c_0_117 ⊕ X1 = numeral_numeral_real bit0 one ⊖ times_times_real esk1_0 X1 = pi c_0_104->c_0_117

Input Dependencies

c_0_10

Assumptions

c_0_95

Conclusion

c_0_104

Dependents

c_0_117

Formula

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

Source

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