Proof Step: c_0_14

name: c_0_14 syntax: thf role: negated_conjecture inference: split_conjunct

Proof State Overview

proof_step c_0_0 c_0_0 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_0->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 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

Input Dependencies

c_0_0

Assumptions

c_0_9

Conclusion

c_0_14

Dependents

c_0_19

Formula

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

Source

inference(split_conjunct,[status(thm)],[c_0_9])