Proof Step: c_0_7

name: c_0_7 syntax: thf role: negated_conjecture inference: fof_simplification

Proof State Overview

proof_step c_0_0 c_0_0 c_0_7 c_0_7 c_0_0->c_0_7 c_0_9 ⊖ typing shift_type e i t2 app var n a foldr_type_type fun X5544 t ⊖ typings shift_type e i t2 as X5544 ⊕ thesis c_0_7->c_0_9

Input Dependencies

c_0_0

Assumptions

c_0_0

Conclusion

c_0_7

Dependents

c_0_9

Formula

~ ? [X1369: list_type] :
    ( ( typing @ ( shift_type @ e @ i @ t2 ) @ ( app @ ( var @ n ) @ a ) @ ( foldr_type_type @ fun @ X1369 @ t ) )
    & ( typings @ ( shift_type @ e @ i @ t2 ) @ as @ X1369 )
    & ~ thesis )

Source

inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[c_0_0])])