Proof Step: c_0_25

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

Proof State Overview

proof_step c_0_4 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_18 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_4->c_0_18 c_0_25 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_18->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_25->c_0_30

Input Dependencies

c_0_4

Assumptions

c_0_18

Conclusion

c_0_25

Dependents

c_0_30

Formula

order_998966685r_on_b @ bot_bot_set_b @ bot_bo1343651123od_b_b

Source

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