Proof Step: c_0_19

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

Proof State Overview

proof_step c_0_0 c_0_0 c_0_14 ⊕ thesis ⊖ typing shift_type e i t2 app var n a foldr_type_type fun X7 t ⊖ typings shift_type e i t2 as X7 c_0_0->c_0_14 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_14->c_0_19 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

Input Dependencies

c_0_0

Assumptions

c_0_14

Conclusion

c_0_19

Dependents

c_0_27

Formula

! [X7: list_type] :
  ( 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 ) ) )

Source

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