val minAndRen = DFA.renameStatesCanonically o DFA.minimize;
val regToDFA  = nfaToDFA o efaToNFA o faToEFA o regToFA;

fun elimVars(gram, nil)     = gram
  | elimVars(gram, q :: qs) =
      elimVars(Gram.eliminateVariable(gram, Sym.fromString q), qs);

(* DFA accepting all elements of {0, 1, 2, 3}^* of even length *)

val evenLenDFA =
      minAndRen(regToDFA(Reg.fromString "((0 + 1 + 2 + 3)(0 + 1 + 2 + 3))*"));

(* initial grammar generating Y *)

val new0 =
      Gram.restart
      (Gram.renameVariablesCanonically(Gram.minus(old, evenLenDFA)));

(* better grammar generating Y, resulting from variable elimination *)

val new1 = elimVars(new0, ["Q", "O", "J", "L", "F", "H", "C", "E"]);

(* renaming of variables so as to make the symmetry clear: <A>/A,
   <B>/B, <C>/C, <D>/D *)

val new =
      Gram.renameVariables
      (new1,
       SymRel.fromString
       ("(D, <A>), (B, A)," ^
        "(G, <B>), (I, B)," ^
        "(K, <C>), (M, C)," ^
        "(P, <D>), (N, D)"));