Proof Step: c_0_33

name: c_0_33 syntax: thf role: negated_conjecture inference: evalgc

Proof State Overview

proof_step c_0_0 c_0_0 c_0_27 ⊖ typing shift_type e n t2 app var n a foldr_type_type fun X7 t ⊖ typings shift_type e n t2 as X7 c_0_0->c_0_27 c_0_1 ⊕ thesis c_0_1->c_0_27 c_0_2 ⊕ n = i c_0_2->c_0_27 c_0_3 c_0_3 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_3->c_0_28 c_0_4 ⊕ foldl_dB_dB X37 X38 cons_dB X39 X40 = foldl_dB_dB X37 X37 X38 X39 X40 c_0_29 ⊕ foldl_dB_dB X37 X37 X6 X12 X3 = foldl_dB_dB X37 X6 cons_dB X12 X3 c_0_4->c_0_29 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_27->c_0_33 c_0_28->c_0_33 c_0_29->c_0_33 c_0_37 ⊕ $false c_0_33->c_0_37

Input Dependencies

c_0_0 c_0_1 c_0_2 c_0_3 c_0_4

Assumptions

c_0_27 c_0_28 c_0_29

Conclusion

c_0_33

Dependents

c_0_37

Formula

! [X3: list_dB] :
  ( ~ ( 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 ) )

Source

inference(evalgc,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28]),c_0_29])])