Proof Step: c_0_249

name: c_0_249 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_8 ⊕ real_of_float float2 X793 X794 = times_times_real ring_1_of_int_real X793 powr_real numeral_numeral_real bit0 one ring_1_of_int_real X794 c_0_219 ⊕ real_of_float float2 archim1031974863r_real times_times_real X2 powr_real numeral_numeral_real bit0 one ring_1_of_int_real X1 uminus_uminus_int X1 = round_down X1 X2 c_0_8->c_0_219 c_0_11 ⊕ ring_1_of_int_real zero_zero_int = zero_zero_real c_0_123 ⊕ ring_1_of_int_real zero_zero_int = zero_zero_real c_0_11->c_0_123 c_0_17 ⊕ round_down = ? c_0_17->c_0_219 c_0_18 ⊕ ring_1_of_int_real uminus_uminus_int X5 = uminus_uminus_real ring_1_of_int_real X5 c_0_18->c_0_219 c_0_37 ⊕ uminus_uminus_int zero_zero_int = zero_zero_int c_0_220 ⊕ uminus_uminus_int zero_zero_int = zero_zero_int c_0_37->c_0_220 c_0_249 ⊕ real_of_float float2 archim1031974863r_real times_times_real X2 powr_real numeral_numeral_real bit0 one zero_zero_real zero_zero_int = round_down zero_zero_int X2 c_0_219->c_0_249 c_0_220->c_0_249 c_0_123->c_0_249 c_0_275 ⊕ round_down zero_zero_int X2 = ring_1_of_int_real archim1031974863r_real X2 c_0_249->c_0_275

Input Dependencies

c_0_8 c_0_11 c_0_17 c_0_18 c_0_37

Assumptions

c_0_219 c_0_220 c_0_123

Conclusion

c_0_249

Dependents

c_0_275

Formula

! [X2: real] :
  ( ( real_of_float @ ( float2 @ ( archim1031974863r_real @ ( times_times_real @ X2 @ ( powr_real @ ( numeral_numeral_real @ ( bit0 @ one ) ) @ zero_zero_real ) ) ) @ zero_zero_int ) )
  = ( round_down @ zero_zero_int @ X2 ) )

Source

inference(evalgc,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_219,c_0_220]),c_0_123])])