X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Ffprs.ma;h=61c720754a0103a784e4f7f918ea280d705925c6;hb=5613a25cee29ef32a597cb4b44e8f2f4d71c4df0;hp=bf429672aa6d1eeca0b75e408b69e76ae7545bde;hpb=9c09a0b1f8801e40612eef429b82fc6dbae01b85;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma
index bf429672a..61c720754 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma
@@ -21,6 +21,18 @@ definition fprs: bi_relation lenv term ≝ bi_TC … fpr.
 interpretation "context-free parallel computation (closure)"
    'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2).
 
+(* Basic eliminators ********************************************************)
+
+lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
+                (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) →
+                ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2.
+/3 width=7 by bi_TC_star_ind/ qed-.
+
+lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
+                   (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) →
+                   ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1.
+/3 width=7 by bi_TC_star_ind_dx/ qed-.
+
 (* Basic properties *********************************************************)
 
 lemma fprs_refl: bi_reflexive … fprs.