Proof Step: c_0_6

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

Proof State Overview

proof_step c_0_2 ⊕ r = insert1116662519od_a_a product_Pair_a_a wellorder_wo_zero_a r wellorder_wo_zero_a r bot_bo2131659635od_a_a c_0_6 ⊕ r = insert1116662519od_a_a product_Pair_a_a wellorder_wo_zero_a r wellorder_wo_zero_a r bot_bo2131659635od_a_a c_0_2->c_0_6 c_0_9 ⊕ insert1116662519od_a_a product_Pair_a_a wellorder_wo_zero_a r wellorder_wo_zero_a r bot_bo2131659635od_a_a = r c_0_6->c_0_9

Input Dependencies

c_0_2

Assumptions

c_0_2

Conclusion

c_0_6

Dependents

c_0_9

Formula

( r
= ( insert1116662519od_a_a @ ( product_Pair_a_a @ ( wellorder_wo_zero_a @ r ) @ ( wellorder_wo_zero_a @ r ) ) @ bot_bo2131659635od_a_a ) )

Source

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