val zero      = Sym.fromString "0";
val one       = Sym.fromString "1";
val minAndRen =
      DFA.renameStatesCanonically o DFA.minimize;
val efaToDFA  = nfaToDFA o efaToNFA;
val strToEFA  = faToEFA o strToFA;
val allStrEFA =
      EFA.closure
      (EFA.union(injNFAToEFA(symToNFA zero), injNFAToEFA(symToNFA one)));
val allStrDFA = minAndRen(efaToDFA allStrEFA);

fun hasSubEFA x =
      EFA.concat
      (injDFAToEFA allStrDFA,
       EFA.concat(strToEFA x, injDFAToEFA allStrDFA));

val hasSubDFA = minAndRen o efaToDFA o hasSubEFA;

fun hasNotSubDFA x = minAndRen(DFA.minus(allStrDFA, hasSubDFA x));

fun someUnmatchedEFA(x, y) =
      EFA.concat
      (injDFAToEFA(hasNotSubDFA y),
       EFA.concat(strToEFA x, injDFAToEFA(hasNotSubDFA y)));

val someUnmatchedDFA = minAndRen o efaToDFA o someUnmatchedEFA;

fun allMatchedDFA(x, y) =
      minAndRen(DFA.minus(allStrDFA, someUnmatchedDFA(x, y)));

fun dcsDFA(x, y) =
      minAndRen(DFA.inter(allMatchedDFA(x, y), allMatchedDFA(y, x)));