Proof Step: c_0_5

name: c_0_5 syntax: thf role: axiom file: '/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Proofs-Lambda/0010_StrongNorm/prob_00123_003167.p' file node: fact_5_local_OCons

Proof State Overview

proof_step c_0_5 ⊕ rs = cons_dB a as c_0_25 ⊕ rs = cons_dB a as c_0_5->c_0_25

Input Dependencies

c_0_5

Assumptions

None

Conclusion

c_0_5

Dependents

c_0_25

Formula

( rs
= ( cons_dB @ a @ as ) )

Source

file('/home/yan/atp/benchmarks/isa/deeper/B-mesh-th0/problems/HOL-Proofs-Lambda/0010_StrongNorm/prob_00123_003167.p',fact_5_local_OCons)