**Exercise:** Prove that for any list xs and element x, behead (prepend xs x) ~ xs, where prepend and behead are defined as follows:  let prepend xs x = x::xs let behead = function | [] -> [] | _::t -> t  *Hint: induction is not needed.* **Exercise:** Prove that for any list xs, noop xs ~ xs, where noop is defined as follows:  let rec noop = function | [] -> [] | h::t -> h :: noop t  Use the following template for an inductive proof:  Theorem: TODO(xs) Proof: by induction on xs Case: xs = [] Show: TODO TODO Case: xs=h::t Show: TODO IH : TODO TODO QED  * * * *In the rest of the exercises, continue to use that template for proofs, and to use structural induction. Make sure for each case to state what you are trying to show for that case and what the inductive hypotheses are.* * * * **Exercise:** Prove that for all f, xs, and ys, map f (xs @ ys) = (map f xs) @ (map f ys), where map and (@) are defined as follows:  let rec append l1 l2 = match l1 with | [] -> l2 | h::t -> h :: (append t l2) let (@) = append let rec map f = function | [] -> [] | h::t -> (f h) :: map f t  **Exercise:** Prove that for all trees t, size (reflect t) ~ size t, given the following definitions:  type 'a tree = Leaf | Branch of 'a * 'a tree * 'a tree let rec reflect = function | Leaf -> Leaf | Branch(x,l,r) -> Branch(x, reflect r, reflect l) let rec size = function | Leaf -> 0 | Branch(x,l,r) -> 1 + size l + size r  **Exercise:** Prove that for all functions f, g, and h (of appropriate types), (f @@ g) @@ h ~ f @@ (g @@ h), where (@@) is defined as follows:  let (@@) f g x = f (g x)  ** *Exercise:** Prove that for all lists xs, and for all lists ys, rev_append xs ys ~ (nrev xs) @ ys, where rev_append and nrev are defined as follows:  let rec rev_append l1 l2 = match l1 with | [] -> l2 | h :: t -> rev_append t (h :: l2) let rec nrev = function | [] -> [] | h::t -> (nrev t) @ [h]  *Hint: you will need to use and prove the following lemma.*  Lemma: for all lists l1, l2, l3, l1 @ (l2 @ l3) ~ (l1 @ l2) @ l3  Next, prove that for all lists xs, rev xs ~ nrev xs, where rev is defined as follows:  let rev xs = rev_append xs []  *Hint: state and prove a lemma.* Note that this definition of rev is, in fact, how OCaml's List.rev is defined. You have therefore proved the correctness of a tail-recursive implementation of list reversal by showing its equivalence to a non-tail-recursive implementation.