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_00955_041225.p' file node: fact_55_wo__rel2_Ooexp__empty

Proof State Overview

proof_step c_0_2 c_0_2 c_0_9 ⊖ ordinal_wo_rel2_b_a X2846 X2847 ⊖ field_b X2846 = bot_bot_set_b ⊕ field_a X2847 = bot_bot_set_a ⊕ ordinal_wo_oexp_b_a X2846 X2847 = bot_bo1798880249_b_a_b c_0_2->c_0_9

Input Dependencies

c_0_2

Assumptions

None

Conclusion

c_0_2

Dependents

c_0_9

Formula

! [X60: set_Product_prod_b_b,X4: set_Product_prod_a_a] :
  ( ( ordinal_wo_rel2_b_a @ X60 @ X4 )
 => ( ( ( field_b @ X60 )
      = bot_bot_set_b )
   => ( ( ( field_a @ X4 )
       != bot_bot_set_a )
     => ( ( ordinal_wo_oexp_b_a @ X60 @ X4 )
        = bot_bo1798880249_b_a_b ) ) ) )

Source

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