Proof Step: c_0_28

name: c_0_28 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_2 c_0_2 c_0_21 ⊕ field_a X2 = bot_bot_set_a ⊕ ordinal_wo_oexp_b_a X3 X2 = bot_bo1798880249_b_a_b ⊖ field_b X3 = bot_bot_set_b ⊖ ordinal_wo_rel2_b_a X3 X2 c_0_2->c_0_21 c_0_28 ⊕ ordinal_wo_oexp_b_a X3 X2 = bot_bo1798880249_b_a_b ⊕ field_a X2 = bot_bot_set_a ⊖ field_b X3 = bot_bot_set_b ⊖ ordinal_wo_rel2_b_a X3 X2 c_0_21->c_0_28 c_0_32 ⊖ ordinal_wo_rel2_b_a bot_bo1343651123od_b_b r c_0_28->c_0_32

Input Dependencies

c_0_2

Assumptions

c_0_21

Conclusion

c_0_28

Dependents

c_0_32

Formula

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

Source

inference(evalgc,[status(thm)],[c_0_21])