Proof Step: c_0_14

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

Proof State Overview

proof_step c_0_0 ⊕ member438542032od_a_a produc603716375od_a_a ordinal_oone insert1116662519od_a_a product_Pair_a_a X80 X80 bot_bo2131659635od_a_a bNF_We1170627973unit_a c_0_11 ⊕ member438542032od_a_a produc603716375od_a_a ordinal_oone insert1116662519od_a_a product_Pair_a_a X2 X2 bot_bo2131659635od_a_a bNF_We1170627973unit_a c_0_0->c_0_11 c_0_1 ⊖ member438542032od_a_a produc603716375od_a_a ordinal_oone r bNF_We1170627973unit_a c_0_13 ⊖ member438542032od_a_a produc603716375od_a_a ordinal_oone r bNF_We1170627973unit_a c_0_1->c_0_13 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_12 ⊕ insert1116662519od_a_a product_Pair_a_a wellorder_wo_zero_a r wellorder_wo_zero_a r bot_bo2131659635od_a_a = r c_0_2->c_0_12 c_0_14 ⊕ $false c_0_11->c_0_14 c_0_12->c_0_14 c_0_13->c_0_14

Input Dependencies

c_0_0 c_0_1 c_0_2

Assumptions

c_0_11 c_0_12 c_0_13

Conclusion

c_0_14

Dependents

None

Formula

$false

Source

inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_11,c_0_12]),c_0_13])

Useful Info

[proof]