Proof Step: c_0_58

name: c_0_58 syntax: thf role: plain inference: fof_simplification

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

Input Dependencies

c_0_2

Assumptions

c_0_2

Conclusion

c_0_58

Dependents

c_0_65

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(fof_simplification,[status(thm)],[c_0_2])