Proof Step: c_0_207

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_77 ⊕ X2 = zero_zero_real ⊖ powr_real X2 X4 = zero_zero_real c_0_0->c_0_77 c_0_4 ⊖ zero_zero_real = numeral_numeral_real X11 c_0_100 ⊖ numeral_numeral_real X8 = zero_zero_real c_0_4->c_0_100 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_207 ⊖ x = zero_zero_real c_0_77->c_0_207 c_0_173->c_0_207 c_0_100->c_0_207 c_0_235 ⊕ ord_less_eq_real powr_real numeral_numeral_real bit0 one zero_zero_real one_one_real c_0_207->c_0_235

Input Dependencies

c_0_0 c_0_4 c_0_26

Assumptions

c_0_77 c_0_173 c_0_100

Conclusion

c_0_207

Dependents

c_0_235

Formula

x != zero_zero_real

Source

inference(evalgc,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_173]),c_0_100])])