Proof Step: c_0_9

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

Proof State Overview

proof_step c_0_2 c_0_2 c_0_9 ⊖ ordinal_wo_rel2_b_a X2846 X2847 ⊖ field_b X2846 = bot_bot_set_b ⊕ field_a X2847 = bot_bot_set_a ⊕ ordinal_wo_oexp_b_a X2846 X2847 = bot_bo1798880249_b_a_b c_0_2->c_0_9 c_0_14 ⊕ field_a X2 = bot_bot_set_a ⊕ ordinal_wo_oexp_b_a X3 X2 = bot_bo1798880249_b_a_b ⊖ ordinal_wo_rel2_b_a X3 X2 ⊖ field_b X3 = bot_bot_set_b c_0_9->c_0_14

Input Dependencies

c_0_2

Assumptions

c_0_2

Conclusion

c_0_9

Dependents

c_0_14

Formula

! [X2846: set_Product_prod_b_b,X2847: set_Product_prod_a_a] :
  ( ~ ( ordinal_wo_rel2_b_a @ X2846 @ X2847 )
  | ( ( field_b @ X2846 )
   != bot_bot_set_b )
  | ( ( field_a @ X2847 )
    = bot_bot_set_a )
  | ( ( ordinal_wo_oexp_b_a @ X2846 @ X2847 )
    = bot_bo1798880249_b_a_b ) )

Source

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