Library DA

Definition Ex := R (lam (lam (lam (
   #0 #1 (lam I) (lam (#3 (Succ #2) #1)) I)))).

Lemma Ex_rec u n : proc u → Ex (enc n) u == u (enc n) (lam I) (lam ((lam (Ex #0)) (Succ (enc n)) u)) I.

Lemma Ex_correct_1 (u : term) n : proc u → u (enc n) == true → converges (Ex (enc n) u).

Definition n_decider u := proc u ∧ ∀ n, u (enc n) == true ∨ u (enc n) == false.

Lemma Ex_correct_3a (u : term) n : n_decider u → converges ( Ex (enc (S n)) u ) → converges ( Ex (enc n) u ).

Lemma Ex_correct_3 (u : term) n m : n_decider u → n ≥ m → converges ( Ex (enc n) u ) → converges ( Ex (enc m) u ).

Lemma Ex_correct_2 (u : term) n : n_decider u → converges (Ex (enc n) u) → ∃ n, u (enc n) == true.

Definition n_ldec P := ∃ u : term,
  proc u ∧
  (∀ s : nat, P s ∧ u (enc s) == true ∨ ¬ P s ∧ u (enc s) == false).

Lemma DA_nat M :
  n_ldec M → lacc (fun _ ⇒ ∃ n, M n).

Theorem DA M :
  ldec M → lacc (fun _ ⇒ ∃ t, M t).