- we set up the support for the "bt-reduction" of Automath literature

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / xpr.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma
index 78dd4502ad18898bf25f799258cdb6737f89acbc..7375349efe659651ab8659973413a664c43298a6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma
@@ -17,8 +17,10 @@ include "basic_2/reducibility/cpr.ma".
 
 (* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
 
-definition xpr: ∀h. sd h → lenv → relation term ≝
-   λh,g,L,T1,T2. L ⊢ T1 ➡ T2 ∨ ∃l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2.
+inductive xpr (h) (g) (L) (T1) (T2): Prop ≝
+| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2
+| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2
+.
 
 interpretation
    "extended parallel reduction (term)"
@@ -26,11 +28,5 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma cpr_xpr: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
-/2 width=1/ qed.
-
-lemma ssta_xpr: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2.
-/3 width=2/ qed.
-
-lemma xpr_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸[g] T.
+lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L).
 /2 width=1/ qed.