Proof Step: c_0_2

name: c_0_2 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Cardinals/0009_Ordinal_Arithmetic/prob_01235_053796.p' file node: fact_23__092_060open_062r_A_061_A_123_Ir_Ozero_M_Ar_Ozero_J_125_092_060close_062

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

Input Dependencies

c_0_2

Assumptions

None

Conclusion

c_0_2

Dependents

c_0_6

Formula

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

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Cardinals/0009_Ordinal_Arithmetic/prob_01235_053796.p',fact_23__092_060open_062r_A_061_A_123_Ir_Ozero_M_Ar_Ozero_J_125_092_060close_062)