Proof Step: c_0_88

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

Proof State Overview

proof_step c_0_0 ⊕ divide_divide_real pi numeral_numeral_real bit0 one = the_real ? c_0_77 ⊕ the_real ? = divide_divide_real pi numeral_numeral_real bit0 one c_0_0->c_0_77 c_0_2 ⊕ pi = times_times_real numeral_numeral_real bit0 one the_real ? c_0_76 ⊕ times_times_real numeral_numeral_real bit0 one the_real ? = pi c_0_2->c_0_76 c_0_88 ⊕ times_times_real numeral_numeral_real bit0 one divide_divide_real pi numeral_numeral_real bit0 one = pi c_0_76->c_0_88 c_0_77->c_0_88 c_0_96 ⊕ times_times_real numeral_numeral_real bit0 one esk1_0 = pi c_0_88->c_0_96

Input Dependencies

c_0_0 c_0_2

Assumptions

c_0_76 c_0_77

Conclusion

c_0_88

Dependents

c_0_96

Formula

( ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ ( divide_divide_real @ pi @ ( numeral_numeral_real @ ( bit0 @ one ) ) ) )
= pi )

Source

inference(evalgc,[status(thm)],[inference(rw,[status(thm)],[c_0_76,c_0_77])])