w6 camil

diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1
new file mode 100644 (file)
index 0000000..0f279ca
--- /dev/null
+++ b/week6/camil/9.4.1
@@ -0,0 +1,11 @@
+9.4.1 - proof by induction over as
+
+Induction base:
+    Suppose as = []. Then we have:
+    map f (as ++ bs) = map f ([] ++ bs) = map f bs = [] ++ (map f bs) = (map f []) ++ (map f bs) = (map f as) ++ (map f bs).
+
+Induction step:
+    Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs. Then we have:
+    map f ([a:as] ++ bs) = map f [a:as ++ bs] = [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)] = [f a : map f as] ++ (map f bs) = (map f [a:as]) ++ (map f bs).
+
+By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs.
\ No newline at end of file

diff --git a/week6/camil/9.4.2 b/week6/camil/9.4.2
new file mode 100644 (file)
index 0000000..c23b58e
--- /dev/null
+++ b/week6/camil/9.4.2
@@ -0,0 +1,11 @@
+9.4.2 - proof by induction over xs
+
+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).
+
+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]).
+
+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