Proof Step: c_0_5

name: c_0_5 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Library/0131_Float/prob_00723_022817.p' file node: fact_252_powr__zero__eq__one

Proof State Overview

proof_step c_0_5 c_0_5 c_0_61 c_0_61 c_0_5->c_0_61

Input Dependencies

c_0_5

Assumptions

None

Conclusion

c_0_5

Dependents

c_0_61

Formula

! [X4: real] :
  ( ( ( X4 = zero_zero_real )
   => ( ( powr_real @ X4 @ zero_zero_real )
      = zero_zero_real ) )
  & ( ( X4 != zero_zero_real )
   => ( ( powr_real @ X4 @ zero_zero_real )
      = one_one_real ) ) )

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Library/0131_Float/prob_00723_022817.p',fact_252_powr__zero__eq__one)