Entry	Value
Package Name	list-zip-thm
Count	15
Theorems	length_zip : !l1 l2 n. LENGTH l1 = n /\ LENGTH l2 = n ==> LENGTH (zip l1 l2) = n length_zipwith : !f l1 l2 n. LENGTH l1 = n /\ LENGTH l2 = n ==> LENGTH (zipwith f l1 l2) = n nth_zip : !l1 l2 n i. LENGTH l1 = n /\ LENGTH l2 = n /\ i < n ==> nth (zip l1 l2) i = nth l1 i,nth l2 i nth_zipwith : !f l1 l2 n i. LENGTH l1 = n /\ LENGTH l2 = n /\ i < n ==> nth (zipwith f l1 l2) i = f (nth l1 i) (nth l2 i) unzip_cons : !h x y t xs ys. unzip (CONS h t) = CONS x xs,CONS y ys <=> h = x,y /\ unzip t = xs,ys unzip_eq_nil1 : !l ys. unzip l = [],ys <=> l = [] /\ ys = [] unzip_eq_nil2 : !l xs. unzip l = xs,[] <=> l = [] /\ xs = [] unzip_nil : unzip [] = [],[] zip_append : !x1 x2 y1 y2. LENGTH x1 = LENGTH y1 /\ LENGTH x2 = LENGTH y2 ==> zip (APPEND x1 x2) (APPEND y1 y2) = APPEND (zip x1 y1) (zip x2 y2) zip_cons : !x y xs ys. LENGTH xs = LENGTH ys ==> zip (CONS x xs) (CONS y ys) = CONS (x,y) (zip xs ys) zip_nil : zip [] [] = [] zip_sing : !x y. zip [x] [y] = [x,y] zip_unzip : !l xs ys. unzip l = xs,ys <=> LENGTH xs = LENGTH ys /\ l = zip xs ys zipwith_append : !f x1 x2 y1 y2. LENGTH x1 = LENGTH y1 /\ LENGTH x2 = LENGTH y2 ==> zipwith f (APPEND x1 x2) (APPEND y1 y2) = APPEND (zipwith f x1 y1) (zipwith f x2 y2) zipwith_sing : !f x y. zipwith f [x] [y] = [f x y]

Back to main package page