+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/grammar/term_simple.ma".
+
+(* CANDIDATES OF REDUCIBILITY ***********************************************)
+
+(* abstract conditions for candidates *)
+
+definition CR1: predicate term → predicate term → Prop ≝
+ λRD,RC. ∀T. RC T → RD T.
+
+definition CR2: relation term → predicate term → Prop ≝
+ λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2.
+
+definition CR3: relation term → predicate term → Prop ≝
+ λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1.
+
+(* a candidate *)
+record cr (RR:relation term) (RD:predicate term): Type[0] ≝ {
+ in_cr: predicate term;
+ cr1: CR1 RD in_cr;
+ cr2: CR2 RR in_cr;
+ cr3: CR3 RR in_cr
+}.
+
+interpretation
+ "context-free parallel reduction (term)"
+ 'InSubset T R = (in_cr ? ? R T).
+
+definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝
+ λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C.