Proof Step: c_0_31

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

Proof State Overview

proof_step c_0_5 ⊕ rs = cons_dB a as c_0_25 ⊕ rs = cons_dB a as c_0_5->c_0_25 c_0_31 ⊕ cons_dB a as = rs c_0_25->c_0_31 c_0_35 ⊕ cons_dB a as = rs c_0_31->c_0_35

Input Dependencies

c_0_5

Assumptions

c_0_25

Conclusion

c_0_31

Dependents

c_0_35

Formula

( ( cons_dB @ a @ as )
= rs )

Source

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