Proof Step: c_0_114

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

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 c_0_139 ⊕ ord_less_eq_real powr_real X4 X2 powr_real X6 X2 ⊖ ord_less_eq_real X4 X6 ⊖ ord_less_eq_real zero_zero_real X4 ⊖ ord_less_eq_real zero_zero_real X2 c_0_114->c_0_139

Input Dependencies

c_0_15

Assumptions

c_0_90

Conclusion

c_0_114

Dependents

c_0_139

Formula

! [X2: real,X4: real,X6: real] :
  ( ( 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 ) )

Source

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