Proof Step: c_0_318

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

Proof State Overview

proof_step c_0_13 c_0_13 c_0_151 ⊕ X1 = zero_zero_real ⊕ X5 = zero_zero_real ⊖ times_times_real X1 X5 = zero_zero_real c_0_13->c_0_151 c_0_38 ⊕ semiri2110766477t_real times_times_nat X14 X23 = times_times_real semiri2110766477t_real X14 semiri2110766477t_real X23 c_0_274 ⊕ times_times_real semiri2110766477t_real X2 semiri2110766477t_real X7 = semiri2110766477t_real times_times_nat X2 X7 c_0_38->c_0_274 c_0_318 ⊕ semiri2110766477t_real X2 = zero_zero_real ⊕ semiri2110766477t_real X7 = zero_zero_real ⊖ semiri2110766477t_real times_times_nat X7 X2 = zero_zero_real c_0_151->c_0_318 c_0_274->c_0_318 c_0_323 ⊕ $false c_0_318->c_0_323

Input Dependencies

c_0_13 c_0_38

Assumptions

c_0_151 c_0_274

Conclusion

c_0_318

Dependents

c_0_323

Formula

! [X7: nat,X2: nat] :
  ( ( ( semiri2110766477t_real @ X2 )
    = zero_zero_real )
  | ( ( semiri2110766477t_real @ X7 )
    = zero_zero_real )
  | ( ( semiri2110766477t_real @ ( times_times_nat @ X7 @ X2 ) )
   != zero_zero_real ) )

Source

inference(evalgc,[status(thm)],[inference(spm,[status(thm)],[c_0_151,c_0_274])])