Proof Step: c_0_18

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

Proof State Overview

proof_step c_0_4 ⊕ foldl_dB_dB X37 X38 cons_dB X39 X40 = foldl_dB_dB X37 X37 X38 X39 X40 c_0_13 ⊕ foldl_dB_dB X3430 X3431 cons_dB X3432 X3433 = foldl_dB_dB X3430 X3430 X3431 X3432 X3433 c_0_4->c_0_13 c_0_18 ⊕ foldl_dB_dB X37 X6 cons_dB X12 X3 = foldl_dB_dB X37 X37 X6 X12 X3 c_0_13->c_0_18 c_0_23 ⊕ foldl_dB_dB X37 X37 X6 X12 X3 = foldl_dB_dB X37 X6 cons_dB X12 X3 c_0_18->c_0_23

Input Dependencies

c_0_4

Assumptions

c_0_13

Conclusion

c_0_18

Dependents

c_0_23

Formula

! [X37: dB > dB > dB,X12: dB,X6: dB,X3: list_dB] :
  ( ( foldl_dB_dB @ X37 @ X6 @ ( cons_dB @ X12 @ X3 ) )
  = ( foldl_dB_dB @ X37 @ ( X37 @ X6 @ X12 ) @ X3 ) )

Source

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