From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 8 Feb 2007 15:24:44 +0000 (+0000)
Subject: definitions fixup
X-Git-Tag: make_still_working~6475
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=46cd94c978fc86ea330b61646a3029d31e1634bd;p=helm.git

definitions fixup
---

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
index 2cc467a30..4c4c9966d 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Inc/defs.ma
@@ -19,9 +19,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Inc/defs".
 
 include "SUB/Term/defs.ma".
 
-inductive Inc (q:Bool) (i:Nat): Head \to Nat \to Prop \def
-   | inc_bind: \forall r. Inc q i (bind q r) (succ i)
-   | inc_skip: \forall p. (q = p \to False) \to
-               \forall r. Inc q i (bind p r) i
-   | inc_flat: \forall p,r. Inc q i (flat p r) i   
+inductive Inc (i:Nat): Bool \to Head \to Nat \to Prop \def
+   | inc_bind: \forall r. Inc i true (bind r) (succ i)
+   | inc_skip: \forall r. Inc i false (bind r) i
+   | inc_flat: \forall r,q. Inc i q (flat r) i   
 .
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
index 0806d35e6..a6534047a 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Lift/defs.ma
@@ -18,7 +18,6 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
    - Usage: invoke with positive polarity
 *)
 
-include "SUB/Switch/defs.ma".
 include "SUB/Inc/defs.ma".
 
 inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
@@ -31,9 +30,9 @@ inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
    | lift_lref_ge: \forall l,i,j1. i <= j1 \to
                    \forall j2. (j1 + l == j2) \to
                    Lift true l i (leaf (lref j1)) (leaf (lref j2))
-   | lift_head   : \forall l,qt,qu,z. Switch qt z qu \to
-                   \forall iu,it. Inc qt iu z it \to
+   | lift_head   : \forall l,qt,qu,q. (qt -- q == qu) \to
+                   \forall z,iu,it. Inc iu qu z it \to
                    \forall u1,u2. Lift qu l iu u1 u2 \to
                    \forall t1,t2. Lift qt l it t1 t2 \to 
-                   Lift qt l iu (head z u1 t1) (head z u2 t2)
+                   Lift qt l iu (head q z u1 t1) (head q z u2 t2)
 .
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma
deleted file mode 100644
index 02470bbda..000000000
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Switch/defs.ma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/LAMBDA-TYPES/Unified-Sub/Switch/defs".
-
-(* POLARITY SWITCH RELATION
-*)
-
-include "SUB/Term/defs.ma".
-
-inductive Switch (q1:Bool): Head \to Bool \to Prop \def
-   | switch_bind: \forall q2,p. (p -- q1 == q2) \to
-                  \forall r. Switch q1 (bind p r) q2 
-   | switch_flat: \forall q2,p. (p -- q1 == q2) \to
-                  \forall r. Switch q1 (flat p r) q2 
-.
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
index 3d39b277d..b73935a07 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Unified/SUB/Term/defs.ma
@@ -44,11 +44,11 @@ inductive Flat: Set \def
 .
 
 inductive Head: Set \def
-   | bind: Bool \to Bind \to Head
-   | flat: Bool \to Flat \to Head
+   | bind: Bind \to Head
+   | flat: Flat \to Head
 .
 
 inductive Term: Set \def
    | leaf: Leaf \to Term
-   | head: Head \to Term \to Term \to Term
+   | head: Bool \to Head \to Term \to Term \to Term
 .