From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 9 Apr 2009 18:59:12 +0000 (+0000)
Subject: - character: we adjusted some "autobatch" parameters
X-Git-Tag: make_still_working~4091
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04f75822f22c6c6522f6d81b412a212885a6ff72;p=helm.git

- character: we adjusted some "autobatch" parameters
- limits: in classes and subssets we now ensure the compatibility between the
  inhabitance predicate and the equivalence relation
---

diff --git a/helm/software/matita/contribs/character/classes/defs.ma b/helm/software/matita/contribs/character/classes/defs.ma
index add242cc4..8283373db 100644
--- a/helm/software/matita/contribs/character/classes/defs.ma
+++ b/helm/software/matita/contribs/character/classes/defs.ma
@@ -16,17 +16,18 @@ include "preamble.ma".
 
 (* NOTE: OEIS sequence identifiers 
    P(n): A016777 "3n+1"
-*)         
+   T(n): A155504 "(3h+1)*3^(k+1)"
+*)
 
-inductive P: nat \to Prop \def
+inductive P: nat → Prop ≝
    | p1: P 1
-   | p2: \forall i,j. T i \to P j \to P (i + j)
-with T: nat \to Prop \def
-   | t1: \forall i. P i \to T (i * 3)
-   | t2: \forall i. T i \to T (i * 3)
+   | p2: ∀i,j. T i → P j → P (i + j)
+with T: nat → Prop ≝
+   | t1: ∀i. P i → T (i * 3)
+   | t2: ∀i. T i → T (i * 3)
 .
 
-inductive S: nat \to Prop \def
-   | s1: \forall i. P i \to S (i * 2)
-   | s2: \forall i. T i \to S (i * 2)
+inductive S: nat → Prop ≝
+   | s1: ∀i. P i → S (i * 2)
+   | s2: ∀i. T i → S (i * 2)
 .
diff --git a/helm/software/matita/contribs/character/classes/props_pt.ma b/helm/software/matita/contribs/character/classes/props_pt.ma
index 64b424ae3..82526c26a 100644
--- a/helm/software/matita/contribs/character/classes/props_pt.ma
+++ b/helm/software/matita/contribs/character/classes/props_pt.ma
@@ -14,7 +14,7 @@
 
 include "classes/defs.ma".
 
-theorem p_inv_O: P 0 \to False.
+theorem p_inv_O: P 0 → False.
  intros; inversion H; clear H; intros;
  [ destruct
  | lapply linear plus_inv_O3 to H3; decompose; destruct; 
@@ -22,28 +22,28 @@ theorem p_inv_O: P 0 \to False.
  ].
 qed.
 
-theorem t_inv_O: T 0 \to False.
+theorem t_inv_O: T 0 → False.
  intros; inversion H; clear H; intros;
  [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
  | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
  ].
 qed.
 
-theorem p_pos: \forall i. P i \to \exists k. i = S k.
+theorem p_pos: ∀i. P i → ∃k. i = S k.
  intros 1; elim i names 0; clear i; intros;
  [ lapply linear p_inv_O to H; decompose
  | autobatch depth = 2
  ].
 qed.
 
-theorem t_pos: \forall i. T i \to \exists k. i = S k.
+theorem t_pos: ∀i. T i → ∃k. i = S k.
  intros 1; elim i names 0; clear i; intros;
  [ lapply linear t_inv_O to H; decompose
  | autobatch depth = 2
  ].
 qed.
 
-theorem t_1: T 1 \to False.
+theorem t_1: T 1 → False.
  intros; inversion H; clear H; intros;
  [ lapply not_3_divides_1 to H1; decompose
  | lapply not_3_divides_1 to H2; decompose
@@ -51,18 +51,18 @@ theorem t_1: T 1 \to False.
 qed.
 
 theorem t_3: T 3.
- change in \vdash (? %) with (1 * 3);
+ change in ⊢ (? %) with (1 * 3);
  autobatch depth = 2.
 qed.
 
-theorem pt_inv_gen: \forall i. 
-                    (P i \to \exists h. i = S (h * 3)) \land
-                    (T i \to \exists h,k. i = S (h * 3) * 3 \sup (S k)).
+theorem pt_inv_gen: ∀i. 
+                    (P i → ∃h. i = S (h * 3)) ∧
+                    (T i → ∃h,k. i = S (h * 3) * 3 \sup (S k)).
  intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
  [ lapply linear p_inv_O to H; decompose
  | lapply linear t_inv_O to H; decompose
  | inversion H1; clear H1; intros;
-   [ destruct; autobatch depth = 3 width = 50 size = 50
+   [ destruct; autobatch paramodulation
    | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
      lapply linear plus_inv_S_S_S to H4; decompose;
      lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
@@ -78,31 +78,31 @@ theorem pt_inv_gen: \forall i.
    | clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
      lapply linear H to H0; decompose; clear H;
      lapply linear H2 to H1; decompose; destruct;
-     autobatch depth = 3
+     autobatch depth = 4
    ]
  ].
 qed.
 
-theorem p_inv_gen: \forall i. P i \to \exists h. i = S (h * 3).
+theorem p_inv_gen: ∀i. P i → ∃h. i = S (h * 3).
  intros; lapply depth = 1 pt_inv_gen; decompose;
  lapply linear H1 to H as H0; autobatch depth = 1.
 qed.
 
-theorem t_inv_gen: \forall i. T i \to \exists h,k. i = (S (h * 3)) * 3 \sup (S k).
+theorem t_inv_gen: ∀i. T i → ∃h,k. i = (S (h * 3)) * 3 \sup (S k).
  intros; lapply depth = 1 pt_inv_gen; decompose;
  lapply linear H2 to H as H0; autobatch depth = 2.
 qed.
 
-theorem p_gen: \forall i. P (S (i * 3)).
+theorem p_gen: ∀i. P (S (i * 3)).
  intros; elim i names 0; clear i; intros;
  [ simplify; autobatch depth = 2
  | rewrite > plus_3_S3n ; autobatch depth = 2
  ].
 qed.
 
-theorem t_gen: \forall i,j. T (S (i * 3) * 3 \sup (S j)).
+theorem t_gen: ∀i,j. T (S (i * 3) * 3 \sup (S j)).
  intros; elim j names 0; clear j; intros;
- [ simplify in \vdash (? (? ? %)); autobatch depth = 2
+ [ simplify in ⊢ (? (? ? %)); autobatch depth = 2
  | rewrite > times_exp_x_y_Sz; autobatch depth = 2
  ].
 qed.
diff --git a/helm/software/matita/contribs/character/preamble.ma b/helm/software/matita/contribs/character/preamble.ma
index ac3f19c6e..34ac9671e 100644
--- a/helm/software/matita/contribs/character/preamble.ma
+++ b/helm/software/matita/contribs/character/preamble.ma
@@ -17,55 +17,53 @@ include "nat/relevant_equations.ma".
 
 alias num (instance 0) = "natural number".
 
-theorem plus_inv_O3: \forall m,n. 0 = n + m \to 0 = n \land 0 = m.
+theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
  intros 2; elim n names 0; clear n; simplify; intros;
  [ autobatch | destruct ].
 qed. 
 
-theorem times_inv_O3_S: \forall x,y. 0 = x * (S y) -> x = 0.
- intros; rewrite < times_n_Sm in H; 
+theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
+ intros; rewrite < times_n_Sm in H;
  lapply linear plus_inv_O3 to H; decompose; destruct; autobatch.
 qed. 
 
-theorem not_3_divides_1: \forall n. 1 = n * 3 \to False.
+theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
  intros 1; rewrite > sym_times; simplify;
  elim n names 0; simplify; intros; destruct;
  rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
 qed.
 
-theorem le_inv_S_S: \forall m,n. S m <= S n \to m <= n.
+theorem le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n.
  intros; inversion H; clear H; intros; destruct; autobatch.
 qed.
 
-theorem plus_inv_S_S_S: \forall x,y,z. S x = S y + S z \to S y <= x \land S z <= x.
+theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
  simplify; intros; destruct;
- rewrite < plus_n_Sm in \vdash (? (? ? %) ?); autobatch depth = 3.
+ rewrite < plus_n_Sm in ⊢ (? (? ? %) ?); autobatch.
 qed.
 
-theorem times_inv_S_m_SS: \forall k,n,m. S n = m * (S (S k)) \to m \le n.
+theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
  intros 3; elim m names 0; clear m; simplify; intros; destruct;
  clear H; apply le_S_S; rewrite < sym_times; simplify;
  autobatch depth = 2.
 qed.
 
-theorem plus_3_S3n: \forall n. S (S n * 3) = 3 + S (n * 3).
- intros; simplify; autobatch.
+theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
+ intros; simplify; autobatch depth = 1.
 qed. 
 
-theorem times_exp_x_y_Sz: \forall x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
+theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
  intros; simplify; autobatch depth = 1.
 qed.  
 
-definition acc_nat \def \lambda P:nat \to Prop. \lambda n. 
-                   \forall m. m <= n \to P m.
+definition acc_nat: (nat → Prop) → nat →Prop ≝
+   λP:nat→Prop. λn. ∀m. m ≤ n → P m.
 
-theorem wf_le: \forall P. 
-               P 0 \to (\forall n. acc_nat P n \to P (S n)) \to
-               \forall n. acc_nat P n.
+theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
  unfold acc_nat; intros 4; elim n names 0; clear n;
  [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch
  | intros 3; elim m; clear m; intros; clear H3;
-   [ clear H H1; autobatch
+   [ clear H H1; autobatch depth = 2
    | clear H; lapply linear le_inv_S_S to H4;
      apply H1; clear H1; intros;
      apply H2; clear H2; autobatch depth = 2
@@ -73,10 +71,8 @@ theorem wf_le: \forall P.
  ].
 qed.
 
-theorem wf_nat_ind: \forall P:nat \to Prop.
-                    P O \to
-                    (\forall n. (\forall m. m <= n \to P m) \to P (S n)) \to
-                    \forall n. P n.
+theorem wf_nat_ind: 
+   ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
  intros; lapply linear depth=2 wf_le to H, H1 as H0; 
- unfold acc_nat in H0; apply (H0 n n); autobatch.
+ unfold acc_nat in H0; apply (H0 n n); autobatch depth = 1.
 qed.
diff --git a/helm/software/matita/contribs/limits/Class/defs.ma b/helm/software/matita/contribs/limits/Class/defs.ma
index bbb071b50..429a6a17f 100644
--- a/helm/software/matita/contribs/limits/Class/defs.ma
+++ b/helm/software/matita/contribs/limits/Class/defs.ma
@@ -14,7 +14,7 @@
 
 include "preamble.ma".
 
-(* ACZEL CATEGORIES
+(* CLASSES:
    - We use typoids with a compatible membership relation
    - The category is intended to be the domain of the membership relation
    - The membership relation is necessary because we need to regard the
@@ -27,19 +27,43 @@ include "preamble.ma".
 *) 
 
 record Class: Type ≝ {
-   class:> Type;
-   cin: class → Prop;
-   ces: class → class \to Prop
+   class     :> Type;
+   cin       :  class → Prop;
+   ces       :  class → class → Prop;
+   ces_cin_fw:  ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
+   ces_cin_bw:  ∀c1,c2. cin c1 → ces c2 c1 → cin c2
 }.
 
-(* default inhabitance predicates *)
-definition true_f ≝ λ(X:Type). λ(_:X). True.
-definition false_f ≝ λ(X:Type). λ(_:X). False.
+(* equality predicate *******************************************************)
 
-(* equality predicate *)
 inductive ceq (C:Class): class C → class C → Prop ≝
-   | ceq_refl : ∀c. cin ? c → ceq ? c c
-   | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
-   | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
+   | ceq_refl : ∀c. ceq ? c c
+   | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
+   | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
 .
 
+(* default inhabitance predicates *******************************************)
+
+definition true_f ≝ λX:Type. λ_:X. True.
+
+definition false_f ≝ λX:Type. λ_:X. False.
+
+(* default foreward compatibilities *****************************************)
+
+theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
+intros; autobatch.
+qed.
+
+definition true_fw ≝ const_fw True.
+
+definition false_fw ≝ const_fw False.
+
+(* default backward compatibilities *****************************************)
+
+theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
+intros; autobatch.
+qed.
+
+definition true_bw ≝ const_bw True.
+
+definition false_bw ≝ const_bw False.
diff --git a/helm/software/matita/contribs/limits/Class/eq.ma b/helm/software/matita/contribs/limits/Class/eq.ma
index 69d6836d8..003365bf4 100644
--- a/helm/software/matita/contribs/limits/Class/eq.ma
+++ b/helm/software/matita/contribs/limits/Class/eq.ma
@@ -14,31 +14,31 @@
 
 include "Class/defs.ma".
 
-(* ACZEL CATEGORIES:
+(* CLASSES:
    - Here we prove the standard properties of the equality.
 *)
 
-theorem ceq_cin_sx: ∀C,c1,c2. ceq C c1 c2 → cin ? c1.
-intros; elim H; clear H c1 c2; autobatch.
+theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2.
+intros 4; elim H; clear H c1 c2; autobatch.
 qed.
 
-theorem ceq_cin_dx: ∀C,c1,c2. ceq C c1 c2 → cin ? c2.
-intros; elim H; clear H c1 c2; autobatch.
+theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1.
+intros 4; elim H; clear H c1 c2; autobatch.
 qed.
 
 theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3.
 intros 4; elim H; clear H c1 c2; autobatch.
 qed.
 
-theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
-intros 4; elim H; clear H c1 c2; autobatch depth = 4.
+theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
+intros; elim H; clear H c1 c2; autobatch.
 qed.
 
-theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1.
-intros; autobatch depth = 4.
+theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3.
+intros; autobatch.
 qed.
 
 theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 →
-                      ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
+                  ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2.
 intros; autobatch.
 qed.
diff --git a/helm/software/matita/contribs/limits/Domain/data.ma b/helm/software/matita/contribs/limits/Domain/data.ma
index f18e43279..690b9483d 100644
--- a/helm/software/matita/contribs/limits/Domain/data.ma
+++ b/helm/software/matita/contribs/limits/Domain/data.ma
@@ -19,7 +19,9 @@ include "Domain/defs.ma".
 *)
 
 definition DBool: Domain ≝
-   mk_Domain (mk_Class bool (true_f ?) (eq ?)).
+   mk_Domain (
+      mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+   ).
 (*
 definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
    \lambda C,c0,c1,b.
@@ -29,7 +31,9 @@ definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def
       ].
 *)
 definition DVoid: Domain ≝
-   mk_Domain (mk_Class void (true_f ?) (eq ?)).
+   mk_Domain (
+      mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?)
+   ).
 (*
 definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def
    \lambda C,v.
diff --git a/helm/software/matita/contribs/limits/Subset/defs.ma b/helm/software/matita/contribs/limits/Subset/defs.ma
index 6dbab4b39..729bdaba9 100644
--- a/helm/software/matita/contribs/limits/Subset/defs.ma
+++ b/helm/software/matita/contribs/limits/Subset/defs.ma
@@ -15,44 +15,124 @@
 include "Domain/defs.ma".
 
 (* SUBSETS
-   - We use predicative subsets coded as propositional functions
-     according to G.Sambin and S.Valentini "Toolbox".
+   - We use predicative subsets encoded as propositional functions
+     according to Sambin/Valentini "Toolbox".
 *)
 
-definition Subset ≝ λD:Domain. D → Prop.
+record Subset (D:Domain): Type ≝ {
+   subset       :1> D → Prop;
+   ces_subset_fw:   ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
+   ces_subset_bw:   ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
+}.
 
-(* subset membership (epsilon) *)
-definition sin : ∀D. Subset D → D → Prop ≝
-   λD:Domain. λU,d. cin D d ∧ U d.
+(* subset membership (epsilon) ********************************************)
 
-(* subset top (full subset) *)
-definition stop ≝ λD:Domain. true_f D.
+definition sin: ∀D. Subset D → D → Prop ≝
+   λD. λU:Subset D. λd. cin D d ∧ U d.
 
-coercion stop.
+theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
+ unfold sin; intros; autobatch.
+qed.
 
-(* subset bottom (empty subset) *)
-definition sbot ≝ λD:Domain. false_f D.
+theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
+ intros; decompose; autobatch.
+qed.
+
+theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
+ intros; decompose; autobatch.
+qed.
+
+(* the domain built upon a subset *****************************************)
+
+theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
+ intros; 
+ apply sin_i; 
+ [ autobatch
+ | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ]. 
+qed.
+
+theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
+ intros; 
+ apply sin_i; 
+ [ autobatch
+ | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ]. 
+qed.
+
+definition domain_of_subset: ∀D. Subset D → Domain ≝
+   λD:Domain. λU.
+   mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
+
+coercion domain_of_subset.
+
+(* subset top (full subset) ***********************************************)
+
+definition stop: ∀D. Subset D ≝
+   λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
+
+coercion stop nocomposites.
+
+(* subset bottom (empty subset) *******************************************)
+
+definition sbot: ∀D. Subset D ≝
+   λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
+
+(* subset and (binary intersection) ***************************************)
+
+theorem ces_sand_fw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sand_bw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
 
-(* subset and (binary intersection) *)
 definition sand: ∀D. Subset D → Subset D → Subset D ≝
-   λD,U1,U2,d. U1 d ∧ U2 d. 
+   λD,U1,U2. 
+   mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
+
+(* subset or (binary union) ***********************************************)
+
+theorem ces_sor_fw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sor_bw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
 
-(* subset or (binary union) *)
 definition sor: ∀D. Subset D → Subset D → Subset D ≝
-   λD,U1,U2,d. U1 d ∨ U2 d.
+   λD,U1,U2. 
+   mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
+
+(* subset less or equal (inclusion) ***************************************)
 
-(* subset less or equal (inclusion) *) 
 definition sle: ∀D. Subset D → Subset D → Prop ≝
-   λD,U1,U2. \iforall d. U1 d → U2 d. 
+   λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d. 
+
+(* subset overlap *********************************************************)
 
-(* subset overlap *) 
 definition sover: ∀D. Subset D → Subset D → Prop ≝
-   λD,U1,U2. \iexists d. U1 d ∧ U2 d. 
+   λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d. 
 
-(* the class of the subsets of a domain *)
-definition subsets_of_domain ≝
-   λD. mk_Class (Subset D) (true_f ?) (sle ?). 
+(* the class of the subsets of a domain ***********************************)
 
-(* the domain built upon a subset *)
-definition domain_of_subset: ∀D. Subset D → Domain ≝
-   λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)).
+definition power: Domain → Class ≝
+   λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).