Proof Step: c_0_9

name: c_0_9 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_256_dual__order_Otrans

Proof State Overview

proof_step c_0_9 c_0_9 c_0_73 ⊖ ord_less_eq_real X2632 X2633 ⊖ ord_less_eq_real X2634 X2632 ⊕ ord_less_eq_real X2634 X2633 c_0_9->c_0_73

Input Dependencies

c_0_9

Assumptions

None

Conclusion

c_0_9

Dependents

c_0_73

Formula

! [X17: real,X6: real,X18: real] :
  ( ( ord_less_eq_real @ X17 @ X6 )
 => ( ( ord_less_eq_real @ X18 @ X17 )
   => ( ord_less_eq_real @ X18 @ X6 ) ) )

Source

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