Proof Step: c_0_28

name: c_0_28 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_3 c_0_3 c_0_22 ⊕ typing X1 X6 foldr_type_type fun esk1_4 X1 X6 X3 X4 X4 ⊖ typing X1 foldl_dB_dB app X6 X3 X4 c_0_3->c_0_22 c_0_28 ⊕ typing X1 X6 foldr_type_type fun esk1_4 X1 X6 X3 X4 X4 ⊖ typing X1 foldl_dB_dB app X6 X3 X4 c_0_22->c_0_28 c_0_33 ⊖ typings shift_type e n t2 as esk1_4 shift_type e n t2 app var n a X3 t ⊖ typing shift_type e n t2 foldl_dB_dB app var n cons_dB a X3 t c_0_28->c_0_33

Input Dependencies

c_0_3

Assumptions

c_0_22

Conclusion

c_0_28

Dependents

c_0_33

Formula

! [X1: nat > type,X3: list_dB,X6: dB,X4: type] :
  ( ( typing @ X1 @ X6 @ ( foldr_type_type @ fun @ ( esk1_4 @ X1 @ X6 @ X3 @ X4 ) @ X4 ) )
  | ~ ( typing @ X1 @ ( foldl_dB_dB @ app @ X6 @ X3 ) @ X4 ) )

Source

inference(evalgc,[status(thm)],[c_0_22])