Proof Step: c_0_13

name: c_0_13 syntax: thf role: plain inference: variable_rename

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

Input Dependencies

c_0_4

Assumptions

c_0_4

Conclusion

c_0_13

Dependents

c_0_18

Formula

! [X3430: dB > dB > dB,X3431: dB,X3432: dB,X3433: list_dB] :
  ( ( foldl_dB_dB @ X3430 @ X3431 @ ( cons_dB @ X3432 @ X3433 ) )
  = ( foldl_dB_dB @ X3430 @ ( X3430 @ X3431 @ X3432 ) @ X3433 ) )

Source

inference(variable_rename,[status(thm)],[c_0_4])