Induction base:
Suppose xs = []. Then we have:
- flatten (map (map f) xs) = flatten (map (map f) []) = flatten [] = [] = map f [] = map f (flatten []) = map f (flatten xs).
+
+ 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. Then we have:
- flatten (map (map f) [x:xs]) = flatten [map f x : map (map f) xs] = (map f x) ++ flatten (map (map f) xs) = (map f x) ++ (map f (flatten xs)) =(9.4.1) map f (x ++ (flatten xs)) = map f (flatten [x:xs]).
+ 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