Proof Step: c_0_48

name: c_0_48 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_602_real__minus__mult__self__le

Proof State Overview

proof_step c_0_48 ⊕ ord_less_eq_real uminus_uminus_real times_times_real X214 X214 times_times_real X4 X4 c_0_209 ⊕ ord_less_eq_real uminus_uminus_real times_times_real X3486 X3486 times_times_real X3487 X3487 c_0_48->c_0_209

Input Dependencies

c_0_48

Assumptions

None

Conclusion

c_0_48

Dependents

c_0_209

Formula

! [X214: real,X4: real] : ( ord_less_eq_real @ ( uminus_uminus_real @ ( times_times_real @ X214 @ X214 ) ) @ ( times_times_real @ X4 @ X4 ) )

Source

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