@leo's

The master solution of the official excercise are online since quite some time on https://www1.ethz.ch/infsec/education/ss11/fmfp/fp_material_secured. Now I also put the solution for the first weeks extra exercises online.

The calculation in GHCi could look like:

Prelude> let x=31
Prelude> let y=11
Prelude> x+y
42
Prelude> x-y
20
Prelude> x*y
341
Prelude> div x y
2
Prelude> mod x y
9
Prelude> x^y
25408476896404831
Prelude> sqrt (fromIntegral x)
5.5677643628300215
Prelude> (fromIntegral x) ** 1/3
10.333333333333334

There are different methods to implement the n-th Factorial. Let me show you some examples. First with if, which is often considered as bad style.

fac n = if n==0 then 1 else n*(fac (n-1))

It's possible to implement it with pattern matching.

fac' 0 = 1
fac' n = n * (fac' (n-1)) 

Or with guards.

fac'' n = 
	| n==0 = 1
	| otherwise = n * (fac'' (n-1))

If this is all to easy for you. You might implement a endless list of factorials (this is beyond the course scope).

fac''' = 1:zipWith (*) fac''' [2..]

The proof for "kn(<k1,k2>), kn({s}k1) |- kn(s)" in ASCII-Art:

G := kn(<k1,k2>), kn({s}k1)

                    ------------------Ax
                     G |- kn(<k1,k2>)
----------------Ax  ------------------ Pair-EL
 G |- kn({s}k1)        G |- kn(k1)
------------------------------------ Enc-E
 G |- kn(s)