Proof Step: c_0_35

name: c_0_35 syntax: thf role: plain inference: evalgc

Proof State Overview

proof_step c_0_5 ⊕ rs = cons_dB a as c_0_31 ⊕ cons_dB a as = rs c_0_5->c_0_31 c_0_35 ⊕ cons_dB a as = rs c_0_31->c_0_35 c_0_37 ⊕ $false c_0_35->c_0_37 c_0_35->c_0_37

Input Dependencies

c_0_5

Assumptions

c_0_31

Conclusion

c_0_35

Dependents

c_0_37 c_0_37

Formula

( ( cons_dB @ a @ as )
= rs )

Source

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