Entry	Value
Package Name	list-fold-thm
Count	14
Theorems	foldl_append : !f b l1 l2. foldl f b (APPEND l1 l2) = foldl f (foldl f b l1) l2 foldl_append_assoc : !g f b l1 l2. (!s. g s b = s) /\ (!s1 s2 x. g s1 (f s2 x) = f (g s1 s2) x) ==> foldl f b (APPEND l1 l2) = g (foldl f b l1) (foldl f b l2) foldl_cons : !f b h t. foldl f b (CONS h t) = foldl f (f b h) t foldl_nil : !f b. foldl f b [] = b foldl_reverse : !f b l. foldl f b (REVERSE l) = foldr (C f) b l foldl_suc : !l k. foldl (\n x. SUC n) k l = LENGTH l + k foldl_with_cons : !l1 l2. foldl (C CONS) l2 l1 = APPEND (REVERSE l1) l2 foldl_with_cons_nil : !l. foldl (C CONS) [] l = REVERSE l foldr_append : !f b l1 l2. foldr f b (APPEND l1 l2) = foldr f (foldr f b l2) l1 foldr_append_assoc : !g f b l1 l2. (!s. g b s = s) /\ (!x s1 s2. g (f x s1) s2 = f x (g s1 s2)) ==> foldr f b (APPEND l1 l2) = g (foldr f b l1) (foldr f b l2) foldr_reverse : !f b l. foldr f b (REVERSE l) = foldl (C f) b l foldr_suc : !l k. foldr (\x n. SUC n) k l = LENGTH l + k foldr_with_cons : !l1 l2. foldr CONS l2 l1 = APPEND l1 l2 foldr_with_cons_nil : !l. foldr CONS [] l = l

Back to main package page