Proof Step: c_0_182

name: c_0_182 syntax: thf role: plain inference: variable_rename

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

Input Dependencies

c_0_35

Assumptions

c_0_35

Conclusion

c_0_182

Dependents

c_0_212

Formula

! [X3017: real,X3018: real,X3019: real] :
  ( ~ ( ord_less_eq_real @ X3017 @ X3018 )
  | ~ ( ord_less_eq_real @ X3019 @ X3017 )
  | ( ord_less_eq_real @ X3019 @ X3018 ) )

Source

inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])