-9.4.2 - proof by induction over xs

-

-Induction base:

- Suppose xs = []. Then we have:

-

- flatten (map (map f) xs) // assumption xs = []

- = flatten (map (map f) []) // definition of map, rule 3

- = flatten [] // definition of flatten, rule 5

- = [] // definition of map, rule 3

- = map f [] // definition of flatten, rule 5

- = map f (flatten []) // assumption xs = []

- = map f (flatten xs).

-

-Induction step:

- Suppose flatten (map (map f) xs) = map f (flatten xs) for certain xs of finite length (induction hypothesis). Then we have:

-

- flatten (map (map f) [x:xs]) // definition of map, rule 4

- = flatten [map f x : map (map f) xs] // definition of flatten, rule 6

- = (map f x) ++ flatten (map (map f) xs) // induction hypothesis: assumption flatten (map (map f) xs) = map f (flatten xs)

- = (map f x) ++ (map f (flatten xs)) // by 9.4.1

- = map f (x ++ (flatten xs)) // definition of flatten, rule 6

- = map f (flatten [x:xs]).

-

-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. \ No newline at end of file