Proof Step: c_0_29

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

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_23 ⊕ foldl_dB_dB X37 X37 X6 X12 X3 = foldl_dB_dB X37 X6 cons_dB X12 X3 c_0_4->c_0_23 c_0_29 ⊕ foldl_dB_dB X37 X37 X6 X12 X3 = foldl_dB_dB X37 X6 cons_dB X12 X3 c_0_23->c_0_29 c_0_33 ⊖ typings shift_type e n t2 as esk1_4 shift_type e n t2 app var n a X3 t ⊖ typing shift_type e n t2 foldl_dB_dB app var n cons_dB a X3 t c_0_29->c_0_33 c_0_37 ⊕ $false c_0_29->c_0_37

Input Dependencies

c_0_4

Assumptions

c_0_23

Conclusion

c_0_29

Dependents

c_0_33 c_0_37

Formula

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

Source

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