5 (++) [y:ys] xs = [y : ys ++ xs] (2)
7 map :: (a -> b) [a] -> [b]
9 map f [x:xs] = [f x : map f xs] (4)
11 flatten :: [[a]] -> [a]
13 flatten [x:xs] = x ++ (flatten xs) (6)
17 voor iedere functie f, eindige lijst as en bs:
19 map f (as ++ bs) = (map f as) ++ (map f bs)
22 met inductie naar de lengte van as.
27 map f ([] ++ bs) = (map f []) ++ (map f bs) basis
29 => map f (bs) = (map f []) ++ (map f bs) (1)
31 => map f (bs) = [] ++ (map f bs) (3)
33 => map f bs = map f bs (1)
36 aanname: stelling geldt voor zekere as, ofwel:
37 map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
39 Te bewijzen: stelling geldt ook voor as, ofwel:
40 map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)
42 map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs) basis
44 => map f [a:as ++ bs] = (map f [a:as]) ++ (map f bs) (2)
46 => [f a : map f (as ++ bs)] = (map f [a:as]) ++ (map f bs) (4)
48 => [f a : map f (as ++ bs)] = [f a : map f as] ++ (map f bs) (4)
49 ****************************
50 => [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)] (4)
51 **************** ************************
52 => map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
54 Dus: basis + inductiestap => stelling bewezen.
58 voor iedere functie f, voor iedere eindige lijst xs:
60 flatten (map (map f) xs) = map f (flatten xs)
63 met inductio van de lengte van xs
68 flatten (map (map f) []) = map f (flatten []) basis
70 = flatten [] = map f (flatten []) (3)
72 = flatten [] = map f [] (5)
79 aanname: stelling geldt voor zekere xs, ofwel:
80 flatten (map (map f) xs) = map f (flatten xs)
82 Te bewijzen: stelling geldt ook voor xs, ofwel:
83 flatten (map (map f) [x:xs]) = map f (flatten [x:xs])
85 flatten (map (map f) [x:xs]) = map f (flatten [x:xs]) basis
87 => flatten [map f x: map (map f) xs] = map f (flatten [x:xs]) (4)
88 *********************************
89 => (map f x) ++ (flatten (map (map f) xs)) = map f (flatten [x:xs]) (6)
91 => (map f x) ++ (flatten (map (map f) xs)) = map f (x ++ (flatten xs)) (6)
92 *************************
93 => (map f x) ++ (flatten (map (map f) xs)) = (map f x) ++ (map f (flatten xs)) (9.4.1)
94 ************************ ****************
95 => flatten (map (map f) xs) = map f (flatten xs) (IH)
97 Dus: basis + inductiestap => stelling bewezen.