Proof Step: c_0_55

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

Proof State Overview

proof_step c_0_1 c_0_1 c_0_55 ⊖ ord_less_real zero_zero_real X3405 ⊕ powr_real X3405 semiri2110766477t_real X3406 = power_power_real X3405 X3406 c_0_1->c_0_55 c_0_57 ⊕ powr_real X2 semiri2110766477t_real X9 = power_power_real X2 X9 ⊖ ord_less_real zero_zero_real X2 c_0_55->c_0_57

Input Dependencies

c_0_1

Assumptions

c_0_1

Conclusion

c_0_55

Dependents

c_0_57

Formula

! [X3405: real,X3406: nat] :
  ( ~ ( ord_less_real @ zero_zero_real @ X3405 )
  | ( ( powr_real @ X3405 @ ( semiri2110766477t_real @ X3406 ) )
    = ( power_power_real @ X3405 @ X3406 ) ) )

Source

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