Proof Step: c_0_4

name: c_0_4 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_22_foldl__Cons

Proof State Overview

proof_step c_0_4 ⊕ foldl_dB_dB X37 X38 cons_dB X39 X40 = foldl_dB_dB X37 X37 X38 X39 X40 c_0_13 ⊕ foldl_dB_dB X3430 X3431 cons_dB X3432 X3433 = foldl_dB_dB X3430 X3430 X3431 X3432 X3433 c_0_4->c_0_13

Input Dependencies

c_0_4

Assumptions

None

Conclusion

c_0_4

Dependents

c_0_13

Formula

! [X37: dB > dB > dB,X38: dB,X39: dB,X40: list_dB] :
  ( ( foldl_dB_dB @ X37 @ X38 @ ( cons_dB @ X39 @ X40 ) )
  = ( foldl_dB_dB @ X37 @ ( X37 @ X38 @ X39 ) @ X40 ) )

Source

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