Proof Step: c_0_9

name: c_0_9 syntax: thf role: negated_conjecture inference: variable_rename

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 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_9->c_0_14

Input Dependencies

c_0_0

Assumptions

c_0_7

Conclusion

c_0_9

Dependents

c_0_14

Formula

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

Source

inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])