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.