week6/camil/9.4.2

   1 9.4.2 - proof by induction over xs
   2
   3 Induction base:
   4     Suppose xs = []. Then we have:
   5
   6     flatten (map (map f) xs)                    // assumption xs = []
   7     = flatten (map (map f) [])                  // definition of map, rule 3
   8     = flatten []                                // definition of flatten, rule 5
   9     = []                                        // definition of map, rule 3
  10     = map f []                                  // definition of flatten, rule 5
  11     = map f (flatten [])                        // assumption xs = []
  12     = map f (flatten xs).
  13
  14 Induction step:
  15     Suppose flatten (map (map f) xs) = map f (flatten xs) for certain xs of finite length (induction hypothesis). Then we have:
  16
  17     flatten (map (map f) [x:xs])                // definition of map, rule 4
  18     = flatten [map f x : map (map f) xs]        // definition of flatten, rule 6
  19     = (map f x) ++ flatten (map (map f) xs)     // induction hypothesis: assumption flatten (map (map f) xs) = map f (flatten xs)
  20     = (map f x) ++ (map f (flatten xs))         // by 9.4.1
  21     = map f (x ++ (flatten xs))                 // definition of flatten, rule 6
  22     = map f (flatten [x:xs]).
  23
  24 By the principle of induction we have now proven that flatten (map (map f) xs) = map f (flatten xs) for any list of finite length xs.