diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal
deleted file mode 100644
index 37bc1ca..0000000
--- a/NominalAngluin.cabal
+++ /dev/null
@@ -1,69 +0,0 @@
-name:                NominalAngluin
-version:             0.1.0.0
-license:             UnspecifiedLicense
-author:              Joshua Moerman
-copyright:           (c) 2016 - 2020, Joshua Moerman
-build-type:          Simple
-cabal-version:       >=1.10
-
-executable NominalAngluin
-  main-is:             Main.hs
-  other-modules:
-    AbstractLStar,
-    Angluin,
-    Bollig,
-    Examples,
-    Examples.Contrived,
-    Examples.ContrivedNFAs,
-    Examples.Fifo,
-    Examples.NonResidual,
-    Examples.Residual,
-    Examples.RunningExample,
-    Examples.Stack,
-    NLStar,
-    ObservationTable,
-    Teacher,
-    Teachers.Teacher,
-    Teachers.Terminal,
-    Teachers.Whitebox
-  build-depends:
-    base >= 4.8 && < 5,
-    containers,
-    haskeline,
-    mtl,
-    NLambda >= 1.1
-  hs-source-dirs:      src
-  default-language:    Haskell2010
-  ghc-options:         -O2 -Wall
-
-executable NominalAngluin2
-  ghc-options:
-    -O2
-  main-is:             Main2.hs
-  other-modules:
-    AbstractLStar,
-    Angluin,
-    Bollig,
-    Examples,
-    Examples.Contrived,
-    Examples.ContrivedNFAs,
-    Examples.Fifo,
-    Examples.NonResidual,
-    Examples.Residual,
-    Examples.RunningExample,
-    Examples.Stack,
-    NLStar,
-    ObservationTable,
-    Teacher,
-    Teachers.Teacher,
-    Teachers.Terminal,
-    Teachers.Whitebox
-  build-depends:
-    base >= 4.8 && < 5,
-    containers,
-    haskeline,
-    mtl,
-    NLambda >= 1.1
-  hs-source-dirs:      src
-  default-language:    Haskell2010
-  ghc-options:         -O2 -Wall
diff --git a/src/Main.hs b/app/Main.hs
similarity index 98%
rename from src/Main.hs
rename to app/Main.hs
index dc3b632..4632a20 100644
--- a/src/Main.hs
+++ b/app/Main.hs
@@ -45,7 +45,7 @@ mainExample learnerName teacherName autName = do
     let h = case read learnerName of
             NomLStar    -> learnAngluinRows teacher
             NomLStarCol -> learnAngluin teacher
-            NomNLStar   -> learnBollig 1 1 teacher
+            NomNLStar   -> learnBollig 0 0 teacher
     print h
 
 mainWithIO :: String -> IO ()
diff --git a/src/Main2.hs b/app/Main2.hs
similarity index 100%
rename from src/Main2.hs
rename to app/Main2.hs
diff --git a/bench/Bench.hs b/bench/Bench.hs
new file mode 100644
index 0000000..3c723e2
--- /dev/null
+++ b/bench/Bench.hs
@@ -0,0 +1,14 @@
+import Bollig
+import Examples
+import Teacher
+
+import Criterion.Main
+
+main :: IO ()
+main = defaultMain [
+  bgroup "NomNLStar"
+    [ bench "NFA1 -" $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 2 Examples.exampleNFA1)
+    , bench "NFA2 1" $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 3 (Examples.exampleNFA2 1))
+    , bench "NFA2 2" $ whnf (learnBollig 0 0) (teacherWithTargetNonDet 4 (Examples.exampleNFA2 2))
+    ]
+  ]
diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal
new file mode 100644
index 0000000..87a0a91
--- /dev/null
+++ b/nominal-lstar.cabal
@@ -0,0 +1,62 @@
+cabal-version:       2.2
+name:                nominal-lstar
+version:             0.1.0.0
+author:              Joshua Moerman
+copyright:           (c) 2016 - 2020, Joshua Moerman
+build-type:          Simple
+extra-source-files:  README.md
+
+common stuff
+  default-language:  Haskell2010
+  ghc-options:       -O2 -Wall
+  build-depends:
+    base >= 4.8 && < 5,
+    containers,
+    haskeline,
+    mtl,
+    NLambda >= 1.1
+
+library
+  import: stuff
+  hs-source-dirs: src
+  exposed-modules:
+    AbstractLStar,
+    Angluin,
+    Bollig,
+    Examples,
+    Examples.Contrived,
+    Examples.ContrivedNFAs,
+    Examples.Fifo,
+    Examples.NonResidual,
+    Examples.Residual,
+    Examples.RunningExample,
+    Examples.Stack,
+    NLStar,
+    ObservationTable,
+    Teacher,
+    Teachers.Teacher,
+    Teachers.Terminal,
+    Teachers.Whitebox
+
+executable NominalAngluin
+  import: stuff
+  hs-source-dirs: app
+  main-is: Main.hs
+  build-depends:
+    nominal-lstar
+
+executable NominalAngluin2
+  import: stuff
+  hs-source-dirs: app
+  main-is: Main2.hs
+  build-depends:
+    nominal-lstar
+
+benchmark bench
+  import: stuff
+  hs-source-dirs: bench
+  type: exitcode-stdio-1.0
+  main-is: Bench.hs
+  build-depends:
+    criterion,
+    nominal-lstar
diff --git a/src/Bollig.hs b/src/Bollig.hs
index c956b82..2001007 100644
--- a/src/Bollig.hs
+++ b/src/Bollig.hs
@@ -8,7 +8,7 @@ import Teacher
 
 import Debug.Trace
 import NLambda
-import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.))
+import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.), (<=))
 import qualified Prelude hiding ()
 
 rowUnion :: NominalType i => Set (BRow i) -> BRow i
@@ -20,8 +20,7 @@ rowUnion set = Prelude.uncurry union . setTrueFalse . partition snd $ map (\is -
         setSecond a (x, _) = (x, a)
 
 boolImplies :: Bool -> Bool -> Bool
-boolImplies True False = False
-boolImplies _ _        = True
+boolImplies = (<=)
 
 sublang :: NominalType i => BRow i -> BRow i -> Formula
 sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf (i1 `eq` i2) (f1 `boolImplies` f2)) r1 r2
diff --git a/src/Examples/ContrivedNFAs.hs b/src/Examples/ContrivedNFAs.hs
index c5518b4..37eb139 100644
--- a/src/Examples/ContrivedNFAs.hs
+++ b/src/Examples/ContrivedNFAs.hs
@@ -57,4 +57,3 @@ exampleNFA2 n = automaton
         `union` sum (fromList [map (Count i, , Count (i+1)) atoms | i <- [0 .. n-1]]))
     (singleton Initial2)
     (singleton (Count n))
-
diff --git a/src/Examples/Residual.hs b/src/Examples/Residual.hs
index cb2b3d5..06dc3cf 100644
--- a/src/Examples/Residual.hs
+++ b/src/Examples/Residual.hs
@@ -15,6 +15,7 @@ import qualified Prelude ()
 data Res1 a = QR1 a | QR2 | QAncStar
   deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
 
+-- Language L = { w a | a fresh for w }, but anchored with a new symbol
 exampleResidual1 :: Automaton (Res1 Atom) DataInput
 exampleResidual1 = automaton
     -- state space