Sum of list


Definition

 sum_list.Nil: sum_list [] = 0
sum_list.Cons: sum_list (?x # ?xs) = ?x + sum_list ?xs
THEOREM    sum_list (xs @ ys) = sum_list xs + sum_list ys
sum_list.append:
	sum_list (?xs @ ?ys) = sum_list ?xs + sum_list ?ys

Proof unavailable