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 "Basic_2/grammar/term_simple.ma".
17 (* CANDIDATES OF REDUCIBILITY ***********************************************)
19 (* abstract conditions for candidates *)
21 definition CR1: predicate term → predicate term → Prop ≝
22 λRD,RC. ∀T. RC T → RD T.
24 definition CR2: relation term → predicate term → Prop ≝
25 λRR,RC. ∀T1,T2. RC T1 → 𝕊[T1] → RR T1 T2 → RC T2.
27 definition CR3: relation term → predicate term → Prop ≝
28 λRR,RC. ∀T1. (∀T2. RR T1 T2 → RC T2) → 𝕊[T1] → RC T1.
31 record cr (RR:relation term) (RD:predicate term): Type[0] ≝ {
32 in_cr: predicate term;
39 "context-free parallel reduction (term)"
40 'InSubset T R = (in_cr ? ? R T).
42 definition in_fun_cr: ∀RR,RD. ∀D,C:(cr RR RD). predicate term ≝
43 λRR,RD,D,C,T. ∀V. V ϵ D → 𝕔{Appl}V.T ϵ C.