Proof Step: c_0_2

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

Proof State Overview

proof_step c_0_0 ⊕ transi72828568clp_dB beta subst r t i subst r t i c_0_2 ⊖ transi72828568clp_dB beta subst r t i subst r t i c_0_0->c_0_2 c_0_4 ⊖ transi72828568clp_dB beta subst r t i subst r t i c_0_2->c_0_4

Input Dependencies

c_0_0

Assumptions

c_0_0

Conclusion

c_0_2

Dependents

c_0_4

Formula

~ ( transi72828568clp_dB @ beta @ ( subst @ r @ t @ i ) @ ( subst @ r @ t @ i ) )

Source

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