Proof Step: c_0_65

name: c_0_65 syntax: thf role: plain inference: split_conjunct

Proof State Overview

proof_step c_0_2 ⊕ pi = times_times_real numeral_numeral_real bit0 one the_real ? c_0_58 ⊕ pi = times_times_real numeral_numeral_real bit0 one the_real ? c_0_2->c_0_58 c_0_65 ⊕ pi = times_times_real numeral_numeral_real bit0 one the_real ? c_0_58->c_0_65 c_0_76 ⊕ times_times_real numeral_numeral_real bit0 one the_real ? = pi c_0_65->c_0_76

Input Dependencies

c_0_2

Assumptions

c_0_58

Conclusion

c_0_65

Dependents

c_0_76

Formula

( pi
= ( times_times_real @ ( numeral_numeral_real @ ( bit0 @ one ) )
  @ ( the_real
    @ ^ [Z0: real] :
        ( ( ord_less_eq_real @ zero_zero_real @ Z0 )
        & ( ord_less_eq_real @ Z0 @ ( numeral_numeral_real @ ( bit0 @ one ) ) )
        & ( ( cos_real @ Z0 )
          = zero_zero_real ) ) ) ) )

Source

inference(split_conjunct,[status(thm)],[c_0_58])