Proof Step: c_0_12

name: c_0_12 syntax: thf role: plain inference: distribute

Proof State Overview

proof_step c_0_3 c_0_3 c_0_12 c_0_12 c_0_3->c_0_12 c_0_17 ⊕ typing X1 X6 foldr_type_type fun esk1_4 X1 X6 X3 X4 X4 ⊖ typing X1 foldl_dB_dB app X6 X3 X4 c_0_12->c_0_17 c_0_24 ⊕ typings X1 X3 esk1_4 X1 X6 X3 X4 ⊖ typing X1 foldl_dB_dB app X6 X3 X4 c_0_12->c_0_24

Input Dependencies

c_0_3

Assumptions

c_0_3

Conclusion

c_0_12

Dependents

c_0_17 c_0_24

Formula

! [X3365: nat > type,X3366: dB,X3367: list_dB,X3368: type] :
  ( ( ( typing @ X3365 @ X3366 @ ( foldr_type_type @ fun @ ( esk1_4 @ X3365 @ X3366 @ X3367 @ X3368 ) @ X3368 ) )
    | ~ ( typing @ X3365 @ ( foldl_dB_dB @ app @ X3366 @ X3367 ) @ X3368 ) )
  & ( ( typings @ X3365 @ X3367 @ ( esk1_4 @ X3365 @ X3366 @ X3367 @ X3368 ) )
    | ~ ( typing @ X3365 @ ( foldl_dB_dB @ app @ X3366 @ X3367 ) @ X3368 ) ) )

Source

inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])