From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 25 Sep 2007 17:38:28 +0000 (+0000)
Subject: bug fix in Track definition
X-Git-Tag: make_still_working~5995
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=add325fb02ab0e46a2c7bbffb2e9c980128f0f69;p=helm.git

bug fix in Track definition
started PRed: parallel reduction simulating cut elimination
---

diff --git a/helm/software/matita/contribs/LOGIC/CLE/defs.ma b/helm/software/matita/contribs/LOGIC/CLE/defs.ma
index 7a2c7606c..31bd7694e 100644
--- a/helm/software/matita/contribs/LOGIC/CLE/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/CLE/defs.ma
@@ -7,7 +7,8 @@ include "datatypes/Context.ma".
 
 inductive CLE: Nat \to Context \to Prop \def
    | cle_zero: \forall Q. CLE zero Q
-   | cle_succ: \forall Q,R,i. CLE i Q \to CLE (succ i) (abst Q R)
+   | cle_succ: \forall Q,i. CLE i Q \to 
+               \forall p1,p2,R. CLE (succ i) (abst Q p1 p2 R)
 .
 
 interpretation "order relation between positions and contexts" 
diff --git a/helm/software/matita/contribs/LOGIC/Insert/defs.ma b/helm/software/matita/contribs/LOGIC/Insert/defs.ma
index 7b72c5c7c..a5c9b273a 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/Insert/defs.ma
@@ -17,10 +17,14 @@ set "baseuri" "cic:/matita/LOGIC/Insert/defs".
 (* INSERT RELATION FOR CONTEXTS
 *)
 
+include "Lift/defs.ma".
 include "datatypes/Context.ma".
 
-inductive Insert (S:Sequent): Nat \to Context \to Context \to Prop \def
-   | insert_zero: \forall P. Insert S zero P (abst P S)
-   | insert_succ: \forall P,Q,R,i. 
-                  Insert S i P Q \to Insert S (succ i) (abst P R) (abst Q R)
+inductive Insert (p,q:Proof) (S:Sequent): 
+                 Nat \to Context \to Context \to Prop \def
+   | insert_zero: \forall P. Insert p q S zero P (abst P p q S)
+   | insert_succ: \forall P,Q,i. Insert p q S i P Q \to 
+                  \forall p1,p2. Lift i (succ zero) p1 p2 \to 
+                  \forall q1,q2. Lift i (succ zero) q1 q2 \to \forall R. 
+                  Insert p q S (succ i) (abst P p1 q1 R) (abst Q p2 q2 R)
 .
diff --git a/helm/software/matita/contribs/LOGIC/Insert/fun.ma b/helm/software/matita/contribs/LOGIC/Insert/fun.ma
index 5661c0a27..f0cc5e514 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/fun.ma
+++ b/helm/software/matita/contribs/LOGIC/Insert/fun.ma
@@ -18,7 +18,7 @@ include "CLE/defs.ma".
 include "Insert/inv.ma".
 
 (* Functional properties ****************************************************)
-
+(*
 theorem insert_total: \forall S,i,P. i <= P \to \exists Q. Insert S i P Q.
  intros 4; elim H; clear H i P;
  decompose; autobatch.
@@ -31,3 +31,4 @@ theorem insert_inj: \forall S1,i,P, Q. Insert S1 i P Q \to
  | lapply linear insert_inv_succ to H3; decompose; subst; autobatch
  ].
 qed.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/Insert/inv.ma b/helm/software/matita/contribs/LOGIC/Insert/inv.ma
index 229b9cc33..b612858a3 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/inv.ma
+++ b/helm/software/matita/contribs/LOGIC/Insert/inv.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LOGIC/Insert/inv".
 *)
 
 include "Insert/defs.ma".
-
+(*
 theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S.
  intros; inversion H; clear H; intros; subst; autobatch.
 qed.
@@ -54,3 +54,4 @@ theorem insert_inv_abst_2: \forall P,i. \forall R,S:Sequent.
  | clear H1. lapply linear insert_inv_leaf_2 to H. decompose
  ].
 qed.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/Insert/props.ma b/helm/software/matita/contribs/LOGIC/Insert/props.ma
index 1e0bc5454..6daa22ea6 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/props.ma
+++ b/helm/software/matita/contribs/LOGIC/Insert/props.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LOGIC/Insert/props".
 *)
 
 include "Insert/fun.ma".
-
+(*
 theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to 
                      \forall Q2,S2,i2. Insert S2 i2 P Q2 \to
                      \exists Q,j1,j2. 
@@ -70,3 +70,4 @@ theorem insert_conf_rev_full: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to
  | autobatch depth = 7 size = 8
  ].
 qed.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/Lift/defs.ma b/helm/software/matita/contribs/LOGIC/Lift/defs.ma
new file mode 100644
index 000000000..ae4f9cb0a
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/Lift/defs.ma
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LOGIC/Lift/defs".
+
+(* PROOF RELOCATION
+*)
+
+include "datatypes/Proof.ma".
+
+inductive Lift: Nat \to Nat \to Proof \to Proof \to Prop \def
+   | lift_lref_lt: \forall jd,jh,i. i < jd \to Lift jd jh (lref i) (lref i)
+   | lift_lref_ge: \forall jd,jh,i1,i2. jd <= i1 \to (i1 + jh == i2) \to 
+                   Lift jd jh (lref i1) (lref i2)
+   | lift_prin   : \forall jd,jh,h. Lift jd jh (prin h) (prin h)
+   | lift_impw   : \forall jd,jh,p1,p2. 
+                   Lift jd jh p1 p2 \to Lift jd jh (impw p1) (impw p2)
+   | lift_impr   : \forall jd,jh,p1,p2. 
+                   Lift jd jh p1 p2 \to Lift jd jh (impr p1) (impr p2)
+   | lift_impi   : \forall jd,jh,p1,p2. Lift jd jh p1 p2 \to 
+                   \forall q1,q2. Lift jd jh q1 q2 \to
+                   \forall r1,r2. Lift (succ jd) jh r1 r2 \to 
+                   Lift jd jh (impi p1 q1 r1) (impi p2 q2 r2)
+   | lift_scut   : \forall jd,jh,p1,p2. Lift jd jh p1 p2 \to 
+                   \forall q1,q2. Lift jd jh q1 q2 \to
+                   Lift jd jh (scut p1 q1) (scut p2 q2)
+.
diff --git a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
index b04cf4bd1..1bf18389f 100644
--- a/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/NTrack/defs.ma
@@ -17,9 +17,8 @@ set "baseuri" "cic:/matita/LOGIC/NTrack/defs".
 (* NORMAL PROOF TREE TRACKS
 *)
 
-include "datatypes/Proof.ma".
 include "Insert/defs.ma".
-
+(*
 inductive NTrack: Context \to Proof \to Sequent \to Prop \def
    | ntrack_proj: \forall P,Q,S,i. Insert S i P Q \to NTrack Q (lref i) S
    | ntrack_posr: \forall P,h.
@@ -36,3 +35,4 @@ inductive NTrack: Context \to Proof \to Sequent \to Prop \def
 		  Insert (pair A B) i P Q \to
 		  NTrack P (impi p q r) (pair (impl a b) D)
 .
+*)
diff --git a/helm/software/matita/contribs/LOGIC/NTrack/inv.ma b/helm/software/matita/contribs/LOGIC/NTrack/inv.ma
index 9f334f19f..6c57c2040 100644
--- a/helm/software/matita/contribs/LOGIC/NTrack/inv.ma
+++ b/helm/software/matita/contribs/LOGIC/NTrack/inv.ma
@@ -15,7 +15,7 @@
 set "baseuri" "cic:/matita/LOGIC/NTrack/inv".
 
 include "NTrack/defs.ma".
-
+(*
 theorem ntrack_inv_lref: \forall Q,S,i. NTrack Q (lref i) S \to
                          \exists P. Insert S i P Q.
  intros; inversion H; clear H; intros; subst; autobatch.
@@ -63,3 +63,4 @@ theorem ntrack_inv_lleaf_impl:
  | subst; autobatch depth = 4
  ].
 qed.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/NTrack/order.ma b/helm/software/matita/contribs/LOGIC/NTrack/order.ma
index 2b41ad83e..11868b6ef 100644
--- a/helm/software/matita/contribs/LOGIC/NTrack/order.ma
+++ b/helm/software/matita/contribs/LOGIC/NTrack/order.ma
@@ -18,7 +18,7 @@ include "Track/order.ma".
 include "NTrack/props.ma".
 
 (* Order properties *********************************************************)
-
+(*
 theorem ntrack_refl: \forall P. \forall c:Formula. \exists r. 
                      NTrack P r (pair c c).
  intros; elim c; clear c;
@@ -36,3 +36,4 @@ theorem ntrack_trans: \forall p,q,A,B. \forall c:Formula.
  lapply linear ntrack_track to H1 as H;
  lapply linear track_trans to H0, H as H1; decompose;
 *)
+*)
diff --git a/helm/software/matita/contribs/LOGIC/NTrack/props.ma b/helm/software/matita/contribs/LOGIC/NTrack/props.ma
index a7edc402f..7d41aebdf 100644
--- a/helm/software/matita/contribs/LOGIC/NTrack/props.ma
+++ b/helm/software/matita/contribs/LOGIC/NTrack/props.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/LOGIC/NTrack/props".
 include "Insert/props.ma".
 include "Track/defs.ma".
 include "NTrack/inv.ma".
-
+(*
 theorem ntrack_weak: \forall R,p,P,Q,S,i. 
                      NTrack P p S \to Insert R i P Q \to 
                      \exists q. NTrack Q q S.
@@ -60,3 +60,4 @@ qed.
 theorem ntrack_track: \forall R,p,P. NTrack P p R \to Track P p R.
  intros; elim H names 0; clear H P p R; intros; autobatch width = 4.
 qed.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/PNF/defs.ma b/helm/software/matita/contribs/LOGIC/PNF/defs.ma
index 12a3b7be8..feea35b43 100644
--- a/helm/software/matita/contribs/LOGIC/PNF/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/PNF/defs.ma
@@ -18,7 +18,8 @@ set "baseuri" "cic:/matita/LOGIC/PNF/defs".
 *)
 
 include "PRed/defs.ma".
-
+(*
 inductive PNF: Proof \to Prop \def
    | pnf: \forall p. (\forall q. p => q \to p = q) \to PNF p
 .
+*)
diff --git a/helm/software/matita/contribs/LOGIC/PRed/defs.ma b/helm/software/matita/contribs/LOGIC/PRed/defs.ma
index 36b431098..ef0f86194 100644
--- a/helm/software/matita/contribs/LOGIC/PRed/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/PRed/defs.ma
@@ -18,22 +18,40 @@ set "baseuri" "cic:/matita/LOGIC/PRed/defs".
    For cut elimination 
 *)
 
-include "datatypes/Proof.ma".
-
-inductive PRed: Proof \to Proof \to Prop \def
-   | pred_lref: \forall i. PRed (lref i) (lref i)
-   | pred_parx: \forall h. PRed (parx h) (parx h)
-   | pred_impw: \forall p1,p2. PRed p1 p2 \to PRed (impw p1) (impw p2)
-   | pred_impr: \forall p1,p2. PRed p1 p2 \to PRed (impr p1) (impr p2)
-   | pred_impi: \forall p1,p2. PRed p1 p2 \to \forall q1,q2. PRed q1 q2 \to
-                \forall r1,r2. PRed r1 r2 \to 
-		PRed (impi p1 q1 r1) (impi p2 q2 r2)
-   | pred_scut: \forall p1,p2. PRed p1 p2 \to \forall q1,q2. PRed q1 q2 \to
-                PRed (scut p1 q1) (scut p2 q2)
+include "Insert/defs.ma".
+ 
+inductive PRed: Context \to Proof \to Sequent \to 
+                Context \to Proof \to Sequent \to Prop \def
+   | pred_lref: \forall P,i,S. PRed P (lref i) S P (lref i) S
+   | pred_prin: \forall P,h,S. PRed P (prin h) S P (prin h) S
+   | pred_impw: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to 
+                \forall S. PRed Q1 (impw p1) S Q2 (impw p2) S
+   | pred_impr: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to
+                \forall S. PRed Q1 (impr p1) S Q2 (impr p2) S
+   | pred_impi: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to
+                \forall q1,q2. (\forall S. PRed Q1 q1 S Q2 q2 S) \to
+                \forall r1,r2. (\forall S,R. PRed (abst Q1 p1 q1 R) r1 S (abst Q2 p2 q2 R) r2 S) \to 
+                \forall S. PRed Q1 (impi p1 q1 r1) S Q2 (impi p2 q2 r2) S
+   | pred_scut: \forall Q1,Q2,p1,p2. (\forall S. PRed Q1 p1 S Q2 p2 S) \to 
+                \forall q1,q2. (\forall S. PRed Q1 q1 S Q2 q2 S) \to
+                \forall S. PRed Q1 (scut p1 q1) S Q2 (scut p2 q2) S
+   | pred_a_sx: \forall p1,p2,R,P,Q1,i. Insert p1 p2 R i P Q1 \to
+                \forall q0,S,Q2. Insert p1 (scut p2 q0) S i P Q2 \to
+                \forall q. Lift zero i q0 q \to
+		PRed Q1 (scut (lref i) q) S Q2 (lref i) S
+   | pred_a_dx: \forall q1,q2,R,P,Q1,i. Insert q1 q2 R i P Q1 \to
+                \forall p0,S,Q2. Insert (scut p0 q1) q2 S i P Q2 \to
+                \forall p. Lift zero i p0 p \to
+		PRed Q1 (scut p (lref i)) S Q2 (lref i) S
+   | pred_b_sx: \forall q1,q2,P1,P2,S. PRed P1 q1 S P2 q2 S \to 
+                \forall h. PRed P1 (scut (prin h) q1) S P2 q2 S
+   | pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
+                \forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S
 .
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation 
    "single step parallel reduction in B->"
-   'parred x y = (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x y)
+   'parred3 x1 y1 z1 x2 y2 z2 = 
+      (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x1 y1 z1 x2 y2 z2)
 .
diff --git a/helm/software/matita/contribs/LOGIC/Track/defs.ma b/helm/software/matita/contribs/LOGIC/Track/defs.ma
index c5e6e69be..25cf7c0b5 100644
--- a/helm/software/matita/contribs/LOGIC/Track/defs.ma
+++ b/helm/software/matita/contribs/LOGIC/Track/defs.ma
@@ -17,24 +17,23 @@ set "baseuri" "cic:/matita/LOGIC/Track/defs".
 (* PROOF TREE TRACKS
 *)
 
-include "datatypes/Proof.ma".
 include "Insert/defs.ma".
 
 inductive Track: Context \to Proof \to Sequent \to Prop \def
-   | track_proj: \forall P,Q,S,i. Insert S i P Q \to Track Q (lref i) S
+   | track_proj: \forall P,Q,p1,p2,S,i. 
+                 Insert p1 p2 S i P Q \to Track Q (lref i) S
    | track_posr: \forall P,h.
-                 Track P (parx h) (pair (posr h) (posr h))
+                 Track P (prin h) (pair (posr h) (posr h))
    | track_impw: \forall P,r,D,a,b. Track P r (pair lleaf D) \to
                  Track P (impw r) (pair (impl a b) D)
    | track_impr: \forall P,r. \forall a,b:Formula. 
                  Track P r (pair a b) \to 
                  Track P (impr r) (pair lleaf (impl a b))
-   | track_impi: \forall P,Q,p,q,r,A,B,D,i. \forall a,b:Formula.
+   | track_impi: \forall P,p,q,r,A,B,D. \forall a,b:Formula.
                  Track P p (pair A a) \to
                  Track P q (pair b B) \to
-		 Track Q r (pair lleaf D) \to
-		 Insert (pair A B) i P Q \to
-		 Track P (impi p q r) (pair (impl a b) D)
+                 Track (abst P p q (pair A B)) r (pair lleaf D) \to
+                 Track P (impi p q r) (pair (impl a b) D)
    | track_scut: \forall P,p,q,A,B. \forall c:Formula.
                  Track P p (pair A c) \to
                  Track P q (pair c B) \to
diff --git a/helm/software/matita/contribs/LOGIC/Track/inv.ma b/helm/software/matita/contribs/LOGIC/Track/inv.ma
new file mode 100644
index 000000000..77d1107cd
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/Track/inv.ma
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LOGIC/Track/inv".
+
+include "Track/defs.ma".
+
+(* Main inversion lemmas ****************************************************)
+
+theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
+                        \exists p1,p2,P. Insert p1 p2 S i P Q.
+ intros; inversion H; clear H; intros; subst; autobatch depth = 4.
+qed.
+
+theorem track_inv_prin: \forall P,S,h. Track P (prin h) S \to
+                        S = pair (posr h) (posr h).
+ intros; inversion H; clear H; intros; subst; autobatch.
+qed.
+
+theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
+                        \exists B,a,b. 
+                        S = pair (impl a b) B \land 
+                        Track P p (pair lleaf B).
+ intros; inversion H; clear H; intros; subst; autobatch depth = 5.
+qed.
+
+theorem track_inv_impr: \forall Q,p,S. Track Q (impr p) S \to
+                        \exists a,b:Formula. 
+                        S = pair lleaf (impl a b) \land
+                        Track Q p (pair a b).
+ intros; inversion H; clear H; intros; subst; autobatch depth = 4.
+qed.
+
+theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to
+                        \exists A,B,D. \exists a,b:Formula.
+                        S = pair (impl a b) D \land
+                        Track P p (pair A a) \land
+                        Track P q (pair b B) \land
+                        Track (abst P p q (pair A B)) r (pair lleaf D).
+ intros; inversion H; clear H; intros; subst; autobatch depth = 9 width = 4 size = 12.
+qed.
+
+theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to
+                        \exists A,B. \exists c:Formula.
+                        S = pair A B \land
+                        Track P q (pair A c) \land
+                        Track P r (pair c B).
+ intros; inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. 
+qed.
diff --git a/helm/software/matita/contribs/LOGIC/Track/order.ma b/helm/software/matita/contribs/LOGIC/Track/order.ma
index 6487433dd..2c90f3303 100644
--- a/helm/software/matita/contribs/LOGIC/Track/order.ma
+++ b/helm/software/matita/contribs/LOGIC/Track/order.ma
@@ -18,7 +18,7 @@ include "Insert/fun.ma".
 include "Track/defs.ma".
 
 (* Order properties *********************************************************)
-
+(*
 theorem track_refl: \forall P. \forall c:Formula. \exists r. 
                     Track P r (pair c c).
  intros; elim c; clear c;
@@ -33,3 +33,4 @@ theorem track_trans: \forall P,p,q,A,B. \forall c:Formula.
                      \exists r. Track P r (pair A B).
  intros; autobatch.
 qed.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/Track/pred.ma b/helm/software/matita/contribs/LOGIC/Track/pred.ma
new file mode 100644
index 000000000..3b640b97c
--- /dev/null
+++ b/helm/software/matita/contribs/LOGIC/Track/pred.ma
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LOGIC/Track/pred".
+
+(**)
+
+include "Track/inv.ma".
+include "PRed/defs.ma".
+
+theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. PRed Q1 p1 S1 Q2 p2 S2 \to
+                    Track Q1 p1 S1 \to Track Q2 p2 S2.
+ intros 7; elim H; clear H Q1 Q2 p1 p2 S1 S2;
+ [ autobatch
+ | autobatch
+ | lapply linear track_inv_impw to H3; decompose; subst; autobatch
+ | lapply linear track_inv_impr to H3; decompose; subst; autobatch
+ | lapply linear track_inv_impi to H7; decompose; subst; autobatch size = 7
+ | lapply linear track_inv_scut to H5; decompose; subst; autobatch
+ | lapply linear track_inv_scut to H4; decompose; subst;
+   lapply linear track_inv_lref to H6; decompose; autobatch
+ | lapply linear track_inv_scut to H4; decompose; subst;
+   lapply linear track_inv_lref to H5; decompose; autobatch
+ | lapply linear track_inv_scut to H3; decompose; subst;
+   lapply linear track_inv_prin to H5; subst; autobatch
+ | lapply linear track_inv_scut to H3; decompose; subst;
+   lapply linear track_inv_prin to H4; subst; autobatch
+ ].
+qed.
diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma b/helm/software/matita/contribs/LOGIC/datatypes/Context.ma
index 0de237801..44d626648 100644
--- a/helm/software/matita/contribs/LOGIC/datatypes/Context.ma
+++ b/helm/software/matita/contribs/LOGIC/datatypes/Context.ma
@@ -19,13 +19,15 @@ set "baseuri" "cic:/matita/LOGIC/datatypes/Context".
      - contexts: P Q
 *)
 
+include "datatypes/Proof.ma".
 include "datatypes/Sequent.ma".
 
 inductive Context: Type \def
    | leaf: Context
-   | abst: Context \to Sequent \to Context
+   | abst: Context \to Proof \to Proof \to Sequent \to Context
 .
-
+(*
 definition inj: Sequent \to Context \def abst leaf.
 
 coercion cic:/matita/LOGIC/datatypes/Context/inj.con.
+*)
diff --git a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma b/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma
index 357b044f5..f6260b026 100644
--- a/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma
+++ b/helm/software/matita/contribs/LOGIC/datatypes/Proof.ma
@@ -23,7 +23,7 @@ include "preamble.ma".
 
 inductive Proof: Type \def
    | lref: Nat \to Proof                       (* projection         *)
-   | parx: Nat \to Proof                       (*                    *)
+   | prin: Nat \to Proof                       (* pos rel inhabitant *)
    | impw: Proof \to Proof                     (* weakening          *)
    | impr: Proof \to Proof                     (* right introduction *)
    | impi: Proof \to Proof \to Proof \to Proof (* left introduction  *)
diff --git a/helm/software/matita/contribs/LOGIC/preamble.ma b/helm/software/matita/contribs/LOGIC/preamble.ma
index 9f28e1bd3..b1e50f811 100644
--- a/helm/software/matita/contribs/LOGIC/preamble.ma
+++ b/helm/software/matita/contribs/LOGIC/preamble.ma
@@ -19,4 +19,4 @@ set "baseuri" "cic:/matita/LOGIC/preamble".
 (* PREAMBLE
 *)
 
-include "../RELATIONAL/datatypes/Nat.ma".
+include "../RELATIONAL/NLE/defs.ma".