Proof Step: c_0_25

name: c_0_25 syntax: thf role: plain inference: split_conjunct

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

Input Dependencies

c_0_5

Assumptions

c_0_5

Conclusion

c_0_25

Dependents

c_0_31

Formula

( rs
= ( cons_dB @ a @ as ) )

Source

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