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

val allStrReg = Reg.fromString "(0 + 1 + 2)*";
val allStrDFA = regToDFAmar allStrReg;
val allStrFA  = injDFAToFA allStrDFA;

fun lenDFA m = regToDFAmar(Reg.power(Reg.fromString "0 + 1 + 2", m));

fun hasStrReg x    =
      Reg.concat(allStrReg, Reg.concat(strToReg x, allStrReg));
fun hasStrDFA x    = regToDFAmar(hasStrReg x);
fun notHasStrDFA x = minAndRen(DFA.minus(allStrDFA, hasStrDFA x));

val hasAllSymsDFA    =
      minAndRen
      (DFA.inter
       (hasStrDFA(Str.fromString "0"),
        DFA.inter
        (hasStrDFA(Str.fromString "1"),
         hasStrDFA(Str.fromString "2"))));
val notHasAllSymsDFA = minAndRen(DFA.minus(allStrDFA, hasAllSymsDFA));

fun lenAndNotHasAllSymsDFA m =
      minAndRen(DFA.inter(lenDFA m, notHasAllSymsDFA));
fun lenAndNotHasAllSymsFA m  = injDFAToFA(lenAndNotHasAllSymsDFA m);

fun someLenNotHasAllSymsFA m  =
      FA.concat(allStrFA, FA.concat(lenAndNotHasAllSymsFA m, allStrFA));
fun someLenNotHasAllSymsDFA m = faToDFAmar(someLenNotHasAllSymsFA m);

fun allLenHasAllSymsDFA m =
      minAndRen(DFA.minus(allStrDFA, someLenNotHasAllSymsDFA m));

val noBadDFA =
      minAndRen
      (DFA.inter
       (notHasStrDFA(Str.fromString "02"),
        DFA.inter
        (notHasStrDFA(Str.fromString "10"),
         notHasStrDFA(Str.fromString "21"))));

fun ansDFA m = minAndRen(DFA.inter(noBadDFA, allLenHasAllSymsDFA m));