(**************************************************************************)
(*       ___                                                              *)
(*      ||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/genv.ma".
include "basic_2/multiple/fpas.ma".

(* GENERIC COMPUTATION PROPERTIES *******************************************)

definition candidate: Type[0] ≝ relation3 genv lenv term.

definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
                 ∀G,L1,L2,T1,T2,s. ⦃L1, T1⦄ ⇳[s] ⦃L2, T2⦄ →
                 NF … (RR G L1) RS T1 → NF … (RR G L2) RS T2.

definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term.
                  ∀G,L1,L2,T1,T2,s. ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ →
                  NF … (RR G L1) RS T1 → NF … (RR G L2) RS T2.

definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
                 ∀G,L. ∃k. NF … (RR G L) RS (⋆k).

definition CP2 ≝ λRP:candidate.
                 ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.

(* requirements for generic computation properties *)
record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
{ cp0: CP0 RR RS;
  cp1: CP1 RR RS;
  cp2: CP2 RP
}.

(* Basic properties *********************************************************)

(* Basic_1: was just: nf2_lift1 *)
lemma gcp_fpas: ∀RR,RS. CP0 RR RS → CP0s RR RS.
#RR #RS #HRR #G #L1 #L2 #T1 #T2 #s #H @(fpas_ind … H) -L2 -T2 /3 width=5 by/
qed.