Added comments

diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1
index 0f279ca..d9b2608 100644 (file)
--- a/week6/camil/9.4.1
+++ b/week6/camil/9.4.1
@@ -2,10 +2,22 @@
 
 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).
+
+    map f (as ++ bs)                        // assumption as = []
+    = map f ([] ++ bs)                      // definition of ++, rule 1
+    = map f bs                              // definition of ++, rule 1
+    = [] ++ (map f bs)                      // definition of map, rule 3
+    = (map f []) ++ (map f bs)              // assumption as = []
+    = (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).
+    Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have:
+    
+    map f ([a:as] ++ bs)                    // definition of ++, rule 2
+    = map f [a:as ++ bs]                    // definition of map, rule 4
+    = [f a : map f (as ++ bs)]              // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs)
+    = [f a : (map f as) ++ (map f bs)]      // rewriting list
+    = [f a : map f as] ++ (map f bs)        // definition of map, rule 4
+    = (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
index c23b58e..bc95352 100644 (file)
--- a/week6/camil/9.4.2
+++ b/week6/camil/9.4.2
@@ -2,10 +2,23 @@
 
 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