Proof Step: c_0_3

name: c_0_3 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_6_list__app__typeD

Proof State Overview

proof_step c_0_3 c_0_3 c_0_12 c_0_12 c_0_3->c_0_12

Input Dependencies

c_0_3

Assumptions

None

Conclusion

c_0_3

Dependents

c_0_12

Formula

! [X1: nat > type,X6: dB,X3: list_dB,X4: type] :
  ( ( typing @ X1 @ ( foldl_dB_dB @ app @ X6 @ X3 ) @ X4 )
 => ? [X7: list_type] :
      ( ( typing @ X1 @ X6 @ ( foldr_type_type @ fun @ X7 @ X4 ) )
      & ( typings @ X1 @ X3 @ X7 ) ) )

Source

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