Proof Step: c_0_40

name: c_0_40 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_558_zero__float_Orep__eq

Proof State Overview

proof_step c_0_40 ⊕ real_of_float zero_zero_float = zero_zero_real c_0_178 ⊕ real_of_float zero_zero_float = zero_zero_real c_0_40->c_0_178

Input Dependencies

c_0_40

Assumptions

None

Conclusion

c_0_40

Dependents

c_0_178

Formula

( ( real_of_float @ zero_zero_float )
= zero_zero_real )

Source

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