Moved the definition of s_u (as s) into the locale
authorpaulson
Thu Aug 13 18:07:38 1998 +0200 (1998-08-13)
changeset 5314c061e6f9d546
parent 5313 1861a564d7e2
child 5315 c9ad6bbf3a34
Moved the definition of s_u (as s) into the locale
src/ZF/AC/AC16_WO4.ML
src/ZF/AC/AC16_WO4.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.ML	Thu Aug 13 18:06:40 1998 +0200
     1.2 +++ b/src/ZF/AC/AC16_WO4.ML	Thu Aug 13 18:07:38 1998 +0200
     1.3 @@ -63,20 +63,20 @@
     1.4  qed "infinite_Un";
     1.5  
     1.6  (* ********************************************************************** *)
     1.7 -(* There is a v : s_u such that k lepoll x Int y (in our case succ(k))    *)
     1.8 +(* There is a v : s(u) such that k lepoll x Int y (in our case succ(k))    *)
     1.9  (* The idea of the proof is the following :                               *)
    1.10 -(* Suppose not, i.e. every element of s_u has exactly k-1 elements of y   *)
    1.11 +(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y   *)
    1.12  (* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k}      *)
    1.13  (*   We have obtained this result in two steps :                          *)
    1.14 -(*   1. y is less than or equipollent to {v:s_u. a <= v}                  *)
    1.15 +(*   1. y is less than or equipollent to {v:s(u). a <= v}                  *)
    1.16  (*      where a is certain k-2 element subset of y                        *)
    1.17 -(*   2. {v:s_u. a <= v} is less than or equipollent                       *)
    1.18 +(*   2. {v:s(u). a <= v} is less than or equipollent                       *)
    1.19  (*      to {v:Pow(x). v eqpoll n-k}                                       *)
    1.20  (* ********************************************************************** *)
    1.21  
    1.22  (*Proof simplified by LCP*)
    1.23  Goal "[| ~(EX x:A. f`x=y); f : inj(A, B); y:B |]  \
    1.24 -\       ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
    1.25 +\     ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
    1.26  by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
    1.27  by (ALLGOALS
    1.28      (asm_simp_tac 
    1.29 @@ -89,14 +89,6 @@
    1.30  by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1);
    1.31  qed "succ_not_lepoll_imp_eqpoll";
    1.32  
    1.33 -val [prem] = Goalw [s_u_def]
    1.34 -        "(ALL v:s_u(u, t_n, k, y). k eqpoll v Int y ==> False)  \
    1.35 -\       ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
    1.36 -by (rtac ccontr 1);
    1.37 -by (resolve_tac [prem RS FalseE] 1);
    1.38 -by (fast_tac (claset() addSEs [succ_not_lepoll_imp_eqpoll]) 1);
    1.39 -qed "suppose_not";
    1.40 -
    1.41  
    1.42  (* ********************************************************************** *)
    1.43  (* There is a k-2 element subset of y                                     *)
    1.44 @@ -127,21 +119,6 @@
    1.45  by (fast_tac (claset() addSIs [cons_eqpoll_succ]) 1);
    1.46  qed "cons_cons_eqpoll";
    1.47  
    1.48 -Goalw [s_u_def] "s_u(u, t_n, k, y) <= t_n";
    1.49 -by (Fast_tac 1);
    1.50 -qed "s_u_subset";
    1.51 -
    1.52 -Goalw [s_u_def, succ_def]
    1.53 -      "[| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; k eqpoll a  \
    1.54 -\      |] ==> w: s_u(u, t_n, succ(k), y)";
    1.55 -by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong]
    1.56 -                addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
    1.57 -qed "s_uI";
    1.58 -
    1.59 -Goalw [s_u_def] "v : s_u(u, t_n, k, y) ==> u : v";
    1.60 -by (Fast_tac 1);
    1.61 -qed "in_s_u_imp_u_in";
    1.62 -
    1.63  Goal "[| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat  \
    1.64  \       |] ==> A = cons(a, B)";
    1.65  by (rtac equalityI 1);
    1.66 @@ -256,8 +233,7 @@
    1.67  val disjoint = thm "disjoint";
    1.68  val includes = thm "includes";
    1.69  val WO_R = thm "WO_R";
    1.70 -val knat = thm "knat";
    1.71 -val kpos = thm "kpos";
    1.72 +val k_def = thm "k_def";
    1.73  val lnat = thm "lnat";
    1.74  val mnat = thm "mnat";
    1.75  val mpos = thm "mpos";
    1.76 @@ -267,10 +243,15 @@
    1.77  val LL_def = thm "LL_def";
    1.78  val MM_def = thm "MM_def";
    1.79  val GG_def = thm "GG_def";
    1.80 +val s_def = thm "s_def";
    1.81  
    1.82 -Addsimps [disjoint, WO_R, knat, lnat, mnat, mpos, Infinite];
    1.83 +Addsimps [disjoint, WO_R, lnat, mnat, mpos, Infinite];
    1.84 +AddSIs [disjoint, WO_R, lnat, mnat, mpos];
    1.85  
    1.86 -AddSIs [disjoint, WO_R, knat, lnat, mnat, mpos];
    1.87 +Goalw [k_def] "k: nat";
    1.88 +by Auto_tac;
    1.89 +qed "knat";
    1.90 +Addsimps [knat];  AddSIs [knat];
    1.91  
    1.92  AddSIs [Infinite];   (*if notI is removed!*)
    1.93  AddSEs [Infinite RS notE];
    1.94 @@ -278,11 +259,11 @@
    1.95  AddEs [IntI RS (disjoint RS equals0E)];
    1.96  
    1.97  (*use k = succ(l) *)
    1.98 -val includes_l = simplify (FOL_ss addsimps [kpos]) includes;
    1.99 -val all_ex_l = simplify (FOL_ss addsimps [kpos]) all_ex;
   1.100 +val includes_l = simplify (FOL_ss addsimps [k_def]) includes;
   1.101 +val all_ex_l = simplify (FOL_ss addsimps [k_def]) all_ex;
   1.102  
   1.103  (* ********************************************************************** *)
   1.104 -(*   1. y is less than or equipollent to {v:s_u. a <= v}                  *)
   1.105 +(*   1. y is less than or equipollent to {v:s(u). a <= v}                  *)
   1.106  (*      where a is certain k-2 element subset of y                        *)
   1.107  (* ********************************************************************** *)
   1.108  
   1.109 @@ -300,38 +281,54 @@
   1.110                  RS lepoll_infinite]) 1);
   1.111  qed "Diff_Finite_eqpoll";
   1.112  
   1.113 +Goalw [s_def] "s(u) <= t_n";
   1.114 +by (Fast_tac 1);
   1.115 +qed "s_subset";
   1.116 +
   1.117 +Goalw [s_def, succ_def, k_def]
   1.118 +      "[| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; l eqpoll a  \
   1.119 +\      |] ==> w: s(u)";
   1.120 +by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong]
   1.121 +                addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1);
   1.122 +qed "sI";
   1.123 +
   1.124 +Goalw [s_def] "v : s(u) ==> u : v";
   1.125 +by (Fast_tac 1);
   1.126 +qed "in_s_imp_u_in";
   1.127 +
   1.128 +
   1.129  Goal "[| l eqpoll a;  a <= y;  b : y - a;  u : x |]  \
   1.130 -\     ==> EX! c. c: s_u(u, t_n, succ(l), y) & a <= c & b:c";
   1.131 +\     ==> EX! c. c: s(u) & a <= c & b:c";
   1.132  by (rtac (all_ex_l RS ballE) 1);
   1.133  by (blast_tac (claset() delrules [PowI]
   1.134  		        addSIs [cons_cons_subset,
   1.135  				eqpoll_sym RS cons_cons_eqpoll]) 2);
   1.136  by (etac ex1E 1);
   1.137  by (res_inst_tac [("a","w")] ex1I 1);
   1.138 -by (blast_tac (claset() addIs [s_uI]) 1);
   1.139 +by (blast_tac (claset() addIs [sI]) 1);
   1.140  by (etac allE 1);
   1.141  by (etac impE 1);
   1.142  by (assume_tac 2);
   1.143 -by (fast_tac (claset() addSEs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1);
   1.144 +by (fast_tac (claset() addSEs [s_subset RS subsetD, in_s_imp_u_in]) 1);
   1.145  qed "ex1_superset_a";
   1.146  
   1.147 -Goal "[| ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y;  \
   1.148 +Goal "[| ALL v:s(u). succ(l) eqpoll v Int y;  \
   1.149  \        l eqpoll a;  a <= y;  b : y - a;  u : x |]   \
   1.150 -\     ==> (THE c. c: s_u(u, t_n, succ(l), y) & a <= c & b:c)  \
   1.151 +\     ==> (THE c. c: s(u) & a <= c & b:c)  \
   1.152  \              Int y = cons(b, a)";
   1.153  by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1));
   1.154  by (rtac set_eq_cons 1);
   1.155  by (REPEAT (Fast_tac 1));
   1.156  qed "the_eq_cons";
   1.157  
   1.158 -Goal "[| ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y;  \
   1.159 +Goal "[| ALL v:s(u). succ(l) eqpoll v Int y;  \
   1.160  \        l eqpoll a;  a <= y;  u:x |]  \
   1.161 -\     ==> y lepoll {v:s_u(u, t_n, succ(l), y). a <= v}";
   1.162 +\     ==> y lepoll {v:s(u). a <= v}";
   1.163  by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS 
   1.164  		 eqpoll_imp_lepoll RS lepoll_trans] 1
   1.165      THEN REPEAT (Fast_tac 1));
   1.166  by (res_inst_tac 
   1.167 -     [("f3", "lam b:y-a. THE c. c: s_u(u, t_n, succ(l), y) & a <= c & b:c")]
   1.168 +     [("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")]
   1.169       (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
   1.170  by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
   1.171  by (rtac CollectI 1);
   1.172 @@ -344,7 +341,7 @@
   1.173  by (Fast_tac 2);
   1.174  by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1);
   1.175  by (asm_full_simp_tac (simpset() addsimps [the_eq_cons]) 1);
   1.176 -qed "y_lepoll_subset_s_u";
   1.177 +qed "y_lepoll_subset_s";
   1.178  
   1.179  
   1.180  (* ********************************************************************** *)
   1.181 @@ -355,23 +352,22 @@
   1.182  by (Fast_tac 1);
   1.183  qed "w_Int_eq_w_Diff";
   1.184  
   1.185 -Goal "[| w:{v:s_u(u, t_n, succ(l), y). a <= v};  \
   1.186 +Goal "[| w:{v:s(u). a <= v};  \
   1.187  \        l eqpoll a;  u : x;  \
   1.188 -\        ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y  \
   1.189 +\        ALL v:s(u). succ(l) eqpoll v Int y  \
   1.190  \     |] ==> w Int (x - {u}) eqpoll m";
   1.191  by (etac CollectE 1);
   1.192  by (stac w_Int_eq_w_Diff 1);
   1.193 -by (fast_tac (claset() addSDs [s_u_subset RS subsetD,
   1.194 +by (fast_tac (claset() addSDs [s_subset RS subsetD,
   1.195  			       includes_l RS subsetD]) 1);
   1.196  by (fast_tac (claset() addSDs [bspec]
   1.197 -        addDs [s_u_subset RS subsetD,
   1.198 -	       includes_l RS subsetD]
   1.199 -        addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_u_imp_u_in]
   1.200 +        addDs [s_subset RS subsetD, includes_l RS subsetD]
   1.201 +        addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_imp_u_in]
   1.202          addSIs [eqpoll_sum_imp_Diff_eqpoll]) 1);
   1.203  qed "w_Int_eqpoll_m";
   1.204  
   1.205  (* ********************************************************************** *)
   1.206 -(*   2. {v:s_u. a <= v} is less than or equipollent                       *)
   1.207 +(*   2. {v:s(u). a <= v} is less than or equipollent                       *)
   1.208  (*      to {v:Pow(x). v eqpoll n-k}                                       *)
   1.209  (* ********************************************************************** *)
   1.210  
   1.211 @@ -383,16 +379,15 @@
   1.212  
   1.213  Goal "[| z : xa Int (x - {u}); l eqpoll a; a <= y; u:x |]  \
   1.214  \     ==> EX! w. w : t_n & cons(z, cons(u, a)) <= w";
   1.215 -by (cut_facts_tac [kpos] 1);
   1.216 -br (all_ex RS bspec) 1;
   1.217 +by (rtac (all_ex RS bspec) 1);
   1.218 +by (rewtac k_def);
   1.219  by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [eqpoll_sym]) 1);
   1.220  qed "cons_cons_in";
   1.221  
   1.222 -Goal "[| ALL v:s_u(u, t_n, succ(l), y). succ(l) eqpoll v Int y;  \
   1.223 +Goal "[| ALL v:s(u). succ(l) eqpoll v Int y;  \
   1.224  \        a <= y; l eqpoll a; u : x |]  \
   1.225 -\     ==> {v:s_u(u, t_n, succ(l), y). a <= v} lepoll {v:Pow(x). v eqpoll m}";
   1.226 -by (res_inst_tac [("f3","lam w:{v:s_u(u, t_n, succ(l), y). a <= v}.  \
   1.227 -\       w Int (x - {u})")] 
   1.228 +\     ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}";
   1.229 +by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")] 
   1.230          (exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
   1.231  by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
   1.232  by (rtac CollectI 1);
   1.233 @@ -409,8 +404,8 @@
   1.234  by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
   1.235  by (etac ex1_two_eq 1);
   1.236  by (REPEAT (blast_tac
   1.237 -	    (claset() addDs [s_u_subset RS subsetD, in_s_u_imp_u_in]) 1));
   1.238 -qed "subset_s_u_lepoll_w";
   1.239 +	    (claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1));
   1.240 +qed "subset_s_lepoll_w";
   1.241  
   1.242  
   1.243  (* ********************************************************************** *)
   1.244 @@ -445,8 +440,8 @@
   1.245  qed "LL_subset";
   1.246  
   1.247  Goal "EX S. well_ord(LL,S)";
   1.248 -br (well_ord_subsets_lepoll_n RS exE) 1;
   1.249 -by (blast_tac (claset() addIs [LL_subset RSN (2,  well_ord_subset)]) 2);
   1.250 +by (rtac (well_ord_subsets_lepoll_n RS exE) 1);
   1.251 +by (blast_tac (claset() addIs [LL_subset RSN (2, well_ord_subset)]) 2);
   1.252  by Auto_tac;
   1.253  qed "well_ord_LL";
   1.254  
   1.255 @@ -487,8 +482,8 @@
   1.256  qed "in_LL_eq_Int";
   1.257  
   1.258  Goal "v : LL ==> (THE x. x : MM & v <= x) <= x Un y";
   1.259 -bd unique_superset1 1;
   1.260 -bw MM_def;
   1.261 +by (dtac unique_superset1 1);
   1.262 +by (rewtac MM_def);
   1.263  by (fast_tac (claset() addSDs [unique_superset1, includes RS subsetD]) 1);
   1.264  qed "the_in_MM_subset";
   1.265  
   1.266 @@ -503,7 +498,7 @@
   1.267  by (etac nat_lepoll_imp_ex_eqpoll_n 1);
   1.268  by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
   1.269          RSN (2, lepoll_trans)] 1);
   1.270 -br WO_R 2;
   1.271 +by (rtac WO_R 2);
   1.272  by (fast_tac 
   1.273      (claset() delrules [notI]
   1.274                addSIs [nat_le_infinite_Ord RS le_imp_lepoll]
   1.275 @@ -513,25 +508,28 @@
   1.276  qed "ex_subset_eqpoll_n";
   1.277  
   1.278  
   1.279 -Goal "u:x ==> EX v : s_u(u, t_n, k, y). succ(k) lepoll v Int y";
   1.280 -by (rtac suppose_not 1);
   1.281 -by (cut_facts_tac [all_ex, includes, kpos, lnat] 1);
   1.282 -by (hyp_subst_tac 1);
   1.283 +Goal "u:x ==> EX v : s(u). succ(k) lepoll v Int y";
   1.284 +by (rtac ccontr 1);
   1.285 +by (subgoal_tac "ALL v:s(u). k eqpoll v Int y" 1);
   1.286 +by (full_simp_tac (simpset() addsimps [s_def]) 2);
   1.287 +by (blast_tac (claset() addIs [succ_not_lepoll_imp_eqpoll]) 2);
   1.288 +by (rewtac k_def);
   1.289 +by (cut_facts_tac [all_ex, includes, lnat] 1);
   1.290  by (rtac (ex_subset_eqpoll_n RS exE) 1 THEN assume_tac 1);
   1.291 -br (noLepoll RS notE) 1;
   1.292 +by (rtac (noLepoll RS notE) 1);
   1.293  by (blast_tac (claset() addIs
   1.294 -	   [[y_lepoll_subset_s_u, subset_s_u_lepoll_w] MRS lepoll_trans]) 1);
   1.295 -qed "exists_proper_in_s_u";
   1.296 +	   [[y_lepoll_subset_s, subset_s_lepoll_w] MRS lepoll_trans]) 1);
   1.297 +qed "exists_proper_in_s";
   1.298  
   1.299  Goal "u:x ==> EX w:MM. u:w";
   1.300 -by (eresolve_tac [exists_proper_in_s_u RS bexE] 1);
   1.301 -by (rewrite_goals_tac [MM_def, s_u_def]);
   1.302 +by (eresolve_tac [exists_proper_in_s RS bexE] 1);
   1.303 +by (rewrite_goals_tac [MM_def, s_def]);
   1.304  by (Fast_tac 1);
   1.305  qed "exists_in_MM";
   1.306  
   1.307  Goal "u:x ==> EX w:LL. u:GG`w";
   1.308  by (rtac (exists_in_MM RS bexE) 1);
   1.309 -ba 1;
   1.310 +by (assume_tac 1);
   1.311  by (rtac bexI 1);
   1.312  by (etac Int_in_LL 2);
   1.313  by (rewtac GG_def);
   1.314 @@ -547,7 +545,7 @@
   1.315  by (rtac subsetI 1);
   1.316  by (etac OUN_E 1);
   1.317  by (resolve_tac [GG_subset RS subsetD] 1);
   1.318 -ba 2;
   1.319 +by (assume_tac 2);
   1.320  by (blast_tac (claset() addIs [ordermap_bij RS bij_converse_bij RS
   1.321  			       bij_is_fun RS apply_type, ltD]) 1);
   1.322  by (rtac subsetI 1);
   1.323 @@ -601,8 +599,8 @@
   1.324      exI 1);
   1.325  by (Simp_tac 1);
   1.326  by (REPEAT (ares_tac [conjI, lam_funtype RS domain_of_fun,
   1.327 -			   Ord_ordertype, 
   1.328 -			   all_in_lepoll_m, OUN_eq_x] 1));
   1.329 +		      Ord_ordertype, 
   1.330 +		      all_in_lepoll_m, OUN_eq_x] 1));
   1.331  qed "conclusion";
   1.332  
   1.333  Close_locale ();
   1.334 @@ -622,7 +620,7 @@
   1.335  by (REPEAT (eresolve_tac [exE, conjE] 1));
   1.336  by (eres_inst_tac [("x","A Un y")] allE 1);
   1.337  by (forward_tac [infinite_Un] 1 THEN (mp_tac 1));
   1.338 +by (etac zero_lt_natE 1); by (assume_tac 1);
   1.339  by (Clarify_tac 1);
   1.340 -be zero_lt_natE 1;
   1.341  by (DEPTH_SOLVE (ares_tac [export conclusion] 1));
   1.342  qed "AC16_WO4";
     2.1 --- a/src/ZF/AC/AC16_WO4.thy	Thu Aug 13 18:06:40 1998 +0200
     2.2 +++ b/src/ZF/AC/AC16_WO4.thy	Thu Aug 13 18:07:38 1998 +0200
     2.3 @@ -2,23 +2,11 @@
     2.4      ID:         $Id$
     2.5      Author:     Krzysztof Grabczewski
     2.6  
     2.7 -
     2.8 -(*for all_in_lepoll_m and OUN_eq_x*)
     2.9 +Tidied using locales by LCP
    2.10  *)
    2.11  
    2.12  AC16_WO4 = OrderType + AC16_lemmas + Cardinal_aux +
    2.13  
    2.14 -consts
    2.15 -
    2.16 -  s_u :: [i, i, i, i] => i
    2.17 -  
    2.18 -defs
    2.19 -
    2.20 -  s_u_def "s_u(u, t_n, k, y) == {v:t_n. u:v & k lepoll v Int y}"
    2.21 -
    2.22 -
    2.23 -
    2.24 -
    2.25  locale AC16 =
    2.26    fixes 
    2.27      x	:: i
    2.28 @@ -31,22 +19,23 @@
    2.29      MM  :: i
    2.30      LL  :: i
    2.31      GG  :: i
    2.32 +    s   :: i=>i
    2.33    assumes
    2.34      all_ex    "ALL z:{z: Pow(x Un y) . z eqpoll succ(k)}.
    2.35  	         EX! w. w:t_n & z <= w "
    2.36      disjoint  "x Int y = 0"
    2.37      includes  "t_n <= {v:Pow(x Un y). v eqpoll succ(k #+ m)}"
    2.38      WO_R      "well_ord(y,R)"
    2.39 -    knat      "k:nat"
    2.40 -    kpos      "k = succ(l)"
    2.41      lnat      "l:nat"
    2.42      mnat      "m:nat"
    2.43      mpos      "0<m"
    2.44      Infinite  "~ Finite(y)"
    2.45      noLepoll  "~ y lepoll {v:Pow(x). v eqpoll m}"
    2.46    defines
    2.47 -    MM_def    "MM == {v:t_n. succ(k) lepoll v Int y}"
    2.48 -    LL_def    "LL == {v Int y. v:MM}"
    2.49 -    GG_def    "GG == lam v:LL. (THE w. w:MM & v <= w) - v"
    2.50 +    k_def     "k   == succ(l)"
    2.51 +    MM_def    "MM  == {v:t_n. succ(k) lepoll v Int y}"
    2.52 +    LL_def    "LL  == {v Int y. v:MM}"
    2.53 +    GG_def    "GG  == lam v:LL. (THE w. w:MM & v <= w) - v"
    2.54 +    s_def     "s(u) == {v:t_n. u:v & k lepoll v Int y}"
    2.55  
    2.56  end