Proof Step: c_0_27

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_19 ⊕ thesis ⊖ typings shift_type e i t2 as X7 ⊖ typing shift_type e i t2 app var n a foldr_type_type fun X7 t c_0_0->c_0_19 c_0_1 ⊕ thesis c_0_21 ⊖ thesis c_0_1->c_0_21 c_0_2 ⊕ n = i c_0_20 ⊕ i = n c_0_2->c_0_20 c_0_2->c_0_20 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_19->c_0_27 c_0_20->c_0_27 c_0_20->c_0_27 c_0_21->c_0_27 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

Input Dependencies

c_0_0 c_0_1 c_0_2

Assumptions

c_0_19 c_0_20 c_0_20 c_0_21

Conclusion

c_0_27

Dependents

c_0_33

Formula

! [X7: list_type] :
  ( ~ ( typing @ ( shift_type @ e @ n @ t2 ) @ ( app @ ( var @ n ) @ a ) @ ( foldr_type_type @ fun @ X7 @ t ) )
  | ~ ( typings @ ( shift_type @ e @ n @ t2 ) @ as @ X7 ) )

Source

inference(evalgc,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19,c_0_20]),c_0_20]),c_0_21])])