(*** Introduction to Computational Logic, Coq part of Assignment 5 ***)
(***
Use Coq to complete the file below.  
If you have any questions, please use the discussion board.
http://www.ps.uni-saarland.de/courses/cl-ss12/forum/
***)

Inductive uni : Type :=
| Typ : nat -> uni
| Prp : uni.

Inductive ter : Type :=
| R : nat -> ter
| L : ter -> ter -> ter
| A : ter -> ter -> ter
| F : ter -> ter -> ter
| U : uni -> ter.

Inductive order : Type :=
| Less : order
| Equal : order
| Greater : order.

Fixpoint order_nat (m n : nat) : order :=
match m,n with
| O, O => Equal
| O, S _ => Less
| S _, O => Greater
| S m, S n => order_nat m n
end.

Definition eq_nat (m n : nat) : bool :=
match order_nat m n with Equal => true | _ => false end.

Fixpoint free (d n : nat) (s : ter) : bool :=
match s with
| R k => eq_nat k (d + n)
| L s1 s2 => orb (free d n s1) (free (S d) n s2)
| A s1 s2 => orb (free d n s1) (free d n s2)
| F s1 s2 => orb (free d n s1) (free (S d) n s2)
| U _ => false
end.

(*** Exercise 5.4 ***)
(*** Define subst (and shift) ***)