Proof Step: c_0_4

name: c_0_4 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/Tutorial/0035_Message/prob_00138_003649.p' file node: fact_99_bot__empty__eq

Proof State Overview

proof_step c_0_4 ⊕ bot_bot_nat_o = ? c_0_14 c_0_14 c_0_4->c_0_14

Input Dependencies

c_0_4

Assumptions

None

Conclusion

c_0_4

Dependents

c_0_14

Formula

( bot_bot_nat_o
= ( ^ [X182: nat] : ( member_nat @ X182 @ bot_bot_set_nat ) ) )

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/Tutorial/0035_Message/prob_00138_003649.p',fact_99_bot__empty__eq)