Proof Step: c_0_35

name: c_0_35 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_201_round__down__shift

Proof State Overview

Input Dependencies

c_0_35

Assumptions

None

Conclusion

c_0_35

Dependents

c_0_148

Formula

! [X172: int,X4: real,X173: int] :
  ( ( round_down @ X172 @ ( times_times_real @ X4 @ ( powr_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ ( ring_1_of_int_real @ X173 ) ) ) )
  = ( times_times_real @ ( powr_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ ( ring_1_of_int_real @ X173 ) ) @ ( round_down @ ( plus_plus_int @ X172 @ X173 ) @ X4 ) ) )

Source

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