1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "lambda/terms/term.ma".
17 (* SUPERCOMBINATOR **********************************************************)
19 inductive is_supercombinator: nat → nat → predicate term ≝
20 | is_supercombinator_vref:
21 ∀i,d. i < d → ∀h. is_supercombinator h d (#i)
22 | is_supercombinator_abst:
23 ∀A,h. is_supercombinator (S h) (S h) A → ∀d. is_supercombinator h d (𝛌.A)
24 | is_supercombinator_appl:
25 ∀B,A,d. is_supercombinator 0 d B → is_supercombinator 0 d A →
26 ∀h. is_supercombinator h d (@B.A)