Proof Step: c_0_9

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

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 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_9->c_0_12

Input Dependencies

c_0_2

Assumptions

c_0_6

Conclusion

c_0_9

Dependents

c_0_12

Formula

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

Source

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