Proof Step: c_0_321

name: c_0_321 syntax: thf role: negated_conjecture inference: evalgc

Proof State Overview

proof_step c_0_33 ⊕ ord_less_eq_real zero_zero_real sin_real divide_divide_real pi semiri2110766477t_real n c_0_310 ⊖ ord_less_eq_real zero_zero_real divide_divide_real pi semiri2110766477t_real n ⊖ ord_less_eq_real semiri2110766477t_real n zero_zero_real c_0_33->c_0_310 c_0_34 c_0_34 c_0_34->c_0_310 c_0_35 c_0_35 c_0_35->c_0_310 c_0_36 c_0_36 c_0_36->c_0_310 c_0_39 c_0_39 c_0_276 ⊕ ord_less_eq_real zero_zero_real divide_divide_real X1 X5 ⊖ ord_less_eq_real zero_zero_real X5 ⊖ ord_less_eq_real zero_zero_real X1 c_0_39->c_0_276 c_0_49 ⊕ ord_less_eq_real zero_zero_real semiri2110766477t_real X23 c_0_301 ⊕ ord_less_eq_real zero_zero_real semiri2110766477t_real X2 c_0_49->c_0_301 c_0_53 ⊕ ord_less_eq_real zero_zero_real pi c_0_53->c_0_310 c_0_294 ⊕ ord_less_eq_real zero_zero_real pi c_0_53->c_0_294 c_0_321 ⊖ ord_less_eq_real semiri2110766477t_real n zero_zero_real c_0_310->c_0_321 c_0_276->c_0_321 c_0_301->c_0_321 c_0_294->c_0_321 c_0_323 ⊕ $false c_0_321->c_0_323

Input Dependencies

c_0_33 c_0_34 c_0_35 c_0_36 c_0_39 c_0_49 c_0_53

Assumptions

c_0_310 c_0_276 c_0_301 c_0_294

Conclusion

c_0_321

Dependents

c_0_323

Formula

~ ( ord_less_eq_real @ ( semiri2110766477t_real @ n ) @ zero_zero_real )

Source

inference(evalgc,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_310,c_0_276]),c_0_301]),c_0_294])])])