(* written so that the string length upper bound is a parameter; this
   generality was not required *)

(* val zeroOne : str set

   zeroOne = {0, 1} *)

val zeroOne = StrSet.fromString "0, 1";

(* val unwanted : int -> str set

   if n >= 0, then unwanted n returns all length-n elements of {0, 1}*
   with an occurrence of either 000/111 *)

fun unwanted n =
      if n < 3
      then Set.empty
      else let (* val bad : str set

                  bad = {000, 111} *)

               val bad = StrSet.fromString "000, 111"

               (* val unwant : int -> str set

                  if 1 <= m <= n - 2, then unwant m is all length n
                  elements of {0, 1}* with an occurrence of 000/111
                  beginning at one of the positions 1, ..., m *)

               fun unwant 1 = StrSet.concat(bad, StrSet.power(zeroOne, n - 3))
                 | unwant m =
                     StrSet.union
                     (StrSet.concat
                      (StrSet.power(zeroOne, m - 1),
                       StrSet.concat(bad,
                                     StrSet.power(zeroOne, n - 3 - (m - 1)))),
                      unwant(m - 1))
           in unwant(n - 2) end;

(* val atMost : int -> str set

   if n >= 0, then atMost n returns all elements of {0, 1}* that have
   length at most n and have no occurrences of 000/111 *)

fun atMost 0 = StrSet.minus(StrSet.power(zeroOne, 0), unwanted 0)
  | atMost n =
      StrSet.union(StrSet.minus(StrSet.power(zeroOne, n), unwanted n),
                   atMost(n - 1));

(* val atMostReg : int -> reg

   if n >= 0, then atMostReg n returns a Reg.weakSubset-simplified
   regular expression whose meaning is the set of all elements of {0,
   1}* that have length at most n and have no occurrences of 000/111 *)

fun atMostReg n = Reg.simplify Reg.weakSubset (Reg.fromStrSet(atMost n));