Proof Step: c_0_212

name: c_0_212 syntax: thf role: plain inference: split_conjunct

Proof State Overview

proof_step c_0_35 c_0_35 c_0_182 ⊖ ord_less_eq_real X3017 X3018 ⊖ ord_less_eq_real X3019 X3017 ⊕ ord_less_eq_real X3019 X3018 c_0_35->c_0_182 c_0_212 ⊕ ord_less_eq_real X6 X5 ⊖ ord_less_eq_real X1 X5 ⊖ ord_less_eq_real X6 X1 c_0_182->c_0_212 c_0_242 ⊕ ord_less_eq_real X6 X5 ⊖ ord_less_eq_real X6 X1 ⊖ ord_less_eq_real X1 X5 c_0_212->c_0_242

Input Dependencies

c_0_35

Assumptions

c_0_182

Conclusion

c_0_212

Dependents

c_0_242

Formula

! [X6: real,X5: real,X1: real] :
  ( ( ord_less_eq_real @ X6 @ X5 )
  | ~ ( ord_less_eq_real @ X1 @ X5 )
  | ~ ( ord_less_eq_real @ X6 @ X1 ) )

Source

inference(split_conjunct,[status(thm)],[c_0_182])