Proof Step: c_0_4

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

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 c_0_6 ⊖ transi72828568clp_dB beta subst r t i subst r t i c_0_4->c_0_6

Input Dependencies

c_0_0

Assumptions

c_0_2

Conclusion

c_0_4

Dependents

c_0_6

Formula

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

Source

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