Proof Step: c_0_33

name: c_0_33 syntax: thf role: plain inference: sr

Proof State Overview

proof_step c_0_0 c_0_0 c_0_30 ⊕ ordinal_wo_rel2_b_a bot_bo1343651123od_b_b X2 ⊖ order_998966684r_on_a field_a X2 X2 c_0_0->c_0_30 c_0_1 ⊕ ordinal_wo_oexp_b_a bot_bo1343651123od_b_b r = bot_bo1798880249_b_a_b c_0_32 ⊖ ordinal_wo_rel2_b_a bot_bo1343651123od_b_b r c_0_1->c_0_32 c_0_2 c_0_2 c_0_2->c_0_32 c_0_3 ⊕ field_b bot_bo1343651123od_b_b = bot_bot_set_b c_0_3->c_0_30 c_0_3->c_0_32 c_0_4 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_4->c_0_30 c_0_5 ⊖ field_a r = bot_bot_set_a c_0_5->c_0_32 c_0_6 ⊕ order_998966684r_on_a field_a r r c_0_31 ⊕ order_998966684r_on_a field_a r r c_0_6->c_0_31 c_0_33 ⊕ $false c_0_30->c_0_33 c_0_31->c_0_33 c_0_32->c_0_33

Input Dependencies

c_0_0 c_0_1 c_0_2 c_0_3 c_0_4 c_0_5 c_0_6

Assumptions

c_0_30 c_0_31 c_0_32

Conclusion

c_0_33

Dependents

None

Formula

$false

Source

inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_31]),c_0_32])

Useful Info

[proof]