Library Proc

Fixpoint dcl (k : nat) (t : term) : bool :=
match t with
| #n ⇒ if decision ( n < k) then Datatypes.true else Datatypes.false
| app s t ⇒ andb (dcl k s) (dcl k t)
| lam s ⇒ dcl (S k) s
end.

Lemma dcl_dclosed k s : Datatypes.true = dcl k s → dclosed k s.

Lemma dclosed_dcl k s : dclosed k s → Datatypes.true = dcl k s.

Lemma leb_lt n m : leb (S n) m = Datatypes.true ↔ n < m.

Definition Leb := R (lam (lam (
   #0 (lam true) (lam (lam (#0 false (lam (#4 #2 #0)))))))).

Lemma Leb_rec_0 m : Leb (enc 0) (enc m) == true.

Lemma Leb_rec_Sm_0 m : Leb (enc (S m)) (enc 0) == false.

Lemma Leb_rec_Sm_Sn m n : Leb (enc (S m)) (enc (S n)) == Leb (enc m) (enc n).

Definition benc (b : bool) := if b then true else false.

Lemma Leb_correct m n : Leb (enc m) (enc n) == benc (leb m n).

Definition Lt := lam (lam (Leb (Succ #1) (#0))).

Lemma Lt_correct n k : Lt (enc n) (enc k) == true ∧ n < k ∨
                       Lt (enc n) (enc k) == false ∧ ¬ n < k.

Definition Dclosed := R (lam (lam (lam (
  #0 (lam ((Lt #0 #2) true false))
     (lam (lam (Andalso (#4 #3 #1) (#4 #3 #0))))
     (lam (#3 (Succ #2) #0))
)))).

Lemma Dclosed_rec_var n k : Dclosed (enc k) (tenc #n) == Lt (enc n) (enc k) true false.

Lemma Dclosed_rec_app k s t : Dclosed (enc k) (tenc (app s t)) ==
  Andalso (Dclosed (enc k) (tenc s)) (Dclosed (enc k) (tenc t)).

Lemma Dclosed_rec_lam k s : Dclosed (enc k) (tenc (lam s)) ==
                                  Dclosed (enc (S k)) (tenc s).

Lemma Andalso_correct s t : Andalso (benc s) (benc t) == benc (s && t).

Lemma Dclosed_correct k s : Dclosed (enc k) (tenc s) == benc (dcl k s).

Definition Closed := Dclosed (enc 0).

Lemma Closed_correct s : Closed (tenc s) == true ∧ closed s ∨
                         Closed (tenc s) == false ∧ ¬ closed s.

Lemma ldec_closed : ldec closed.

Definition Lambda := lam (#0 (lam false) (lam (lam false)) (lam true)).


Lemma Lambda_correct s : Lambda (tenc s) == true ∧ lambda s ∨
                         Lambda (tenc s) == false ∧ ¬ lambda s.

Lemma ldec_lambda : ldec lambda.

Lemma ldec_proc : ldec proc.