// Mart Lubbers, s4109503
// Camil Staps, s4498062

Zij gegeven:

(++) :: [a] [a] -> [a]
(++) []     xs = xs                (1)
(++) [y:ys] xs = [y : ys ++ xs]    (2)

map :: (a -> b) [a] -> [b]
map f []       = []                (3)
map f [x:xs]   = [f x : map f xs]  (4)

flatten :: [[a]] -> [a]
flatten []     = []                (5)
flatten [x:xs] = x ++ (flatten xs) (6)

1. 
Te bewijzen: 
	voor iedere functie f, eindige lijst as en bs:
		
		map f (as ++ bs) = (map f as) ++ (map f bs)

Bewijs:
Met inductie over as.

Inductiebasis: 
Stel as = []. Dan hebben we:

    map f (as ++ bs)                        // aanname as = []
    = map f ([] ++ bs)                      // definitie van ++, regel 1
    = map f bs                              // definitie van ++, regel 1
    = [] ++ (map f bs)                      // definitie van map, regel 3
    = (map f []) ++ (map f bs)              // aanname as = []
    = (map f as) ++ (map f bs).

Inductiestap:
Stel map f (as ++ bs) = (map f as) ++ (map f bs) voor zekere as en elke bs (inductiehypothese). Dan hebben we:

    map f ([a:as] ++ bs)                    // definitie van ++, regel 2
    = map f [a:as ++ bs]                    // definitie van map, regel 4
    = [f a : map f (as ++ bs)]              // inductiehypothese: map f (as ++ bs) = (map f as) ++ (map f bs)
    = [f a : (map f as) ++ (map f bs)]      // lijst herschrijven
    = [f a : map f as] ++ (map f bs)        // definitie van map, regel 4
    = (map f [a:as]) ++ (map f bs).

Uit het principe van volledige inductie volgt nu dat voor iedere functie f, eindige lijst as en bs:

    map f (as ++ bs) = (map f as) ++ (map f bs)     (9.4.1)

2. 
Te bewijzen:
	voor iedere functie f, voor iedere eindige lijst xs:
	
		flatten (map (map f) xs) = map f (flatten xs)

Bewijs:
Met inductie over xs.

Inductiebasis:
Stel xs = []. Dan hebben we:

    flatten (map (map f) xs)                    // aanname xs = []
    = flatten (map (map f) [])                  // definitie van map, regel 3
    = flatten []                                // definitie van flatten, regel 5
    = []                                        // definitie van map, regel 3
    = map f []                                  // definitie van flatten, regel 5
    = map f (flatten [])                        // aanname xs = []
    = map f (flatten xs).

Inductiestap:
Stel flatten (map (map f) xs) = map f (flatten xs) voor een zekere eindige lijst xs (inductiehypothese). Dan hebben we:

    flatten (map (map f) [x:xs])                // definitie van map, regel 4
    = flatten [map f x : map (map f) xs]        // definitie van flatten, regel 6
    = (map f x) ++ flatten (map (map f) xs)     // inductiehypothese: flatten (map (map f) xs) = map f (flatten xs)
    = (map f x) ++ (map f (flatten xs))         // 9.4.1
    = map f (x ++ (flatten xs))                 // definitie van flatten, regel 6
    = map f (flatten [x:xs]).

Uit het principe van volledige inductie volgt nu dat voor iedere functie f en eindige lijst xs geldt:

    flatten (map (map f) xs) = map f (flatten xs)