miz3/Samples/lagrange1.ml

   1 needs "Library/prime.ml";;
   2
   3 parse_as_infix("**",(20,"right"));;
   4
   5 let group = new_definition
   6   `group(g,(**),i,(e:A)) <=>
   7     (e IN g) /\ (!x. x IN g ==> i(x) IN g) /\
   8     (!x y. x IN g /\ y IN g ==> x**y IN g) /\
   9     (!x y z. x IN g /\ y IN g /\ z IN g ==> x**(y**z) = (x**y)**z) /\
  10     (!x. x IN g ==> x**e = x /\ e**x = x) /\
  11     (!x. x IN g ==> x**i(x) = e /\ i(x)**x = e)`;;
  12
  13 let subgroup = new_definition
  14   `subgroup h (g,(**),i,(e:A)) <=> h SUBSET g /\ group(h,(**),i,e)`;;
  15
  16 (* ======== translation of John's proof ==================================== *)
  17
  18 horizon := 1;;
  19
  20 let GROUP_LAGRANGE_COSETS = thm `;
  21   !g h (**) i e.
  22        group(g,(**),i,e:A) /\ subgroup h (g,(**),i,e) /\ FINITE g
  23        ==> ?q. CARD g = CARD q * CARD h /\
  24                !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x
  25 proof exec REWRITE_TAC[group; subgroup; SUBSET];
  26   let g h be A->bool;
  27   let (**) be A->A->A;
  28   let i be A->A;
  29   let e be A;
  30   assume e IN g;
  31   assume !x. x IN g ==> i(x) IN g [1];
  32   assume !x y. x IN g /\ y IN g ==> x**y IN g [2];
  33   assume !x y z. x IN g /\ y IN g /\ z IN g
  34                  ==> x**(y**z) = (x**y)**z [3];
  35   assume !x. x IN g ==> x**e = x /\ e**x = x [4];
  36   assume !x. x IN g ==> x**i(x) = e /\ i(x)**x = e [5];
  37   assume !x. x IN h ==> x IN g [6];
  38   assume e IN h [7];
  39   assume !x. x IN h ==> i(x) IN h [8];
  40   assume !x y. x IN h /\ y IN h ==> x**y IN h [9];
  41   assume !x y z. x IN h /\ y IN h /\ z IN h
  42                  ==> x**(y**z) = (x**y)**z;
  43   assume !x. x IN h ==> x**e = x /\ e**x = x [10];
  44   assume !x. x IN h ==> x**i(x) = e /\ i(x)**x = e [11];
  45   assume FINITE g [12];
  46   set coset = \a. {b | b IN g /\ ?x. x IN h /\ b = a**x} [coset];
  47   !a. coset a = {b' | b' IN g /\ ?x. x IN h /\ b' = a**x} [13];
  48   !a. a IN g ==> a IN coset a [14]
  49   proof let a be A;
  50     assume a IN g [15];
  51     ?x. x IN h /\ a = a**x by 4,7;
  52   qed by SIMP_TAC,13,15,IN_ELIM_THM;
  53   FINITE h [16] by 6,12,FINITE_SUBSET,SUBSET;
  54   !a. FINITE (coset a)
  55   proof let a be A;
  56     ?t. FINITE t /\ coset a SUBSET t
  57     proof take g;
  58     qed by SIMP_TAC,12,13,IN_ELIM_THM,SUBSET;
  59   qed by MATCH_MP_TAC,FINITE_SUBSET;
  60   !a x y. a IN g /\ x IN g /\ y IN g /\ a**x = a**y ==> x = y [17]
  61   proof let a x y be A;
  62     assume a IN g /\ x IN g /\ y IN g /\ a**x = a**y [18];
  63     (i(a)**a)**x = (i(a)**a)**y by 1,3;
  64     e**x = e**y by 5,18;
  65   qed by 4,18;
  66   !a. a IN g ==> CARD (coset a) = CARD h
  67   proof let a be A;
  68     assume a IN g [19];
  69     coset a = IMAGE (\x. a**x) h [20]
  70     proof
  71       !x. x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
  72           ?x'. x = a**x' /\ x' IN h by 2,6;
  73     qed by REWRITE_TAC,13,EXTENSION,IN_IMAGE,IN_ELIM_THM;
  74     (!x y. x IN h /\ y IN h /\ a**x = a**y ==> x = y) /\ FINITE h
  75       by 6,16,17,19;
  76     CARD (IMAGE (\x. a**x) h) = CARD h by MATCH_MP_TAC,CARD_IMAGE_INJ;
  77   qed by 20;
  78   !x y. x IN g /\ y IN g ==> i(x**y) = i(y)**i(x) [21]
  79   proof let x y be A;
  80     assume x IN g /\ y IN g [22];
  81     ?a. a IN g /\ i(x**y) IN g /\ i(y)**i(x) IN g /\
  82         a**i(x**y) = a**i(y)**i(x)
  83     proof take x**y;
  84       e = x**(y**i(y))**i(x) by 1,4,5,22;
  85         .= ((x**y)**i(y))**i(x) by 1,2,3,22;
  86     qed by SIMP_TAC,1,2,3,5,22;
  87   qed by 17;
  88   !x. x IN g ==> i(i(x)) = x [23]
  89   proof let x be A;
  90     assume x IN g;
  91     ?a. a IN g /\ i(i(x)) IN g /\ x IN g /\ a**i(i(x)) = a**x
  92     proof take i(x);
  93     qed by 1,5;
  94   qed by MATCH_MP_TAC,17;
  95   !a b. a IN g /\ b IN g
  96         ==> coset a = coset b \/ coset a INTER coset b = {}
  97   proof let a b be A;
  98     assume a IN g /\ b IN g [24];
  99     cases;
 100     suppose i(b)**a IN h [25];
 101       now let x be A;
 102         !x. x IN h ==> b**(i(b)**a)**x = a**x /\ a**i(i(b)**a)**x = b**x
 103           by SIMP_TAC,1,3,4,5,6,21,23,24;
 104         thus x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
 105              x IN g /\ (?x'. x' IN h /\ x = b**x') by 8,9,25;
 106       end;
 107       coset a = coset b by REWRITE_TAC,13,EXTENSION,IN_ELIM_THM;
 108     qed;
 109     suppose ~(i(b)**a IN h) [26];
 110       now let x be A;
 111         assume x IN g /\ (?y. y IN h /\ x = a**y) /\ (?z. z IN h /\ x = b**z);
 112         consider y z such that y IN h /\ x = a**y /\ z IN h /\ x = b**z [27];
 113         (i(b)**a)**y = i(b)**a**y by 1,3,6,24,27;
 114           .= i(b)**b**z by 27;
 115           .= e**z by 1,3,5,6,24,27;
 116           .= z by 10,27;
 117         z**i(y) = ((i(b)**a)**y)**i(y);
 118           .= (i(b)**a)**y**i(y) by 1,2,3,5,6,24,27;
 119           .= (i(b)**a)**e by 11,27;
 120           .= i(b)**a by 1,2,4,24;
 121         thus F by 8,9,26,27;
 122       end;
 123       !x. ~((x IN g /\ ?y. y IN h /\ x = a**y) /\
 124             (x IN g /\ ?z. z IN h /\ x = b**z));
 125       coset a INTER coset b = {}
 126         by REWRITE_TAC,13,EXTENSION,NOT_IN_EMPTY,IN_INTER,IN_ELIM_THM;
 127     qed;
 128   end;
 129   set q = {c | ?a. a IN g /\ c = (@)(coset a)} [q] [28]; take q;
 130   !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x [29]
 131   proof let b be A;
 132     assume b IN g [30];
 133     set C = (@)(coset b) [C] [31]; take C;
 134     (@)(coset b) IN {c | ?a. a IN g /\ c = (@)(coset a)} by 30;
 135     thus C IN q by q,C;
 136     C IN coset b by 14,30,C,IN,SELECT_AX;
 137     C IN {b' | b' IN g /\ ?x. x IN h /\ b' = b**x} by 13;
 138     consider c such that
 139       C IN g /\ c IN h /\ C = b**c [32];
 140     take i(c);
 141     (b**c)**i(c) = b**c**i(c) by 1,3,6,30;
 142       .= b by 1,4,5,6,30,32;
 143   qed by 8,32;
 144   !a b. a IN g /\ b IN g /\ a IN coset b ==> b IN coset a [33]
 145   proof let a b be A;
 146     a IN g /\ b IN g /\ a IN g /\ (?x. x IN h /\ a = b**x)
 147     ==> b IN g /\ (?x. x IN h /\ b = a**x)
 148     proof
 149       assume a IN g /\ b IN g /\ a IN g /\ ?x. x IN h /\ a = b**x [34];
 150       thus b IN g;
 151       consider c such that c IN h /\ a = b**c by 34;
 152       take i(c);
 153     qed by 3,4,6,8,11,34;
 154   qed by REWRITE_TAC,13,IN_ELIM_THM;
 155   !a b c. a IN coset b /\ b IN coset c /\ c IN g ==> a IN coset c [35]
 156   proof let a b c be A;
 157     now assume (a IN g /\ ?x. x IN h /\ a = b**x) /\
 158                (b IN g /\ ?x. x IN h /\ b = c**x) /\ c IN g [36];
 159       consider x x' such that x IN h /\ a = b**x /\ x' IN h /\ b = c**x';
 160       thus a IN g /\ ?x. x IN h /\ a = c**x by 3,6,9,36;
 161     end;
 162   qed by REWRITE_TAC,13,IN_ELIM_THM;
 163   !a b. a IN coset b ==> a IN g [37]
 164   proof let a b be A;
 165     a IN g /\ (?x. x IN h /\ a = b**x) ==> a IN g;
 166   qed by REWRITE_TAC,13,IN_ELIM_THM;
 167   !a b. a IN coset b /\ b IN g ==> coset a = coset b [38]
 168     by 33,35,37,EXTENSION;
 169   !a. a IN g ==> (@)(coset a) IN coset a [39] by 14,IN,SELECT_AX;
 170   !a. a IN q ==> a IN g [40]
 171   proof let a be A; assume a IN q;
 172     a IN {c | ?a. a IN g /\ c = (@)(coset a)} by q;
 173     consider a' such that a' IN g /\ a = (@)(coset a');
 174   qed by 37,39;
 175   !a x a' x'. a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x
 176               ==> a' = a /\ x' = x [41]
 177   proof let a x a' x' be A;
 178     assume a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x [42];
 179     a IN {c | ?a. a IN g /\ c = (@)(coset a)} /\
 180     a' IN {c | ?a. a IN g /\ c = (@)(coset a)} by q;
 181     consider a1 a2 such that
 182       a1 IN g /\ a = (@)(coset a1) /\ a2 IN g /\ a' = (@)(coset a2) [43];
 183     a IN g /\ a' IN g [44] by 37,39;
 184     coset a = coset a1 /\ coset a' = coset a2 by 38,39,43;
 185     a = (@)(coset a) /\ a' = (@)(coset a') [45] by 43;
 186     ?x. x IN h /\ a' = a**x
 187     proof take x**i(x');
 188       thus x**i(x') IN h by 8,9,42;
 189       a' = a'**x'**i(x') by 4,5,6,42,44;
 190         .= (a**x)**i(x') by 1,2,3,6,42,44;
 191     qed by 1,2,3,6,42,44;
 192     a' IN coset a by REWRITE_TAC,13,44,IN_ELIM_THM;
 193     coset a = coset a' by 38,44;
 194   qed by 6,17,42,44,45;
 195   g = IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h}
 196   proof
 197     !x. x IN g <=> ?p1 p2. (x = p1**p2 /\ p1 IN q) /\ p2 IN h by 2,6,29,40;
 198   qed by REWRITE_TAC,EXTENSION,IN_IMAGE,IN_ELIM_THM,EXISTS_PAIR_THM,PAIR_EQ,
 199          CONJ_ASSOC,ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1;
 200   CARD g = CARD (IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h}) [46];
 201     .= CARD {(a,x) | a IN q /\ x IN h}
 202   proof
 203     !x y. x IN {(a,x) | a IN q /\ x IN h} /\
 204           y IN {(a,x) | a IN q /\ x IN h} /\
 205           (\(a,x). a**x) x = (\(a,x). a**x) y
 206           ==> x = y [47]
 207     proof
 208       !p1 p2 p1' p2'. (?a x. (a IN q /\ x IN h) /\ p1 = a /\ p2 = x) /\
 209                       (?a x. (a IN q /\ x IN h) /\ p1' = a /\ p2' = x) /\
 210                       p1**p2 = p1'**p2'
 211                       ==> p1 = p1' /\ p2 = p2' by 41;
 212     qed by REWRITE_TAC,FORALL_PAIR_THM,IN_ELIM_THM,PAIR_EQ;
 213     FINITE q /\ FINITE h by 6,12,40,FINITE_SUBSET,SUBSET;
 214     FINITE {(a,x) | a IN q /\ x IN h} by FINITE_PRODUCT;
 215   qed by MATCH_MP_TAC CARD_IMAGE_INJ,47;
 216     .= CARD q * CARD h by 6,12,40,46,CARD_PRODUCT,FINITE_SUBSET,SUBSET;
 217 qed by 29`;;
 218
 219 let GROUP_LAGRANGE = thm `;
 220   !g h (**) i e.
 221        group (g,( ** ),i,e:A) /\ subgroup h (g,(**),i,e) /\ FINITE g
 222        ==> CARD h divides CARD g
 223   by GROUP_LAGRANGE_COSETS,DIVIDES_LMUL,DIVIDES_REFL`;;
 224
 225 (* ======== and formal proof sketch derived from this translation ========== *)
 226
 227 horizon := -1;;
 228
 229 let GROUP_LAGRANGE_COSETS_SKETCH = ref None;;
 230
 231 GROUP_LAGRANGE_COSETS_SKETCH := Some `;
 232   !g h (**) i e.
 233        group(g,(**),i,e:A) /\ subgroup h (g,(**),i,e) /\ FINITE g
 234        ==> ?q. CARD g = CARD q * CARD h /\
 235                !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x
 236 proof exec REWRITE_TAC[group; subgroup; SUBSET];
 237   let g h be A->bool;
 238   let (**) be A->A->A;
 239   let i be A->A;
 240   let e be A;
 241   assume e IN g;
 242   assume !x. x IN g ==> i(x) IN g;
 243   assume !x y. x IN g /\ y IN g ==> x**y IN g;
 244   assume !x y z. x IN g /\ y IN g /\ z IN g
 245                  ==> x**(y**z) = (x**y)**z;
 246   assume !x. x IN g ==> x**e = x /\ e**x = x;
 247   assume !x. x IN g ==> x**i(x) = e /\ i(x)**x = e;
 248   assume !x. x IN h ==> x IN g;
 249   assume e IN h;
 250   assume !x. x IN h ==> i(x) IN h;
 251   assume !x y. x IN h /\ y IN h ==> x**y IN h;
 252   assume !x y z. x IN h /\ y IN h /\ z IN h
 253                  ==> x**(y**z) = (x**y)**z;
 254   assume !x. x IN h ==> x**e = x /\ e**x = x;
 255   assume !x. x IN h ==> x**i(x) = e /\ i(x)**x = e;
 256   assume FINITE g;
 257   set coset = \a. {b | b IN g /\ ?x. x IN h /\ b = a**x};
 258   !a. coset a = {b' | b' IN g /\ ?x. x IN h /\ b' = a**x};
 259   !a. a IN g ==> a IN coset a
 260   proof let a be A;
 261     assume a IN g;
 262     ?x. x IN h /\ a = a**x;
 263   qed;
 264   FINITE h;
 265 ::        #1
 266 :: 1: inference error
 267   !a. FINITE (coset a)
 268   proof let a be A;
 269     ?t. FINITE t /\ coset a SUBSET t
 270     proof take g;
 271     qed;
 272 ::     #2
 273 :: 2: inference time-out
 274   qed;
 275 ::   #2
 276   !a x y. a IN g /\ x IN g /\ y IN g /\ a**x = a**y ==> x = y
 277   proof let a x y be A;
 278     assume a IN g /\ x IN g /\ y IN g /\ a**x = a**y;
 279     (i(a)**a)**x = (i(a)**a)**y;
 280     e**x = e**y;
 281 ::             #2
 282   qed;
 283   !a. a IN g ==> CARD (coset a) = CARD h
 284   proof let a be A;
 285     assume a IN g;
 286     coset a = IMAGE (\x. a**x) h
 287     proof
 288       !x. x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
 289           ?x'. x = a**x' /\ x' IN h;
 290     qed;
 291 ::     #2
 292     (!x y. x IN h /\ y IN h /\ a**x = a**y ==> x = y) /\ FINITE h;
 293     CARD (IMAGE (\x. a**x) h) = CARD h;
 294 ::                                    #2
 295   qed;
 296   !x y. x IN g /\ y IN g ==> i(x**y) = i(y)**i(x)
 297   proof let x y be A;
 298     assume x IN g /\ y IN g;
 299     ?a. a IN g /\ i(x**y) IN g /\ i(y)**i(x) IN g /\
 300         a**i(x**y) = a**i(y)**i(x)
 301     proof take x**y;
 302       e = x**(y**i(y))**i(x);
 303 ::                          #2
 304         .= ((x**y)**i(y))**i(x);
 305 ::                             #2
 306     qed;
 307   qed;
 308   !x. x IN g ==> i(i(x)) = x
 309   proof let x be A;
 310     assume x IN g;
 311     ?a. a IN g /\ i(i(x)) IN g /\ x IN g /\ a**i(i(x)) = a**x
 312     proof take i(x);
 313     qed;
 314   qed;
 315   !a b. a IN g /\ b IN g
 316         ==> coset a = coset b \/ coset a INTER coset b = {}
 317   proof let a b be A;
 318     assume a IN g /\ b IN g;
 319     cases;
 320     suppose i(b)**a IN h;
 321       now let x be A;
 322         !x. x IN h ==> b**(i(b)**a)**x = a**x /\ a**i(i(b)**a)**x = b**x;
 323 ::                                                                      #2
 324         thus x IN g /\ (?x'. x' IN h /\ x = a**x') <=>
 325              x IN g /\ (?x'. x' IN h /\ x = b**x');
 326 ::                                                #2
 327       end;
 328       coset a = coset b;
 329 ::                     #2
 330     qed;
 331     suppose ~(i(b)**a IN h);
 332       now let x be A;
 333         assume x IN g /\ (?y. y IN h /\ x = a**y) /\ (?z. z IN h /\ x = b**z);
 334         consider y z such that y IN h /\ x = a**y /\ z IN h /\ x = b**z;
 335         (i(b)**a)**y = i(b)**a**y;
 336           .= i(b)**b**z;
 337           .= e**z;
 338 ::               #2
 339           .= z;
 340         z**i(y) = ((i(b)**a)**y)**i(y);
 341           .= (i(b)**a)**y**i(y);
 342 ::                             #2
 343           .= (i(b)**a)**e;
 344           .= i(b)**a;
 345 ::                  #2
 346         thus F;
 347 ::            #2
 348       end;
 349       !x. ~((x IN g /\ ?y. y IN h /\ x = a**y) /\
 350             (x IN g /\ ?z. z IN h /\ x = b**z));
 351       coset a INTER coset b = {};
 352 ::                              #2
 353     qed;
 354   end;
 355   set q = {c | ?a. a IN g /\ c = (@)(coset a)};
 356   take q;
 357   !b. b IN g ==> ?a x. a IN q /\ x IN h /\ b = a**x
 358   proof let b be A;
 359     assume b IN g;
 360     set C = (@)(coset b);
 361     take C;
 362     (@)(coset b) IN {c | ?a. a IN g /\ c = (@)(coset a)};
 363     thus C IN q;
 364     C IN coset b;
 365 ::              #2
 366     C IN {b' | b' IN g /\ ?x. x IN h /\ b' = b**x};
 367     consider c such that
 368       C IN g /\ c IN h /\ C = b**c;
 369     take i(c);
 370     (b**c)**i(c) = b**c**i(c);
 371       .= b;
 372   qed;
 373   !a b. a IN g /\ b IN g /\ a IN coset b ==> b IN coset a
 374   proof let a b be A;
 375     a IN g /\ b IN g /\ a IN g /\ (?x. x IN h /\ a = b**x)
 376     ==> b IN g /\ (?x. x IN h /\ b = a**x)
 377     proof
 378       assume a IN g /\ b IN g /\ a IN g /\ ?x. x IN h /\ a = b**x;
 379       thus b IN g;
 380       consider c such that c IN h /\ a = b**c;
 381       take i(c);
 382     qed;
 383 ::     #2
 384   qed;
 385   !a b c. a IN coset b /\ b IN coset c /\ c IN g ==> a IN coset c
 386   proof let a b c be A;
 387     now assume (a IN g /\ ?x. x IN h /\ a = b**x) /\
 388                (b IN g /\ ?x. x IN h /\ b = c**x) /\ c IN g;
 389       consider x x' such that x IN h /\ a = b**x /\ x' IN h /\ b = c**x';
 390       thus a IN g /\ ?x. x IN h /\ a = c**x;
 391 ::                                         #2
 392     end;
 393   qed;
 394 ::   #2
 395   !a b. a IN coset b ==> a IN g
 396   proof let a b be A;
 397     a IN g /\ (?x. x IN h /\ a = b**x) ==> a IN g;
 398   qed;
 399   !a b. a IN coset b /\ b IN g ==> coset a = coset b;
 400 ::                                                  #2
 401   !a. a IN g ==> (@)(coset a) IN coset a;
 402 ::                                      #2
 403   !a. a IN q ==> a IN g
 404   proof let a be A;
 405     assume a IN q;
 406     a IN {c | ?a. a IN g /\ c = (@)(coset a)};
 407     consider a' such that a' IN g /\ a = (@)(coset a');
 408   qed;
 409   !a x a' x'. a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x
 410               ==> a' = a /\ x' = x
 411   proof let a x a' x' be A;
 412     assume a IN q /\ a' IN q /\ x IN h /\ x' IN h /\ a'**x' = a**x;
 413     a IN {c | ?a. a IN g /\ c = (@)(coset a)} /\
 414     a' IN {c | ?a. a IN g /\ c = (@)(coset a)};
 415     consider a1 a2 such that
 416       a1 IN g /\ a = (@)(coset a1) /\ a2 IN g /\ a' = (@)(coset a2);
 417 ::                                                                 #2
 418     a IN g /\ a' IN g;
 419     coset a = coset a1 /\ coset a' = coset a2;
 420 ::                                           #2
 421     a = (@)(coset a) /\ a' = (@)(coset a');
 422     ?x. x IN h /\ a' = a**x
 423     proof take x**i(x');
 424       thus x**i(x') IN h;
 425 ::                      #2
 426       a' = a'**x'**i(x');
 427 ::                      #2
 428         .= (a**x)**i(x');
 429 ::                      #2
 430     qed;
 431 ::     #2
 432     a' IN coset a;
 433 ::               #2
 434     coset a = coset a';
 435   qed;
 436 ::   #2
 437   g = IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h}
 438   proof
 439     !x. x IN g <=> ?p1 p2. (x = p1**p2 /\ p1 IN q) /\ p2 IN h;
 440 ::                                                           #2
 441   qed;
 442 ::   #2
 443   CARD g = CARD (IMAGE (\(a,x). a**x) {(a,x) | a IN q /\ x IN h});
 444     .= CARD {(a,x) | a IN q /\ x IN h}
 445   proof
 446     !x y. x IN {(a,x) | a IN q /\ x IN h} /\
 447           y IN {(a,x) | a IN q /\ x IN h} /\
 448           (\(a,x). a**x) x = (\(a,x). a**x) y
 449           ==> x = y
 450     proof
 451       !p1 p2 p1' p2'. (?a x. (a IN q /\ x IN h) /\ p1 = a /\ p2 = x) /\
 452                       (?a x. (a IN q /\ x IN h) /\ p1' = a /\ p2' = x) /\
 453                       p1**p2 = p1'**p2'
 454                       ==> p1 = p1' /\ p2 = p2';
 455     qed;
 456 ::     #2
 457     FINITE q /\ FINITE h;
 458 ::                      #2
 459     FINITE {(a,x) | a IN q /\ x IN h};
 460 ::                                   #2
 461   qed;
 462 ::   #2
 463     .= CARD q * CARD h;
 464 ::                    #2
 465 qed`;;
 466