(* standard definitions *)

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

(* the alphabet {0, 1, 2, 3} *)

val syms0123 = SymSet.fromString "0, 1, 2, 3";

(* regular expression and DFA generating/accepting {0, 1, 2, 3}* *)

val allStrReg = Reg.closure(Reg.allSym syms0123);
val allStrDFA = minAndRen(regToDFA allStrReg);

(* symbolic relation on {0, 1, 2, 3} swapping 0 and 1 *)

val swap01 = SymRel.fromString "(0, 1), (1, 0), (2, 2), (3, 3)";

(* symbolic relation on {0, 1, 2, 3} swapping 0 and 2 *)

val swap02 = SymRel.fromString "(0, 2), (2, 0), (1, 1), (3, 3)";

(* symbolic relation on {0, 1, 2, 3} swapping 0 and 3 *)

val swap03 = SymRel.fromString "(0, 3), (3, 0), (1, 1), (2, 2)";

(* DFA accepting all elements of {0, 1, 2, 3}* with odd number of 1s *)

val odd1sDFA =
      minAndRen
      (DFA.minus
       (allStrDFA,
        DFA.renameAlphabet(even0sDFA, swap01)));

(* DFA accepting all elements of {0, 1, 2, 3}* with even number of 2s *)

val even2sDFA = DFA.renameAlphabet(even0sDFA, swap02);

(* DFA accepting all elements of {0, 1, 2, 3}* with odd number of 3s *)

val odd3sDFA =
      minAndRen
      (DFA.minus
       (allStrDFA,
        DFA.renameAlphabet(even0sDFA, swap03)));

(* DFA accepting all elements of {0, 1, 2, 3}* in which the
   number of 0s is even and the number of 1s is odd and the
   number of 2s is even and the number of 3s is odd *)

val paritiesDFA =
      minAndRen
      (DFA.genInter
       [even0sDFA, odd1sDFA, even2sDFA, odd3sDFA]);

(* grammar generating X *)

val gram0 =
      Gram.renameVariablesCanonically
      (Gram.inter(origGram, injDFAToEFA paritiesDFA));