Proof Step: c_0_325

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

Proof State Overview

proof_step c_0_25 ⊕ ord_less_eq_real zero_zero_real powr_real X4 X16 c_0_206 ⊕ ord_less_eq_real zero_zero_real powr_real X2 X4 c_0_25->c_0_206 c_0_26 ⊕ x = powr_real numeral_numeral_real bit0 one log numeral_numeral_real bit0 one x c_0_173 ⊕ powr_real numeral_numeral_real bit0 one log numeral_numeral_real bit0 one x = x c_0_26->c_0_173 c_0_325 ⊕ ord_less_eq_real zero_zero_real x c_0_206->c_0_325 c_0_173->c_0_325 c_0_327 ⊕ $false c_0_325->c_0_327

Input Dependencies

c_0_25 c_0_26

Assumptions

c_0_206 c_0_173

Conclusion

c_0_325

Dependents

c_0_327

Formula

ord_less_eq_real @ zero_zero_real @ x

Source

inference(evalgc,[status(thm)],[inference(spm,[status(thm)],[c_0_206,c_0_173])])