Exercise 1:  COS 441

1. Here is an inductive definition for lists:

Judgement Form:   |- l list

------------ (nil)
|- nil list

|- n nat     |- l list
------------------------ (cons)
|- cons (n, l) list

(a) Prove that cons (S Z, cons (Z, nil)) is a list.

(b) Define another judgement |- l ENlist that is valid when l has
an even number of elements.

(c) Define another judgement |- l ENlist that is valid when all
natural numbers in l are a multiple of 3.  (Allow yourself to define 
an auxiliary judgement if you need to.)

(d) Define the judgement |- append l1 l2 l3 so that l3 is equal to l2
appended to the end of l1 (for any l1 and l2).

(e) Define the judgement |- t tree so that t is a binary tree of 
natural numbers.  Each internal node should carry a natural number.
Leaf nodes of the tree should not carry natural numbers.

(f) Define the judgement |- size t n such that n is the number of
internal nodes (as opposed to leaf nodes in t.