These notes re-present the proofs from lecture. ## Proof 1  let easy x y z = x * (y + z) Theorem: easy 1 20 30 ~ 50 Proof: easy 1 20 30 ~ 50 (by eval) QED  ## Proof 2  let easy x y z = x * (y + z) Theorem: easy a b c ~ easy a c b Proof: easy a b c ~ a * (b + c) (by eval) ~ a * (c + b) (by math) ~ easy a c b (by eval, symm.) QED  ## Proof 3  let rec even n = match n with | 0 -> true | 1 -> false | n -> even (n-2) Theorem: for all natural numbers n, even (2*n) ~ true. Proof: by induction on n Case: n = 0 Show: even (2*0) ~ true even (2*0) ~ even 0 (math,congr.) ~ true (eval) Case: n = k+1, where k >= 0 IH: even (2*k) ~ true Show: even (2*(k+1)) ~ true even (2*(k+1)) ~ even (2*k+2) (math,congr.) ~ even (2*k+2-2) (eval,k>=0) ~ even (2*k) (math,congr.) ~ true (IH) QED