Proof Step: c_0_12

name: c_0_12 syntax: thf role: plain inference: split_conjunct

Proof State Overview

proof_step c_0_4 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_12 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_4->c_0_12 c_0_18 ⊕ order_998966685r_on_b bot_bot_set_b bot_bo1343651123od_b_b c_0_12->c_0_18

Input Dependencies

c_0_4

Assumptions

c_0_4

Conclusion

c_0_12

Dependents

c_0_18

Formula

order_998966685r_on_b @ bot_bot_set_b @ bot_bo1343651123od_b_b

Source

inference(split_conjunct,[status(thm)],[c_0_4])