Proof Step: c_0_8

name: c_0_8 syntax: thf role: negated_conjecture inference: cn

Proof State Overview

proof_step c_0_0 ⊕ transi72828568clp_dB beta subst r t i subst r t i c_0_6 ⊖ transi72828568clp_dB beta subst r t i subst r t i c_0_0->c_0_6 c_0_1 ⊕ transi72828568clp_dB X49 X50 X50 c_0_7 ⊕ transi72828568clp_dB X15 X1 X1 c_0_1->c_0_7 c_0_8 ⊕ $false c_0_6->c_0_8 c_0_7->c_0_8

Input Dependencies

c_0_0 c_0_1

Assumptions

c_0_6 c_0_7

Conclusion

c_0_8

Dependents

None

Formula

$false

Source

inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_6,c_0_7])])

Useful Info

[proof]