val faToDFA   = nfaToDFA o efaToNFA o faToEFA;
val regToDFA  = faToDFA o regToFA;
val minAndRen = DFA.renameStatesCanonically o DFA.minimize;
val allStrDFA = minAndRen(regToDFA(Reg.fromString "(0 + 1 + 2)*"));
val allStrFA  = injDFAToFA allStrDFA;

fun hasSufFA x = FA.concat(allStrFA, strToFA x);
val hasSufDFA = minAndRen o faToDFA o hasSufFA;
fun hasNotSufDFA x = DFA.minus(allStrDFA, hasSufDFA x);
val hasNotSufFA = injDFAToFA o hasNotSufDFA;

fun hasPrefFA x = FA.concat(strToFA x, allStrFA);
val hasPrefDFA = minAndRen o faToDFA o hasPrefFA;
fun hasNotPrefDFA x = DFA.minus(allStrDFA, hasPrefDFA x);
val hasNotPrefFA = injDFAToFA o hasNotPrefDFA;

fun notSurFA(x,y,z) =
      FA.union(FA.concat(hasNotSufFA x,
                         FA.concat(strToFA y,
                                   allStrFA)),
               FA.concat(allStrFA,
                         FA.concat(strToFA y,
                                   hasNotPrefFA z)));
val notSurDFA = minAndRen o faToDFA o notSurFA;

fun surDFA(x, y, z) = minAndRen(DFA.minus(allStrDFA, notSurDFA(x, y, z)));