Proof Step: c_0_90

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

Proof State Overview

proof_step c_0_15 c_0_15 c_0_90 ⊖ ord_less_eq_real zero_zero_real X3417 ⊖ ord_less_eq_real zero_zero_real X3418 ⊖ ord_less_eq_real X3418 X3419 ⊕ ord_less_eq_real powr_real X3418 X3417 powr_real X3419 X3417 c_0_15->c_0_90 c_0_114 ⊕ ord_less_eq_real powr_real X4 X2 powr_real X6 X2 ⊖ ord_less_eq_real zero_zero_real X2 ⊖ ord_less_eq_real zero_zero_real X4 ⊖ ord_less_eq_real X4 X6 c_0_90->c_0_114

Input Dependencies

c_0_15

Assumptions

c_0_15

Conclusion

c_0_90

Dependents

c_0_114

Formula

! [X3417: real,X3418: real,X3419: real] :
  ( ~ ( ord_less_eq_real @ zero_zero_real @ X3417 )
  | ~ ( ord_less_eq_real @ zero_zero_real @ X3418 )
  | ~ ( ord_less_eq_real @ X3418 @ X3419 )
  | ( ord_less_eq_real @ ( powr_real @ X3418 @ X3417 ) @ ( powr_real @ X3419 @ X3417 ) ) )

Source

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