Proof Step: c_0_6

name: c_0_6 syntax: thf role: negated_conjecture inference: evalgc

Proof State Overview

proof_step c_0_0 ⊕ transi72828568clp_dB beta subst r t i subst r t i c_0_4 ⊖ transi72828568clp_dB beta subst r t i subst r t i c_0_0->c_0_4 c_0_6 ⊖ transi72828568clp_dB beta subst r t i subst r t i c_0_4->c_0_6 c_0_8 ⊕ $false c_0_6->c_0_8

Input Dependencies

c_0_0

Assumptions

c_0_4

Conclusion

c_0_6

Dependents

c_0_8

Formula

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

Source

inference(evalgc,[status(thm)],[c_0_4])