Proof Step: c_0_7

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_7 ⊖ order_998966685r_on_b field_b X2897 X2897 ⊖ order_998966684r_on_a field_a X2898 X2898 ⊕ ordinal_wo_rel2_b_a X2897 X2898 c_0_0->c_0_7 c_0_10 ⊕ ordinal_wo_rel2_b_a X3 X2 ⊖ order_998966685r_on_b field_b X3 X3 ⊖ order_998966684r_on_a field_a X2 X2 c_0_7->c_0_10

Input Dependencies

c_0_0

Assumptions

c_0_0

Conclusion

c_0_7

Dependents

c_0_10

Formula

! [X2897: set_Product_prod_b_b,X2898: set_Product_prod_a_a] :
  ( ~ ( order_998966685r_on_b @ ( field_b @ X2897 ) @ X2897 )
  | ~ ( order_998966684r_on_a @ ( field_a @ X2898 ) @ X2898 )
  | ( ordinal_wo_rel2_b_a @ X2897 @ X2898 ) )

Source

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