(FUN nil : natlist cons : nat -> natlist -> natlist plus : nat -> nat -> nat foldr : (nat -> nat -> nat) -> nat -> natlist -> nat sum : natlist -> nat 0 : nat ) (VAR x : nat y : nat n : nat F : nat -> nat -> nat h : nat t : natlist l : natlist ) (RULES foldr (\x y. F x y) n nil -> n, foldr (\x y. F x y) n (cons h t) -> F h (foldr (\x y. F x y) n t), sum l -> foldr (\x y. plus y x) 0 l, sum nil -> 0, sum (cons h t) -> plus (sum t) h, )