From f6464ba2cffc9936b4d8285604786cd91531e0d0 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 3 Sep 2012 14:30:24 +0000
Subject: [PATCH] lambda_delta: partial commit ...

---
 .../lambda_delta/basic_2/etc/top/lenv_top.ma  | 68 ++++++++++++++
 .../lambda_delta/basic_2/grammar/cl_shift.ma  | 24 ++++-
 .../basic_2/grammar/lenv_append.ma            | 77 +++++++++++----
 .../basic_2/grammar/lenv_length.ma            | 28 ++++++
 .../lambda_delta/basic_2/grammar/lenv_px.ma   | 11 ++-
 .../basic_2/grammar/lenv_px_bi.ma             | 88 ++++++++++++++++++
 .../contribs/lambda_delta/basic_2/notation.ma |  4 +
 .../lambda_delta/basic_2/reducibility/fpr.ma  | 57 ++++++++++++
 .../basic_2/reducibility/lfpr_alt.ma          | 93 +++++++++++++++++++
 .../lambda_delta/basic_2/reducibility/tpr.ma  | 30 ++++++
 .../lambda_delta/basic_2/substitution/tps.ma  | 12 +++
 .../contribs/lambda_delta/ground_2/arith.ma   |  7 ++
 matita/matita/lib/basics/relations.ma         |  7 ++
 matita/matita/predefined_virtuals.ml          | 18 ++--
 14 files changed, 493 insertions(+), 31 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma b/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma
new file mode 100644
index 000000000..ab90cebe7
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/etc/top/lenv_top.ma
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+notation "hvbox( T1 𝟙 break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'RTop $T1 $T2 }.
+
+include "basic_2/grammar/lenv_px.ma".
+
+(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
+
+definition ttop: relation term ≝ λT1,T2. True.
+
+definition ltop: relation lenv ≝ lpx ttop.
+
+interpretation
+  "top reduction (environment)"
+  'RTop L1 L2 = (ltop L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltop_refl: reflexive … ltop.
+/2 width=1/ qed.
+
+lemma ltop_sym: symmetric … ltop.
+/2 width=1/ qed.
+
+lemma ltop_trans: transitive … ltop.
+/2 width=3/ qed.
+
+lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆.
+/2 width=2 by lpx_inv_atom1/ qed-.
+
+lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 →
+                      ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2.
+#K1 #I #V1 #L2 #H
+elim (lpx_inv_pair1 … H) -H /2 width=4/
+qed-.
+
+lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆.
+/2 width=2 by lpx_inv_atom2/ qed-.
+
+lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 →
+                      ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1.
+#L1 #K2 #I #V2 #H
+elim (lpx_inv_pair2 … H) -H /2 width=4/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|.
+/2 width=2 by lpx_fwd_length/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
index 319569fe5..837b1c670 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv.ma".
+include "basic_2/grammar/lenv_append.ma".
 
 (* SHIFT OF A CLOSURE *******************************************************)
 
@@ -22,3 +22,25 @@ let rec shift L T on L ≝ match L with
 ].
 
 interpretation "shift (closure)" 'Append L T = (shift L T).
+
+(* Basic properties *********************************************************)
+
+lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T.
+#L #K elim K -K normalize //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma shift_inj: ∀L1,L2. ∀T1,T2:term. L1 @@ T1 = L2 @@ T2 → |L1| = |L2| →
+                 L1 = L2 ∧ T1 = T2.
+#L1 elim L1 -L1
+[ * normalize /2 width=1/
+  #L2 #I2 #V2 #T1 #T2 #_ <plus_n_Sm #H destruct
+| #L1 #H1 #V1 #IH * normalize
+  [ #T1 #T2 #_ <plus_n_Sm #H destruct
+  | #L2 #I2 #V2 #T1 #T2 #H1 #H2
+    elim (IH … H1 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+  ]
+]
+qed-.
+  
\ No newline at end of file
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
index a97908233..83b65a335 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_append.ma
@@ -35,27 +35,64 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-axiom discr_lpair_append_xy_x: ∀I,L,K,V. (L @@ K).ⓑ{I}V = L → ⊥.
-(*
-#I #L #K #V #H
-lapply (refl … (|L|)) <H in ⊢ (? ? % ? → ?); -H
-normalize >append_length -I -V #H
-*)
-lemma append_inv_sn: ∀L1,L2,L. L1 @@ L = L2 @@ L → L1 = L2.
-#L1 #L2 #L elim L -L normalize //
-#L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
-qed.
+lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
+                     L1 = L2 ∧ K1 = K2.
+#K1 elim K1 -K1
+[ * normalize /2 width=1/
+  #K2 #I2 #V2 #L1 #L2 #_ <plus_n_Sm #H destruct
+| #K1 #I1 #V1 #IH * normalize
+  [ #L1 #L2 #_ <plus_n_Sm #H destruct
+  | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
+    elim (IH … e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+  ]
+]
+qed-.
 
 (* Note: lemma 750 *)
-lemma append_inv_dx: ∀L1,L2,L. L @@ L1 = L @@ L2 → L1 = L2.
-#L1 elim L1 -L1
-[ * normalize //
-  #L2 #I2 #V2 #L #H
-  elim (discr_lpair_append_xy_x I2 L L2 V2 ?) //
-| #L1 #I1 #V1 #IHL1 * normalize
-  [ #L #H -IHL1 elim (discr_lpair_append_xy_x … H)
-  | #L2 #I2 #V2 #L normalize #H destruct (**) (* destruct does not simplify well *)
-    -H >e0 /3 width=2/
+lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
+                     L1 = L2 ∧ K1 = K2.
+#K1 elim K1 -K1
+[ * normalize /2 width=1/
+  #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct
+  normalize in H2; >append_length in H2; #H
+  elim (plus_xySz_x_false … H)
+| #K1 #I1 #V1 #IH * normalize
+  [ #L1 #L2 #H1 #H2 destruct
+    normalize in H2; >append_length in H2; #H
+    elim (plus_xySz_x_false … (sym_eq … H))
+  | #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
+    elim (IH … e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
   ]
 ]
-qed.
+qed-.
+
+lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
+                                ∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
+#d @(nat_ind_plus … d) -d
+[ #L #H 
+  elim (length_inv_pos_dx … H) -H #I #K #V #H
+  >(length_inv_zero_dx … H) -H #H destruct
+  @ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (* /3/ does not work *)
+| #d #IHd #L #H
+  elim (length_inv_pos_dx … H) -H #I #K #V #H
+  elim (IHd … H) -IHd -H #I0 #K0 #V0 #H1 #H2 #H3 destruct
+  @(ex2_3_intro … (K0.ⓑ{I}V)) //
+]
+qed-.
+
+(* Basic_eliminators ********************************************************)
+
+fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ →
+                      (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
+                      ∀d,L. |L| = d → R L.
+#R #Hatom #Hpair #d @(nat_ind_plus … d) -d
+[ #L #H >(length_inv_zero_dx … H) -H //
+| #d #IH #L #H
+  elim (length_inv_pos_dx_append … H) -H #I #K #V #H1 #H2 destruct /3 width=1/
+]
+qed-.
+
+lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ →
+                   (∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
+                   ∀L. R L.
+/3 width=2 by lenv_ind_dx_aux/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma
index 780edc161..faf6de02d 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma
@@ -22,3 +22,31 @@ let rec length L ≝ match L with
 ].
 
 interpretation "length (local environment)" 'card L = (length L).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
+* // #L #I #V normalize <plus_n_Sm #H destruct
+qed-.
+
+lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
+* // #L #I #V normalize <plus_n_Sm #H destruct
+qed-.
+
+lemma length_inv_pos_dx: ∀d,L. |L| = d + 1 →
+                         ∃∃I,K,V. |K| = d & L = K. ⓑ{I}V.
+#d *
+[ normalize <plus_n_Sm #H destruct
+| #K #I #V #H
+  lapply (injective_plus_l … H) -H /2 width=5/
+]
+qed-.
+
+lemma length_inv_pos_sn: ∀d,L. d + 1 = |L| →
+                         ∃∃I,K,V. d = |K| & L = K. ⓑ{I}V.
+#d *
+[ normalize <plus_n_Sm #H destruct
+| #K #I #V #H
+  lapply (injective_plus_l … H) -H /2 width=5/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
index 1b0c88e02..9de1599e4 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/lenv_append.ma".
 
 (* POINTWISE EXTENSION OF A CONTEXT-FREE REALTION FOR TERMS *****************)
 
@@ -80,6 +80,10 @@ lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
 #R #HR #L elim L -L // /2 width=1/
 qed.
 
+lemma lpx_sym: ∀R. symmetric ? R → symmetric … (lpx R).
+#R #HR #L1 #L2 #H elim H -H // /3 width=1/
+qed.
+
 lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R).
 #R #HR #L1 #L #H elim H -L //
 #I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H
@@ -129,3 +133,8 @@ lemma lpx_inv_TC: ∀R. reflexive ? R →
                   ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2.
 #R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/
 qed.
+
+lemma lpx_append: ∀R,K1,K2. lpx R K1 K2 → ∀L1,L2. lpx R L1 L2 →
+                  lpx R (L1 @@ K1) (L2 @@ K2).
+#R #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma
new file mode 100644
index 000000000..931d075ab
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px_bi.ma
@@ -0,0 +1,88 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lenv_length.ma".
+
+(* POINTWISE EXTENSION OF A FOCALIZED REALTION FOR TERMS ********************)
+
+inductive lpx_bi (R:bi_relation lenv term): relation lenv ≝
+| lpx_bi_stom: lpx_bi R (⋆) (⋆)
+| lpx_bi_pair: ∀I,K1,K2,V1,V2.
+               lpx_bi R K1 K2 → R K1 V1 K2 V2 →
+               lpx_bi R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
+.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_bi_inv_atom1_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L1 = ⋆ → L2 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom1: ∀R,L2. lpx_bi R (⋆) L2 → L2 = ⋆.
+/2 width=4 by lpx_bi_inv_atom1_aux/ qed-.
+
+fact lpx_bi_inv_pair1_aux: ∀R,L1,L2. lpx_bi R L1 L2 →
+                           ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+                           ∃∃K2,V2. lpx_bi R K1 K2 &
+                                    R K1 V1 K2 V2 & L2 = K2. ⓑ{I} V2.
+#R #L1 #L2 * -L1 -L2
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_bi_inv_pair1: ∀R,I,K1,V1,L2. lpx_bi R (K1. ⓑ{I} V1) L2 →
+                        ∃∃K2,V2. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+                                 L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_bi_inv_pair1_aux/ qed-.
+
+fact lpx_bi_inv_atom2_aux: ∀R,L1,L2. lpx_bi R L1 L2 → L2 = ⋆ → L1 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_bi_inv_atom2: ∀R,L1. lpx_bi R L1 (⋆) → L1 = ⋆.
+/2 width=4 by lpx_bi_inv_atom2_aux/ qed-.
+
+fact lpx_bi_inv_pair2_aux: ∀R,L1,L2. lpx_bi R L1 L2 →
+                           ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+                           ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+                                    L1 = K1. ⓑ{I} V1.
+#R #L1 #L2 * -L1 -L2
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_bi_inv_pair2: ∀R,I,L1,K2,V2. lpx_bi R L1 (K2. ⓑ{I} V2) →
+                        ∃∃K1,V1. lpx_bi R K1 K2 & R K1 V1 K2 V2 &
+                                 L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_bi_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_bi_fwd_length: ∀R,L1,L2. lpx_bi R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_bi_refl: ∀R. bi_reflexive ? ? R → reflexive … (lpx_bi R).
+#R #HR #L elim L -L // /2 width=1/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index a115260b9..1b64f3c90 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -312,6 +312,10 @@ notation "hvbox( ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
    non associative with precedence 45
    for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
 
+notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedAlt $L1 $L2 }.
+
 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'XPRed $h $g $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma
new file mode 100644
index 000000000..46c201147
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reducibility/tpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************)
+
+definition fpr: bi_relation lenv term ≝
+                λL1,T1,L2,T2. |L1| = |L2| ∧ L1 @@ T1 ➡ L2 @@ T2.
+
+interpretation
+   "focalized parallel reduction (closure)"
+   'FocalizedPRed L1 T1 L2 T2 = (fpr L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fpr_refl: bi_reflexive … fpr.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fpr_inv_atom1: ∀L2,T1,T2. ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → T1 ➡ T2 ∧ L2 = ⋆.
+#L2 #T1 #T2 * #H
+lapply (length_inv_zero_sn … H) -H #H destruct /2 width=1/
+qed-.
+
+lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
+                     ∃∃K2,V2. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄  &
+                              L2 = K2.ⓑ{I}V2.
+#I1 #K1 #L2 #V1 #T1 #T2 * #H
+elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct #H
+elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/
+qed-.
+
+lemma fpr_inv_atom3: ∀L1,T1,T2. ⦃L1,T1⦄ ➡ ⦃⋆,T2⦄ → T1 ➡ T2 ∧ L1 = ⋆.
+#L1 #T1 #T2 * #H
+lapply (length_inv_zero_dx … H) -H #H destruct /2 width=1/
+qed-.
+
+lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ →
+                     ∃∃K1,V1. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄  &
+                              L1 = K1.ⓑ{I}V1.
+#I2 #L1 #K2 #V2 #T1 #T2 * #H
+elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct #H
+elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma
new file mode 100644
index 000000000..46f98452e
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr_alt.ma
@@ -0,0 +1,93 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lenv_px_bi.ma".
+include "basic_2/reducibility/fpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************)
+
+(* alternative definition *)
+definition lfpra: relation lenv ≝ lpx_bi fpr.
+
+interpretation
+  "focalized parallel reduction (environment) alternative"
+  'FocalizedPRedAlt L1 L2 = (lfpra L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lfpra_refl: reflexive … lfpra.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfpra_inv_atom1: ∀L2. ⦃⋆⦄ ➡➡ ⦃L2⦄ → L2 = ⋆.
+/2 width=2 by lpx_bi_inv_atom1/ qed-.
+
+lemma lfpra_inv_pair1: ∀K1,I,V1,L2. ⦃K1. ⓑ{I} V1⦄ ➡➡ ⦃L2⦄ →
+                       ∃∃K2,V2. ⦃K1⦄ ➡➡ ⦃K2⦄ & ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ &
+                                L2 = K2. ⓑ{I} V2.
+/2 width=1 by lpx_bi_inv_pair1/ qed-.
+
+lemma lfpra_inv_atom2: ∀L1. ⦃L1⦄ ➡➡ ⦃⋆⦄ → L1 = ⋆.
+/2 width=2 by lpx_bi_inv_atom2/ qed-.
+
+lemma lfpra_inv_pair2: ∀L1,K2,I,V2. ⦃L1⦄ ➡➡ ⦃K2. ⓑ{I} V2⦄ →
+                       ∃∃K1,V1. ⦃K1⦄ ➡➡ ⦃K2⦄ & ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ &
+                                L1 = K1. ⓑ{I} V1.
+/2 width=1 by lpx_bi_inv_pair2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lfpra_fwd_length: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → |L1| = |L2|.
+/2 width=2 by lpx_bi_fwd_length/ qed-.
+
+(****************************************************************************)
+
+lemma fpr_lfpra: ∀L1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
+#L1 #T1 @(cw_wf_ind … L1 T1) -L1 -T1 *
+[ #T1 #_ #L2 #T2 #H
+  elim (fpr_inv_atom1 … H) -H #_ #H destruct //
+| #L1 #I #V1 #T1 #IH #Y #X #H
+  elim (fpr_inv_pair1 … H) -H #L2 #V2 #HL12 #H destruct
+  @lpx_bi_pair 
+  [ @(IH … HL12) 
+  | @IH 
+  
+  /3 width=4/
+
+lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
+#L1 elim L1 -L1
+[ #L2 #T1 #T2 #H
+  elim (fpr_inv_atom1 … H) -H #_ #H destruct //
+| #L1 #I #V1 #IH #L2 #T1 #T2 #H
+  elim (fpr_inv_pair1 … H) -H #L #V #HL1 #H destruct
+  @lpx_bi_pair /2 width=3/ 
+  
+  /4 width=3/
+
+(*
+include "basic_2/reducibility/lcpr.ma".
+
+lemma lcpr_pair2: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ →
+                  ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
+#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
+#H1 #H2 #I
+@(ex2_1_intro … (L.ⓑ{I}V1)) /2 width=1/
+@tpss_
+
+(*
+<(ltpss_fwd_length … HL2) /4 width=5/
+qed.
+*)
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
index d204eba79..a74757b2a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
@@ -203,6 +203,36 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
                       | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
 /2 width=3/ qed-.
 
+(* Basic forward lemmas *****************************************************)
+
+lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
+                      ∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #T1 #T #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #T1 #T >shift_append_assoc #H
+  elim (tpr_inv_bind1 … H) -H *
+  [ #V0 #T0 #X0 #_ #HT10 #HTX0 #H destruct
+    elim (IH … HT10) -IH -T1 #L2 #V2 #HL12 #H destruct
+    elim (tps_fwd_shift1 … HTX0) -V2 #L3 #X3 #HL23 #H destruct
+    lapply (ltop_trans … HL12 HL23) -L2 #HL13
+    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L3)) /2 width=4/ /3 width=1/
+  | #T0 #_ #_ #H destruct
+  ]
+]
+qed-.
+
+lemma tpr_fwd_shift_bind_minus: ∀L1,L2. |L1| = |L2| → ∀I1,I2,V1,V2,T1,T2.
+                                L1 @@ -ⓑ{I1}V1.T1 ➡ L2 @@ -ⓑ{I2}V2.T2 →
+                                L1 𝟙 L2 ∧ I1 = I2.
+#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
+elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX
+elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct
+elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX
+[ #H1 #_ destruct /2 width=1/
+| lapply (ltop_fwd_length … HL1) -HL1 normalize // 
+]
+qed-.
+
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0
    Basic_1: removed local theorems: 1: pr0_delta_tau
diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
index db116f77e..7e35dca7c 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/grammar/lenv_top.ma".
 include "basic_2/substitution/ldrop.ma".
 
 (* PARALLEL SUBSTITUTION ON TERMS *******************************************)
@@ -250,6 +251,17 @@ lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #{T1} ≤ #{T2}.
 /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
 qed-.
 
+lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶ [d, e] T →
+                      ∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H
+  elim (tps_inv_bind1 … H) -H #V2 #T2 #_ #HT12 #H destruct
+  elim (IH … HT12) -IH -L -T1 -d -e #L2 #T #HL12 #H destruct
+  @(ex2_2_intro … (⋆.ⓑ{I}V2@@L2)) /2 width=4/ /3 width=2/
+]
+qed-.
+
 (* Basic_1: removed theorems 25:
             subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
             subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
index c51873baa..f7f5e35c4 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma
@@ -69,6 +69,13 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
 #Hxy elim (H Hxy)
 qed-.
 
+lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥.
+#z #x elim x -x normalize
+[ #y <plus_n_Sm #H destruct
+| /3 width=2/
+]
+qed-.
+
 (* iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetcs/bigops.ma *)
diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 36b5fc2a3..afb5d5aae 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -156,3 +156,10 @@ for @{'eqF ? ? f g}.
 interpretation "functional extentional equality" 
 'eqF A B f g = (exteqF A B f g).
 
+(********** relations on unboxed pairs **********)
+
+definition bi_relation: Type[0] → Type[0] → Type[0]
+≝ λA,B.A→B→A→B→Prop.
+
+definition bi_reflexive: ∀A,B. ∀R :bi_relation A B. Prop
+≝ λA,B,R. ∀x,y. R x y x y.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 9e4efa32a..b51681d92 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1579,15 +1579,15 @@ let predefined_classes = [
  ["z"; "ζ"; "𝕫"; "𝐳"; "𝛇"; "ⓩ"; ] ;
  ["Z"; "ℨ"; "ℤ"; "𝐙"; "Ⓩ"; ] ;
  ["0"; "𝟘"; "⓪"; ] ;
- ["1"; "𝟙"; "①"; ] ;
- ["2"; "𝟚"; "②"; ] ;
- ["3"; "𝟛"; "③"; ] ;
- ["4"; "𝟜"; "④"; ] ;
- ["5"; "𝟝"; "⑤"; ] ;
- ["6"; "𝟞"; "⑥"; ] ;
- ["7"; "𝟟"; "⑦"; ] ;
- ["8"; "𝟠"; "⑧"; ] ;
- ["9"; "𝟡"; "⑨"; ] ;
+ ["1"; "𝟙"; "①"; "⓵"; ] ;
+ ["2"; "𝟚"; "②"; "⓶"; ] ;
+ ["3"; "𝟛"; "③"; "⓷"; ] ;
+ ["4"; "𝟜"; "④"; "⓸"; ] ;
+ ["5"; "𝟝"; "⑤"; "⓹"; ] ;
+ ["6"; "𝟞"; "⑥"; "⓺"; ] ;
+ ["7"; "𝟟"; "⑦"; "⓻"; ] ;
+ ["8"; "𝟠"; "⑧"; "⓼"; ] ;
+ ["9"; "𝟡"; "⑨"; "⓽"; ] ;
  ]
 ;;
 
-- 
2.39.2