Proof Step: c_0_30

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_23 ⊕ 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_0->c_0_23 c_0_3 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_24 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_3->c_0_24 c_0_4 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_25 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_4->c_0_25 c_0_30 ⊕ ordinal_wo_rel2_b_a bot_bo1343651123od_b_b X2 ⊖ order_998966684r_on_a field_a X2 X2 c_0_23->c_0_30 c_0_24->c_0_30 c_0_25->c_0_30 c_0_33 ⊕ $false c_0_30->c_0_33

Input Dependencies

c_0_0 c_0_3 c_0_4

Assumptions

c_0_23 c_0_24 c_0_25

Conclusion

c_0_30

Dependents

c_0_33

Formula

! [X2: set_Product_prod_a_a] :
  ( ( ordinal_wo_rel2_b_a @ bot_bo1343651123od_b_b @ X2 )
  | ~ ( order_998966684r_on_a @ ( field_a @ X2 ) @ X2 ) )

Source

inference(evalgc,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_24]),c_0_25])])])