helm/software/matita/nlibrary/re/re.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (*include "logic/connectives.ma".*)
  16 (*include "logic/equality.ma".*)
  17 include "datatypes/list.ma".
  18 include "datatypes/pairs.ma".
  19
  20 (*include "Plogic/equality.ma".*)
  21
  22 ndefinition word ≝ λS:Type[0].list S.
  23
  24 ninductive re (S: Type[0]) : Type[0] ≝
  25    z: re S
  26  | e: re S
  27  | s: S → re S
  28  | c: re S → re S → re S
  29  | o: re S → re S → re S
  30  | k: re S → re S.
  31
  32 (*
  33 alias symbol "not" (instance 1) = "Clogical not".
  34 nlemma foo1: ∀S. ¬ (z S = e S). #S; @; #H; ndestruct. nqed.
  35 nlemma foo2: ∀S,x. ¬ (z S = s S x). #S; #x; @; #H; ndestruct. nqed.
  36 nlemma foo3: ∀S,x1,x2. ¬ (z S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
  37 nlemma foo4: ∀S,x1,x2. ¬ (z S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
  38 nlemma foo5: ∀S,x. ¬ (z S = k S x). #S; #x; @; #H; ndestruct. nqed.
  39 nlemma foo6: ∀S,x. ¬ (e S = s S x). #S; #x; @; #H; ndestruct. nqed.
  40 nlemma foo7: ∀S,x1,x2. ¬ (e S = c S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
  41 nlemma foo8: ∀S,x1,x2. ¬ (e S = o S x1 x2). #S; #x1; #x2; @; #H; ndestruct. nqed.
  42 nlemma foo9: ∀S,x. ¬ (e S = k S x). #S; #x; @; #H; ndestruct. nqed.
  43 *)
  44
  45 ninductive in_l (S: Type[0]): word S → re S → Prop ≝
  46    in_e: in_l S [] (e ?)
  47  | in_s: ∀x. in_l S [x] (s ? x)
  48  | in_c: ∀w1,w2,e1,e2. in_l ? w1 e1 → in_l ? w2 e2 → in_l S (w1@w2) (c ? e1 e2)
  49  | in_o1: ∀w,e1,e2. in_l ? w e1 → in_l S w (o ? e1 e2)
  50  | in_o2: ∀w,e1,e2. in_l ? w e2 → in_l S w (o ? e1 e2)
  51  | in_ke: ∀e. in_l S [] (k ? e)
  52  | in_ki: ∀w1,w2,e. in_l ? w1 e → in_l ? w2 (k ? e) → in_l S (w1@w2) (k ? e).
  53
  54 naxiom in_l_inv_z:
  55  ∀S,w. ¬ (in_l S w (z ?)).
  56 (* #S; #w; #H; ninversion H
  57   [ #_; #b; ndestruct
  58   | #a; #b; #c; ndestruct
  59   | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
  60   | #a; #b; #c; #d; #e; #f; #g; ndestruct
  61   | #a; #b; #c; #d; #e; #f; #g; ndestruct
  62   | #a; #b; #c; ndestruct
  63   | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
  64 nqed. *)
  65
  66 nlemma in_l_inv_e:
  67  ∀S,w. in_l S w (e ?) → w = [].
  68  #S; #w; #H; ninversion H
  69   [ #a; #b; ndestruct; //
  70   | #a; #b; #c; ndestruct
  71   | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
  72   | #a; #b; #c; #d; #e; #f; #g; ndestruct
  73   | #a; #b; #c; #d; #e; #f; #g; ndestruct
  74   | #a; #b; #c; ndestruct
  75   | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]
  76 nqed.
  77
  78 naxiom in_l_inv_s:
  79  ∀S,w,x. in_l S w (s ? x) → w = [x].
  80
  81 naxiom in_l_inv_c:
  82  ∀S,w,E1,E2. in_l S w (c S E1 E2) → ∃w1.∃w2. w = w1@w2 ∧ in_l S w1 E1 ∧ in_l S w2 E2.
  83
  84 ninductive pre (S: Type[0]) : Type[0] ≝
  85    pz: pre S
  86  | pe: pre S
  87  | ps: S → pre S
  88  | pp: S → pre S
  89  | pc: pre S → pre S → pre S
  90  | po: pre S → pre S → pre S
  91  | pk: pre S → pre S.
  92
  93 nlet rec forget (S: Type[0]) (l : pre S) on l: re S ≝
  94  match l with
  95   [ pz ⇒ z S
  96   | pe ⇒ e S
  97   | ps x ⇒ s S x
  98   | pp x ⇒ s S x
  99   | pc E1 E2 ⇒ c S (forget ? E1) (forget ? E2)
 100   | po E1 E2 ⇒ o S (forget ? E1) (forget ? E2)
 101   | pk E ⇒ k S (forget ? E) ].
 102
 103 ninductive in_pl (S: Type[0]): word S → pre S → Prop ≝
 104    in_pp: ∀x. in_pl S [x] (pp S x)
 105  | in_pc1: ∀w1,w2,e1,e2. in_pl ? w1 e1 → in_l ? w2 (forget ? e2) →
 106             in_pl S (w1@w2) (pc ? e1 e2)
 107  | in_pc2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (pc ? e1 e2)
 108  | in_po1: ∀w,e1,e2. in_pl ? w e1 → in_pl S w (po ? e1 e2)
 109  | in_po2: ∀w,e1,e2. in_pl ? w e2 → in_pl S w (po ? e1 e2)
 110  | in_pki: ∀w1,w2,e. in_pl ? w1 e → in_l ? w2 (k ? (forget ? e)) →
 111            in_pl S (w1@w2) (pk ? e).
 112
 113 nlet rec eclose (S: Type[0]) (E: pre S) on E ≝
 114  match E with
 115   [ pz ⇒ 〈 false, pz ? 〉
 116   | pe ⇒ 〈 true, pe ? 〉
 117   | ps x ⇒ 〈 false, pp ? x 〉
 118   | pp x ⇒ 〈 false, pp ? x 〉
 119   | pc E1 E2 ⇒
 120      let E1' ≝ eclose ? E1 in
 121      let E1'' ≝ snd … E1' in
 122       match fst … E1' with
 123        [ true =>
 124           let E2' ≝ eclose ? E2 in
 125            〈 fst … E2', pc ? E1'' (snd … E2') 〉
 126        | false ⇒ 〈 false, pc ? E1'' E2 〉 ]
 127   | po E1 E2 ⇒
 128      let E1' ≝ eclose ? E1 in
 129      let E2' ≝ eclose ? E2 in
 130       〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
 131   | pk E ⇒ 〈 true, pk ? (snd … (eclose S E)) 〉 ].
 132
 133 ntheorem forget_eclose:
 134  ∀S,E. forget S (snd … (eclose … E)) = forget ? E.
 135  #S; #E; nelim E; nnormalize; //;
 136  #p; ncases (fst … (eclose S p)); nnormalize; //.
 137 nqed.
 138
 139 ntheorem eclose_true:
 140  ∀S,E. (* bug refiner se si scambia true con il termine *)
 141   true = fst bool (pre S) (eclose S E) → in_l S [] (forget S E).
 142  #S; #E; nelim E; nnormalize; //
 143   [ #H; ncases (?: False); /2/
 144   | #x; #H; ncases (?: False); /2/
 145   | #x; #H; ncases (?: False); /2/
 146   | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/;
 147     #_; #_; #H; ncases (?:False); /2/
 148   | #w1; #w2; ncases (fst … (eclose S w1)); nnormalize; /3/]
 149 nqed.
 150
 151 (* to be moved *)
 152 nlemma eq_append_nil_to_eq_nil1:
 153  ∀A.∀l1,l2:list A. l1 @ l2 = [] → l1 = [].
 154  #A; #l1; nelim l1; nnormalize; /2/;
 155  #x; #tl; #_; #l3; #K; ndestruct.
 156 nqed.
 157
 158 (* to be moved *)
 159 nlemma eq_append_nil_to_eq_nil2:
 160  ∀A.∀l1,l2:list A. l1 @ l2 = [] → l2 = [].
 161  #A; #l1; nelim l1; nnormalize; /2/;
 162  #x; #tl; #_; #l3; #K; ndestruct.
 163 nqed.
 164
 165 ntheorem in_l_empty_c:
 166  ∀S,E1,E2. in_l S [] (c … E1 E2) → in_l S [] E2.
 167  #S; #E1; #E2; #H; ninversion H
 168   [ #_; #H2; ndestruct
 169   | #x; #K; ndestruct
 170   | #w1; #w2; #E1'; #E2'; #H1; #H2; #H3; #H4; #H5; #H6;
 171     nrewrite < H5; nlapply (eq_append_nil_to_eq_nil2 … w1 w2 ?); //;
 172     ndestruct; //
 173   | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
 174   | #w; #E1'; #E2'; #H1; #H2; #H3; #H4; ndestruct
 175   | #E; #_; #K; ndestruct
 176   | #w1; #w2; #w3; #H1; #H2; #H3; #H4; #H5; #H6; ndestruct ]
 177 nqed.
 178
 179 ntheorem eclose_true':
 180  ∀S,E. (* bug refiner se si scambia true con il termine *)
 181   in_l S [] (forget S E) → true = fst bool (pre S) (eclose S E).
 182  #S; #E; nelim E; nnormalize; //
 183   [ #H; ncases (?:False); /2/
 184   |##2,3: #x; #H; ncases (?:False); nlapply (in_l_inv_s ??? H); #K; ndestruct
 185   | #E1; #E2; ncases (fst … (eclose S E1)); nnormalize
 186      [ #H1; #H2; #H3; ninversion H3; /3/;
 187    ##| #H1; #H2; #H3; ninversion H3
 188         [ #_; #K; ndestruct
 189         | #x; #K; ndestruct
 190         | #w1; #w2; #E1'; #E2'; #H4; #H5; #K1; #K2; #K3; #K4; ndestruct;
 191           napply H1; nrewrite < (eq_append_nil_to_eq_nil1 … w1 w2 ?); //
 192         | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
 193         | #w1; #E1'; #E2'; #H4; #H5; #H6; #H7; ndestruct
 194         | #E'; #_; #K; ndestruct
 195         | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct ]##]
 196 ##| #E1; ncases (fst … (eclose S E1)); nnormalize; //;
 197     #E2; #H1; #H2; #H3; ninversion H3
 198      [ #_; #K; ndestruct
 199      | #w; #_; #K; ndestruct
 200      | #a; #b; #c; #d; #e; #f; #g; #h; #i; #l; ndestruct
 201      | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct;
 202        ncases (?: False); napply (absurd ?? (not_eq_true_false …));
 203        /2/
 204      | #w; #E1'; #E2'; #H1'; #H2'; #H3'; #H4; ndestruct; /2/
 205      | #a; #b; #c; ndestruct
 206      | #a; #b; #c; #d; #e; #f; #g; #h; #i; ndestruct]##]
 207 nqed.
 208
 209 (*
 210 ntheorem eclose_superset:
 211  ∀S,E.
 212   ∀w. in_l S w (forget … E) ∨ in_pl ? w E →
 213        let E' ≝ eclose … E in
 214        in_pl ? w (snd … E') ∨ fst … E' = true ∧ w = [].
 215  #S; #E; #w; *
 216   [ ngeneralize in match w; nelim E; nnormalize
 217      [ #w'; #H; ncases (? : False); /2/
 218    ##| #w'; #H; @2; @; //; napply in_l_inv_e; //; (* auto non va *)
 219    ##|##3,4: #x; #w'; #H; @1; nrewrite > (in_l_inv_s … H); //;
 220    ##| #E1; #E2; #H1; #H2; #w'; #H3;
 221        ncases (in_l_inv_c … H3); #w1; *; #w2; *; *; #H4; #H5; #H6;
 222        ncases (fst … (eclose S E1)) in H1 H2 ⊢ %; nnormalize
 223         [ #H1; #H2; ncases (H1 … H5); ncases (H2 … H6)
 224           [ #K1; #K2; nrewrite > H4; /3/;
 225         ##| *; #_; #K1; #K2; nrewrite > H4; /3/;
 226         ##| #K1; *; #_; #K2; nrewrite > H4; @1; nrewrite > K2;
 227             /3/ ]
 228
 229     @2; @; //; ninversion H; //;
 230 ##| #H; nwhd; @1; (* manca intro per letin*)
 231     (* LEMMA A PARTE? *) (* manca clear E' *)
 232     nelim H; nnormalize; /2/
 233      [ #w1; #w2; #p; ncases (fst … (eclose S p));
 234        nnormalize; /2/
 235      | #w; #p; ncases (fst … (eclose S p));
 236        nnormalize; /2/ ]
 237 nqed.
 238 *)
 239
 240 nrecord decidable : Type[1] ≝
 241  { carr :> Type[0];
 242    eqb: carr → carr → bool;
 243    eqb_true: ∀x,y. eqb x y = true → x=y;
 244    eqb_false: ∀x,y. eqb x y = false → x≠y
 245  }.
 246
 247 nlet rec move (S: decidable) (x:S) (E: pre S) on E ≝
 248  match E with
 249   [ pz ⇒ 〈 false, pz ? 〉
 250   | pe ⇒ 〈 false, pe ? 〉
 251   | ps y ⇒ 〈false, ps ? y 〉
 252   | pp y ⇒ 〈 eqb … x y, ps ? y 〉
 253   | pc E1 E2 ⇒
 254      let E1' ≝ move ? x E1 in
 255      let E2' ≝ move ? x E2 in
 256      let E1'' ≝ snd … E1' in
 257      let E2'' ≝ snd ?? E2' in
 258       match fst … E1' with
 259        [ true =>
 260           let E2''' ≝ eclose S E2'' in
 261            〈 fst … E2' ∨ fst … E2''', pc ? E1'' (snd … E2''') 〉
 262        | false ⇒ 〈 fst … E2', pc ? E1'' E2'' 〉 ]
 263   | po E1 E2 ⇒
 264      let E1' ≝ move ? x E1 in
 265      let E2' ≝ move ? x E2 in
 266       〈 fst … E1' ∨ fst … E2', po ? (snd … E1') (snd … E2') 〉
 267   | pk E ⇒
 268      let E' ≝ move S x E in
 269      let E'' ≝ snd bool (pre S) E' in
 270       match fst … E' with
 271        [ true ⇒ 〈 true, pk ? (snd … (eclose … E'')) 〉
 272        | false ⇒ 〈 false, pk ? E'' 〉 ]].
 273
 274 (*
 275 ntheorem move_ok:
 276  ∀S:decidable.∀E,a,w.
 277   in_pl S w (snd … (move S a E)) → in_pl S (a::w) E.
 278  #S; #E; #a; #w;
 279 nqed.
 280 *)
 281
 282 nlet rec move_star S w E on w ≝
 283  match w with
 284   [ nil ⇒ E
 285   | cons x w' ⇒ move_star S w' (move S x (snd … E))].
 286
 287 ndefinition in_moves ≝ λS,w,E. fst … (move_star S w E).
 288
 289 ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
 290  mk_equiv:
 291   ∀E1,E2: bool × (pre S).
 292    fst ?? E1  = fst ?? E2 →
 293     (∀x. equiv S (move S x (snd … E1)) (move S x (snd … E2))) →
 294      equiv S E1 E2.
 295
 296 ndefinition NAT: decidable.
 297  @ nat eqb; /2/.
 298 nqed.
 299
 300 ninductive unit: Type[0] ≝ I: unit.
 301
 302 nlet corec foo_nop (b: bool):
 303  equiv NAT
 304   〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
 305   〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
 306  @; //; #x; ncases x
 307   [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 308   | #y; ncases y
 309      [ nnormalize in ⊢ (??%%); napply (foo_nop false)
 310      | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
 311 nqed.
 312
 313 nlet corec foo (a: unit):
 314  equiv NAT
 315   (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
 316   (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
 317 ≝ ?.
 318  @;
 319   ##[ nnormalize; //
 320   ##| #x; ncases x
 321        [ nnormalize in ⊢ (??%%);
 322          nnormalize in foo: (? → ??%%);
 323          @; //; #y; ncases y
 324            [ nnormalize in ⊢ (??%%); napply foo_nop
 325            | #y; ncases y
 326               [ nnormalize in ⊢ (??%%);
 327
 328             ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
 329      ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
 330   ##]
 331 nqed.
 332
 333 ndefinition test1 ≝
 334  pc ? (pk ? (po ? (ps ? 0) (ps ? 1))) (ps ? 0).
 335
 336 ndefinition test2 ≝
 337  po ?
 338   (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0))
 339   (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 1)).
 340
 341 ndefinition test3 ≝
 342  pk ? (pc ? (pc ? (ps ? 0) (pk ? (pc ? (ps ? 0) (ps ? 1)))) (ps ? 1)).
 343
 344 nlemma foo: in_moves NAT
 345   [0;0;1;0;1;1] (eclose ? test3) = true.
 346  nnormalize;
 347
 348 (**********************************************************)
 349
 350 ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
 351    der_z: der S a (z S) (z S)
 352  | der_e: der S a (e S) (z S)
 353  | der_s1: der S a (s S a) (e ?)
 354  | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
 355  | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
 356             der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
 357  | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
 358             der S a (c ? e1 e2) (c ? e1' e2)
 359  | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
 360     der S a (o ? e1 e2) (o ? e1' e2').
 361
 362 nlemma eq_rect_CProp0_r:
 363  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
 364  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
 365 nqed.
 366
 367 nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
 368
 369 naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
 370 (* #S; #r1; #r2; #w; nelim r1
 371   [ #K; ninversion K
 372   | #H1; #H2; napply (in_c ? []); //
 373   | (* tutti casi assurdi *) *)
 374
 375 ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
 376    in_l_empty1: ∀E.in_l S [] E → in_l' S [] E
 377  | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
 378
 379 ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
 380    mk_eq_re: ∀E1,E2.
 381     (in_l S [] E1 → in_l S [] E2) →
 382     (in_l S [] E2 → in_l S [] E1) →
 383     (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
 384       eq_re S E1 E2.
 385
 386 (* serve il lemma dopo? *)
 387 ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
 388  #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
 389   [ #r; #K (* ok *)
 390   | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
 391
 392 (* IL VICEVERSA NON VALE *)
 393 naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
 394 (* #S; #w; #E; #H; nelim H
 395   [ //
 396   | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
 397   ]
 398 nqed. *)
 399
 400 ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
 401  #S; #a; #E; #E'; #w; #H; nelim H
 402   [##1,2: #H1; ninversion H1
 403      [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
 404      |##2,9: #X; #Y; #K; ncases (?:False); /2/
 405      |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 406      |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 407      |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 408      |##6,13: #x; #y; #K; ncases (?:False); /2/
 409      |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
 410 ##| #H1; ninversion H1
 411      [ //
 412      | #X; #Y; #K; ncases (?:False); /2/
 413      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 414      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 415      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 416      | #x; #y; #K; ncases (?:False); /2/
 417      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 418 ##| #H1; #H2; #H3; ninversion H3
 419      [ #_; #K; ncases (?:False); /2/
 420      | #X; #Y; #K; ncases (?:False); /2/
 421      | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
 422      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 423      | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
 424      | #x; #y; #K; ncases (?:False); /2/
 425      | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
 426 ##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
 427