(* 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)"
(* 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.