diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for typecheck-plugin-nat-simple
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Yoshikuni Jujo (c) 2020
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Yoshikuni Jujo nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,167 @@
+# typecheck-plugin-nat-simple
+
+## what's this
+
+This package provide plugin which extend type checking of Nat.
+The type checker can calculate only addition, subtraction and less or equal of
+constants and variables.
+
+(View sample code on directory sample/.)
+
+## motivation
+
+Suppose you need lengthed list. You define like following.
+(View `sample/lengthed_tail.hs`)
+
+```haskell
+import GHC.TypeNats
+
+infixr 6 :.
+
+data List :: Nat -> * -> * where
+        Nil :: List 0 a
+	(:.) :: a -> List ln a -> List (ln + 1) a
+```
+
+And you want to define function `tail`.
+
+```haskell
+tail_ :: List (n + 1) a -> List n a
+tail_ Nil = error "tail_: Nil"
+tail_ (_ :. xs) = xs
+```
+
+But it cause type check error.
+
+```
+error:
+  ・Could not deduce: ln ~ n
+    from the context: (n + 1) ~ (ln + 1)
+    ...
+```
+
+Type checker say "I cannot derive (ln == n) from (n + 1 == ln + 1)".
+But it seems to be obvious.
+You can use this plugin like following.
+
+```haskell
+{-# OPTIONS_GHC -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+```
+
+Add it to top of the code, then type check succeed.
+
+## more example
+
+To show more example, I will use Data.Proxy.Proxy.
+First examle is following (View `sample/mplus1_nplus1.hs`).
+
+```haskell
+foo :: (m + 1) ~ (n + 1) => Proxy m -> Proxy n
+foo = id
+```
+
+If you don't use this plugin, then following error occur.
+
+```
+  ・Could not deduce: m ~ n
+    from the context: (m + 1) ~ (n + 1)
+    ...
+```
+
+Use this plugin, you can compile it.
+
+Second example is following (View `sample/two_equations.hs`).
+
+```haskell
+foo :: ((x + y) ~ z, (w - y) ~ v) => Proxy (x + w) -> Proxy (z + v)
+foo = id
+```
+
+Without this plugin, following error occur.
+
+```
+  ・Could not deduce: (x + w) ~ (z + v)
+    from the context: ((x + y) ~ z, (w - y) ~ v)
+    ...
+```
+
+Use this plugin, you can compile it.
+
+## error and recovery
+
+### type check error
+
+See following code.
+
+```haskell
+foo :: Proxy (n - 1 + 1) -> Proxy n
+foo = id
+```
+
+This cause type check error even if you use this plugin.
+
+```
+  ・Couldn't match type `n' with `(n - 1) + 1'
+  ...
+```
+
+### research
+
+What's wrong?
+You can see type check log of this plugin like following.
+
+```
+% stack ghc sample/minus1plus1.hs -- -ddump-tc-trace 2>&1 | grep -A 20 'Plugin.TypeCheck.Nat.Simple'
+...
+givens ([Exp v 'Boolean]): given (Givens v): (Givens [])
+exBool: not boolean: (n_a1s2[sk:1] - 1) + 1
+wanted (Exp v 'Boolean): ((((Var n_a1s2[sk:1]) :- (Const 1)) :+ (Const 1)) :== (Var n_a1s2[sk:1]))
+wanted (Wanted v): (Wanted [(0 == 0), (1 * n_a1s2[sk:1] >= 0), (-1 + 1 * n_a1s2[sk:1] >= 0), (1 * n_a1s2[sk:1] >= 0)])
+canDerive1: (0 == 0) is self-contained
+canDerive1: (1 * n_a1s2[sk:1] >= 0) is self-contained
+canDerive1: (-1 + 1 * n_a1s2[sk:1] >= 0) cannot be derived from
+canDerive1: (1 * n_a1s2[sk:1] >= 0) is self-contained
+result: type checker: return False
+...
+```
+
+See the line of `canDerive1: (- 1 + 1 * n_a1s2[sk:1] >= 0) cannot be derived from`.
+It mean "`-1 + n_a1s2[sk:1]` should be greater or equal than 0. But no such context".
+
+### try calculation more portably
+
+You can try to caluculate more simply.
+
+```
+% stack ghci
+> :set -XTypeApplications
+> :module Data.Derivation.Parse Data.Derivation.CanDerive Control.Monad.Try Data.Maybe
+> parseConstraint "n - 1 + 1 == n"
+Just ((:==) ((:+) ((:=) (Var "n") (Const 1)) (Const 1)) (Var "n"))
+> Just w = wanted @String <$> it
+> gs = givens @String []
+> fst . runTry $ uncurry canDerive =<< (,) <$> gs <*> w
+Right False
+```
+
+The wanted constraint cannot be derived from empty given constraint.
+Let's add `1 <= n` constraint.
+
+```
+> gs = given @String . maybeToList $ parseConstraint "1 <= n"
+> fst . runTry $ uncurry canDerive =<< (,) <$> gs <*> w
+Right True
+```
+
+OK! It succeed if you add `1 <= n` to given constraint.
+
+### recovery
+
+Let's add `1 <= n` context like following.
+
+```haskell
+foo :: 1 <= n => Proxy (n - 1 + 1) -> Proxy n
+foo = id
+```
+
+Then it succeed to type check.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/sample/complex.hs b/sample/complex.hs
new file mode 100644
--- /dev/null
+++ b/sample/complex.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE ScopedTypeVariables, RankNTypes #-}
+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+import Data.Proxy
+
+main :: forall (a :: Nat) . IO ()
+main = do
+	print (foo (Proxy :: Proxy (a + 3)) :: Proxy (a + 3))
+--	print (bar (Proxy :: Proxy (a + 3)) :: Proxy (a + 3))
+--	print (bar (Proxy :: Proxy a) :: Proxy a)
+	print (bar (Proxy :: Proxy 123) :: Proxy 123)
+-- main = print (foo (Proxy :: Proxy a) :: Proxy a)
+
+foo :: ((m + n) ~ (j + k), (n - j) ~ 3) => Proxy (m + 3) -> Proxy k
+foo = id
+
+bar :: ((m + n) ~ (j + k), (n - j) ~ 3) => Proxy k -> Proxy (m + 3)
+bar = id
diff --git a/sample/lengthed_tail.hs b/sample/lengthed_tail.hs
new file mode 100644
--- /dev/null
+++ b/sample/lengthed_tail.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneDeriving #-}
+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+
+main :: IO ()
+main = print . tail_ $ 1 :. 2 :. 3 :. Nil
+
+infixr 6 :.
+
+data List :: Nat -> * -> * where
+	Nil :: List 0 a
+	(:.) :: a -> List ln a -> List (ln + 1) a
+
+deriving instance Show a => Show (List n a)
+
+tail_ :: List (n + 1) a -> List n a
+tail_ Nil = error "tail_: Nil"
+tail_ (_ :. xs) = xs
diff --git a/sample/minus1plus1.hs b/sample/minus1plus1.hs
new file mode 100644
--- /dev/null
+++ b/sample/minus1plus1.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import GHC.TypeNats
+import Data.Proxy
+
+main :: IO ()
+main = print $ foo @1 Proxy
+
+-- foo :: Proxy (n - 1 + 1) -> Proxy n
+foo :: 1 <= n => Proxy (n - 1 + 1) -> Proxy n
+foo = id
diff --git a/sample/mplus1_nplus1.hs b/sample/mplus1_nplus1.hs
new file mode 100644
--- /dev/null
+++ b/sample/mplus1_nplus1.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import GHC.TypeNats
+import Data.Proxy
+
+main :: IO ()
+main = print $ foo Proxy
+
+foo :: (m + 1) ~ (n + 1) => Proxy m -> Proxy n
+foo = id
diff --git a/sample/plus1minus1.hs b/sample/plus1minus1.hs
new file mode 100644
--- /dev/null
+++ b/sample/plus1minus1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import GHC.TypeNats
+import Data.Proxy
+
+main :: IO ()
+main = print $ foo Proxy
+
+foo :: Proxy (n + 1 - 1) -> Proxy n
+foo = id
diff --git a/sample/two_equations.hs b/sample/two_equations.hs
new file mode 100644
--- /dev/null
+++ b/sample/two_equations.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+-- {-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import GHC.TypeNats
+import Data.Proxy
+
+main :: IO ()
+main = print $ foo Proxy
+
+foo :: ((x + y) ~ z, (w - y) ~ v) => Proxy (x + w) -> Proxy (z + v)
+foo = id
diff --git a/src/Control/Monad/StateT.hs b/src/Control/Monad/StateT.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/StateT.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE BlockArguments, TupleSections #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Control.Monad.StateT (StateT(..), lift) where
+
+import Control.Applicative (Alternative(..))
+import Control.Arrow (first)
+import Control.Monad (MonadPlus, (>=>))
+
+---------------------------------------------------------------------------
+
+-- * NEWTYPE STATE T
+-- * INSTANCE
+--	+ FUNCTOR
+--	+ APPLICATIVE AND ALTERNATIVE
+--	+ MONAD AND MONAD PLUS
+
+---------------------------------------------------------------------------
+-- NEWTYPE STATE T
+---------------------------------------------------------------------------
+
+newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
+
+lift :: Functor m => m a -> StateT s m a
+lift m = StateT \s -> (, s) <$> m
+
+---------------------------------------------------------------------------
+-- INSTANCE
+---------------------------------------------------------------------------
+
+-- FUNCTOR
+
+instance Functor m => Functor (StateT s m) where
+	f `fmap` StateT k = StateT $ ((f `first`) <$>) . k
+
+-- APPLICATIVE AND ALTERNATIVE
+
+instance Monad m => Applicative (StateT s m) where
+	pure = StateT . (pure .) . (,)
+	StateT kf <*> mx = StateT $ kf >=> \(f, s') -> (f <$> mx) `runStateT` s'
+
+instance MonadPlus m => Alternative (StateT s m) where
+	empty = StateT $ const empty
+	StateT k <|> StateT l = StateT $ (<|>) <$> k <*> l
+
+-- MONAD AND MONAD PLUS
+
+instance Monad m => Monad (StateT s m) where
+	StateT k >>= f = StateT $ k >=> \(x, s') -> f x `runStateT` s'
+
+instance MonadPlus m => MonadPlus (StateT s m)
diff --git a/src/Control/Monad/Try.hs b/src/Control/Monad/Try.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Try.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE BlockArguments, LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Control.Monad.Try (
+	-- * DATA TRY
+	Try, maybeToTry,
+	-- * RUN TRY
+	runTry, gatherSuccess,
+	-- * THROW AND CATCH ERROR
+	throw, catch, rights,
+	-- * WRITE AND GET LOG
+	Set, tell, partial,
+	-- * TOOL
+	cons ) where
+
+import Control.Applicative (Alternative(..))
+import Control.Arrow (first)
+import Control.Monad (MonadPlus)
+import Data.Maybe (catMaybes)
+
+---------------------------------------------------------------------------
+
+-- * DATA TRY
+--	+ DATA
+--	+ INSTANCE
+-- * RUN TRY
+-- * THROW AND CATCH ERROR
+-- * WRITE AND GET LOG
+-- * TOOL
+
+---------------------------------------------------------------------------
+-- DATA TRY
+---------------------------------------------------------------------------
+
+-- DATA
+
+data Try e w a = Try (Either e a) w deriving Show
+
+try :: (Either e a -> w -> b) -> Try e w a -> b
+try f (Try ex w) = f ex w
+
+maybeToTry :: Monoid w => e -> Maybe a -> Try e w a
+maybeToTry e = maybe (throw e) pure
+
+-- INSTANCE
+
+instance Functor (Try e w) where
+	fmap f = try $ either (Try . Left) (Try . Right . f)
+
+instance Monoid w => Applicative (Try e w) where
+	pure = (`Try` mempty) . Right
+	Try (Left e) w <*> _ = Try (Left e) w
+	Try (Right f) w <*> mx = (\ex -> Try ex . (w <>)) `try` (f <$> mx)
+
+instance Monoid w => Alternative (Try w w) where
+	empty = Try (Left mempty) mempty
+	Try (Left e) w <|> t = tell w >> tell e >> t
+	t@(Try (Right _) _) <|> _ = t
+
+instance Monoid w => Monad (Try e w) where
+	Try (Left e) w >>= _ = Try (Left e) w
+	Try (Right x) w >>= f = (\ex -> Try ex . (w <>)) `try` f x
+
+instance Monoid w => MonadPlus (Try w w)
+
+---------------------------------------------------------------------------
+-- RUN TRY
+---------------------------------------------------------------------------
+
+runTry :: Try e w a -> (Either e a, w)
+runTry (Try ex w) = (ex, w)
+
+gatherSuccess :: (Monoid w, Set w w) => [Try w w a] -> ([a], w)
+gatherSuccess = (either (const []) id `first`) . runTry . rights
+
+---------------------------------------------------------------------------
+-- THROW AND CATCH ERROR
+---------------------------------------------------------------------------
+
+throw :: Monoid w => e -> Try e w a
+throw = (`Try` mempty) . Left
+
+catch :: Semigroup w => Try e w a -> (e -> Try e w a) -> Try e w a
+Try (Left e) w `catch` h = (\ex -> Try ex . (w <>)) `try` h e
+t@(Try (Right _) _) `catch` _ = t
+
+rights :: (Monoid w, Set w w) => [Try w w a] -> Try w w [a]
+rights = (catMaybes <$>) . mapM ((`catch` (Nothing <$) . tell) . (Just <$>))
+
+---------------------------------------------------------------------------
+-- WRITE AND GET LOG
+---------------------------------------------------------------------------
+
+class Set x xs where set :: x -> xs
+
+instance Set x x where set = id
+instance Monoid xs => Set x (x, xs) where set x = (x, mempty)
+
+instance {-# OVERLAPPABLE #-} (Monoid y, Set x xs) => Set x (y, xs) where
+	set x = (mempty, set x)
+
+tell :: Set w ws => w -> Try e ws ()
+tell = Try (Right ()) . set
+
+partial :: Try e (w, ws) a -> Try e ws (Either e a, w)
+partial (Try ex (w, ws)) = Try (Right (ex, w)) ws
+
+---------------------------------------------------------------------------
+-- TOOL
+---------------------------------------------------------------------------
+
+cons :: (Monoid w, Set w w) => Either w a -> [a] -> Try w w [a]
+cons = either (flip (<$) . tell) ((pure .) . (:))
diff --git a/src/Data/Derivation/CanDerive.hs b/src/Data/Derivation/CanDerive.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Derivation/CanDerive.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE BlockArguments, OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Derivation.CanDerive (
+	-- * CAN DERIVE
+	canDerive,
+	-- * GIVENS
+	Givens, givens,
+	-- * WANTED
+	Wanted, wanted ) where
+
+import Prelude hiding (unwords, log)
+
+import Control.Arrow (second)
+import Control.Monad ((<=<))
+import Control.Monad.Try (Try, throw, tell, cons)
+import Data.Map.Strict (empty)
+import Data.Either (partitionEithers)
+import Data.List (unfoldr, (\\), nub, partition, sort)
+import Data.Bool (bool)
+import Data.String (IsString)
+import Data.Log (Log, (.+.), intersperse, unwords, log, Loggable(..))
+import Data.Derivation.Constraint (
+	Constraint,
+	vars, has, isDerivFrom, positives, selfContained, eliminate )
+import Data.Derivation.Expression.Internal (
+	Exp, ExpType(..), constraint, varBool )
+
+---------------------------------------------------------------------------
+
+-- * CAN DERIVE
+-- * GIVENS
+--	+ NEWTYPE GIVENS AND CONSTRUCTOR
+--	+ GIVENS VARIABLES
+--	+ REMOVE VARIABLE
+-- * WANTED
+
+---------------------------------------------------------------------------
+-- CAN DERIVE
+---------------------------------------------------------------------------
+
+canDerive :: (IsString s, Ord v) => Givens v -> Wanted v -> Try e (Log s v) Bool
+canDerive g = (canDerive1 g `allM`) . unWanted
+
+allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
+p `allM` xs = and <$> p `mapM` xs
+
+canDerive1 :: forall s v e .
+	(IsString s, Ord v) => Givens v -> Wanted1 v -> Try e (Log s v) Bool
+canDerive1 g w = (s || d) <$ if s
+	then t $ ttl .+. lw .+. " is self-contained"
+	else t $ ttl .+. lw .+. " can" .+. nt .+. " be derived from"
+	where
+	s = selfContained w
+	d = any (w `isDerivFrom`) . unGivens . foldr rmVar g $ gVars g \\ vars w
+	t = tell @(Log s v)
+	ttl = "canDerive1: "; lw = log w; nt = bool "not" "" d
+
+---------------------------------------------------------------------------
+-- GIVENS
+---------------------------------------------------------------------------
+
+-- NEWTYPE GIVENS AND CONSTRUCTOR
+
+newtype Givens v = Givens { unGivens :: [Constraint v] } deriving Show
+
+instance IsString s => Loggable s v (Givens v) where
+	log (Givens cs) = "(Givens [" .+. intersperse ", " (log <$> cs) .+. "])"
+
+givens :: forall s v . (IsString s, Ord v) =>
+	[Exp v 'Boolean] -> Try (Log s v) (Log s v) (Givens v)
+givens gs = do
+	t $ "givens ([Exp v 'Boolean]): " .+. unwords (log <$> gs)
+	gs' <- Givens . nub . sort . ((++) <$> id <*> (positives <$>)) . concat
+		<$> (uncurry cons <=< constraint (varBool gs)) `mapM` gs
+	gs' <$ t ("givens (Givens v): " .+. log gs')
+	where t = tell @(Log s v)
+
+-- GIVENS VARIABLES
+
+gVars :: Ord v => Givens v -> [Maybe v]
+gVars = nub . sort . concat . (vars <$>) . unGivens
+
+-- REMOVE VARIABLE
+
+rmVar :: Ord v => Maybe v -> Givens v -> Givens v
+rmVar v (Givens gs) = Givens . sort . concat . uncurry (:)
+	. second (unfoldUntil null (rvStep v)) $ partition (not . (`has` v)) gs
+
+rvStep :: Ord v => Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])
+rvStep _ [] = ([], [])
+rvStep v (c : cs) = partitionEithers $ rmVar1 v c <$> cs
+
+rmVar1 :: Ord v => Maybe v -> Constraint v ->
+	Constraint v -> Either (Constraint v) (Constraint v)
+rmVar1 v c0 c = maybe (Right c) Left $ eliminate v c0 c
+
+unfoldUntil :: (s -> Bool) -> (s -> (r, s)) -> s -> [r]
+unfoldUntil p f = unfoldr $ flip bool Nothing <$> Just . f <*> p
+
+---------------------------------------------------------------------------
+-- WANTED
+---------------------------------------------------------------------------
+
+newtype Wanted v = Wanted { unWanted :: [Wanted1 v] } deriving Show
+
+type Wanted1 v = Constraint v
+
+instance IsString s => Loggable s v (Wanted v) where
+	log (Wanted cs) = "(Wanted [" .+. intersperse ", " (log <$> cs) .+. "])"
+
+wanted :: forall s v . (IsString s, Ord v) =>
+	Exp v 'Boolean -> Try (Log s v) (Log s v) (Wanted v)
+wanted w = do
+	t $ "wanted (Exp v 'Boolean): " .+. log w
+	(e, s) <- constraint empty w
+	w' <- either throw (pure . Wanted . (: s)) e
+	w' <$ t ("wanted (Wanted v): " .+. log w')
+	where t = tell @(Log s v)
diff --git a/src/Data/Derivation/Constraint.hs b/src/Data/Derivation/Constraint.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Derivation/Constraint.hs
@@ -0,0 +1,144 @@
+{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Derivation.Constraint (
+	Constraint, equal, greatEqualThan, greatThan, vars, has,
+	isDerivFrom, positives, selfContained, eliminate,
+	Poly, (.+), (.-) ) where
+
+import Prelude hiding (null, filter)
+
+import Control.Monad (guard)
+import Data.Map.Strict (Map, null, singleton, (!?), filter, toList, lookupMin)
+import Data.Map.Merge.Strict (
+	merge, preserveMissing, mapMissing,
+	zipWithMatched, zipWithMaybeMatched )
+import Data.Maybe (isJust)
+import Data.String (IsString, fromString)
+import Data.Log (Log, logVar, (.+.), intersperse, Loggable(..))
+
+---------------------------------------------------------------------------
+
+-- * CONSTRAINT
+--	+ DATA CONSTRAINT
+--	+ CONSTRUCT
+--	+ READ
+-- 	+ CONVERT
+-- * POLYNOMIAL
+-- 	+ TYPE POLY
+-- 	+ CONSTRUCT
+-- 	+ READ
+-- 	+ CONVERT
+
+---------------------------------------------------------------------------
+-- CONSTRAINT
+---------------------------------------------------------------------------
+
+-- DATA CONSTRAINT
+
+data Constraint v = Eq (Poly v) | Geq (Poly v) deriving (Show, Eq, Ord)
+
+constraint :: (Poly v -> a) -> (Poly v -> a) -> Constraint v -> a
+constraint f g = \case Eq p -> f p; Geq p -> g p
+
+instance IsString s => Loggable s v (Constraint v) where
+	log = constraint
+		(\p -> "(" .+. polyToLog (toList p) .+. " == 0)")
+		(\p -> "(" .+. polyToLog (toList p) .+. " >= 0)")
+
+-- CONSTRUCT
+
+equal :: Ord v => Poly v -> Poly v -> Constraint v
+l `equal` r = Eq . posit . reduce $ l .- r
+
+greatEqualThan :: Ord v => Poly v -> Poly v -> Constraint v
+l `greatEqualThan` r = Geq . reduce $ l .- r
+
+greatThan :: Ord v => Poly v -> Poly v -> Constraint v
+l `greatThan` r = Geq $ reduce (l .- r) .- singleton Nothing 1
+
+-- READ
+
+vars :: Ord v => Constraint v -> [Maybe v]
+vars = (fst <$>) . constraint toList toList
+
+has :: Ord v => Constraint v -> Maybe v -> Bool
+has = constraint (\p -> isJust . (p !?)) (\p -> isJust . (p !?))
+
+selfContained :: Constraint v -> Bool
+selfContained = constraint null $ all (>= 0)
+
+isDerivFrom :: Ord v => Constraint v -> Constraint v -> Bool
+Eq w `isDerivFrom` Eq g = w == g
+Geq w `isDerivFrom` Eq g = w `isGeqThan` g
+Geq w `isDerivFrom` Geq g = w `isGeqThan` g
+_ `isDerivFrom` _ = False
+
+-- CONVERT
+
+positives :: Constraint v -> Constraint v
+positives = constraint Eq $ Geq . filter (>= 0)
+
+eliminate ::
+	Ord v => Maybe v -> Constraint v -> Constraint v -> Maybe (Constraint v)
+eliminate v (Eq l) (Eq r) = Eq . posit . reduce . uncurry (.+) <$> alignEE v l r
+eliminate v (Eq l) (Geq r) = Geq . reduce . uncurry (.+) <$> alignEG v l r
+eliminate v (Geq l) (Geq r) = Geq . reduce . uncurry (.+) <$> alignGG v l r
+eliminate v l r = eliminate v r l
+
+type Aligned v = Maybe (Poly v, Poly v)
+
+alignEE :: Ord v => Maybe v -> Poly v -> Poly v -> Aligned v
+alignEE v l r =
+	(<$> ((,) <$> l !? v <*> r !? v)) \(m, s) -> (l `mul` s, r `mul` (- m))
+
+alignEG :: Ord v => Maybe v -> Poly v -> Poly v -> Aligned v
+alignEG v l r = (<$> ((,) <$> l !? v <*> r !? v)) \(m, s) ->
+	(l `mul` (- signum m * s), r `mul` abs m)
+
+alignGG :: Ord v => Maybe v -> Poly v -> Poly v -> Aligned v
+alignGG v l r = (,) <$> l !? v <*> r !? v >>= \(m, s) ->
+	(l `mul` abs s, r `mul` abs m) <$ guard (m * s < 0)
+
+---------------------------------------------------------------------------
+-- POLYNOMIAL
+---------------------------------------------------------------------------
+
+-- TYPE POLY
+
+type Poly v = Map (Maybe v) Integer
+
+polyToLog :: IsString s => [(Maybe v, Integer)] -> Log s v
+polyToLog [] = "0"
+polyToLog ps = intersperse " + " $ polyToLog1 <$> ps
+
+polyToLog1 :: IsString s => (Maybe v, Integer) -> Log s v
+polyToLog1 (Nothing, n) = fromString $ show n
+polyToLog1 (Just v, n) = fromString (show n ++ " * ") .+. logVar v
+
+-- CONSTRUCT
+
+(.+), (.-) :: Ord v => Poly v -> Poly v -> Poly v
+(.+) = merge preserveMissing preserveMissing
+	(zipWithMaybeMatched \_ a b -> (<$) <$> id <*> guard . (/= 0) $ a + b)
+(.-) = merge preserveMissing (mapMissing $ const negate)
+	(zipWithMaybeMatched \_ a b -> (<$) <$> id <*> guard . (/= 0) $ a - b)
+
+-- READ
+
+isGeqThan :: Ord v => Poly v -> Poly v -> Bool
+isGeqThan = (and .) . merge
+	(mapMissing \_ nl -> nl >= 0)
+	(mapMissing \_ nr -> nr <= 0) (zipWithMatched $ const (>=))
+
+-- CONVERT
+
+posit :: Poly v -> Poly v
+posit p = p `maybe` ((p `mul`) . signum . snd) $ lookupMin p
+
+reduce :: Poly v -> Poly v
+reduce = divide <$> id <*> foldr gcd 0
+
+mul, divide :: Poly v -> Integer -> Poly v
+mul p = (<$> p) . (*); divide p = (<$> p) . flip div
diff --git a/src/Data/Derivation/Expression.hs b/src/Data/Derivation/Expression.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Derivation/Expression.hs
@@ -0,0 +1,7 @@
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Derivation.Expression (
+	-- * DATA EXP
+	Exp(..), ExpType(..) ) where
+
+import Data.Derivation.Expression.Internal (Exp(..), ExpType(..))
diff --git a/src/Data/Derivation/Expression/Internal.hs b/src/Data/Derivation/Expression/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Derivation/Expression/Internal.hs
@@ -0,0 +1,158 @@
+{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Derivation.Expression.Internal (
+	Exp(..), ExpType(..), constraint, varBool ) where
+
+import Prelude hiding ((<>), log)
+
+import Outputable (Outputable(..), SDoc, (<>), (<+>), text)
+import Control.Arrow (first, second)
+import Control.Monad.Try (Try, throw, tell, partial)
+import Data.Map.Strict (Map, (!?), empty, singleton, insert)
+import Data.Maybe (fromJust)
+import Data.List (find)
+import Data.String (IsString, fromString)
+import Data.Log (Log, (.+.), logVar, Loggable(..))
+import Data.Derivation.Constraint (
+	Constraint, equal, greatEqualThan, greatThan, Poly, (.+), (.-) )
+
+---------------------------------------------------------------------------
+
+-- * DATA EXP
+--	+ DATA
+--	+ INSTANCE
+-- * CONSTRAINT
+--	+ CONSTRAINT
+--	+ PROCESS EQUATION
+-- * POLYNOMIAL
+-- * MAP FROM VARIABLE TO BOOL
+
+---------------------------------------------------------------------------
+-- DATA EXP
+---------------------------------------------------------------------------
+
+-- DATA
+
+data Exp v t where
+	Bool :: Bool -> Exp v 'Boolean; Var :: v -> Exp v t
+	Const :: Integer -> Exp v 'Number
+	(:==) :: Exp v t -> Exp v t -> Exp v 'Boolean
+	(:<=) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Boolean
+	(:+) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Number
+	(:-) :: Exp v 'Number -> Exp v 'Number -> Exp v 'Number
+
+data ExpType = Boolean | Number deriving Show
+
+-- INSTANCE
+
+deriving instance Show v => Show (Exp v t)
+
+instance Outputable v => Outputable (Exp v t) where
+	ppr = \case
+		Bool b -> text "(Bool" <+> ppr b <> text ")"
+		Var v -> text "(Var" <+> ppr v <> text ")"
+		Const n -> text "(Const" <+> ppr n <> text ")"
+		l :== r -> pprOp ":==" l r; l :<= r -> pprOp ":<=" l r
+		l :+ r -> pprOp ":+" l r; l :- r -> pprOp ":-" l r
+
+pprOp :: Outputable v => String -> Exp v t -> Exp v t -> SDoc
+pprOp op l r = text "(" <> ppr l <+> text op <+> ppr r <> text ")"
+
+instance IsString s => Loggable s v (Exp v t) where
+	log = \case
+		Bool b -> fromString $ "(Bool " ++ show b ++ ")"
+		Var v -> fromString "(Var " .+. logVar v .+. fromString ")"
+		Const n -> fromString $ "(Const " ++ show n ++ ")"
+		l :== r -> logOp ":==" l r; l :<= r -> logOp ":<=" l r
+		l :+ r -> logOp ":+" l r; l :- r -> logOp ":-" l r
+
+logOp :: IsString s => String -> Exp v t -> Exp v t -> Log s v
+logOp op l r = fromString "(" .+.
+	log l .+. fromString (" " ++ op ++ " ") .+. log r .+. fromString ")"
+
+---------------------------------------------------------------------------
+-- CONSTRAINT
+---------------------------------------------------------------------------
+
+-- CONSTRAINT
+
+constraint :: (Monoid w, IsString s, Ord v) => VarBool v -> Exp v 'Boolean ->
+	Try (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
+constraint vb ex = partial $ procEq vb ex True
+
+-- PROCCESS EQUATION
+
+procEq :: (Monoid w, IsString s, Ord v) => VarBool v -> Exp v 'Boolean ->
+	Bool -> Try (Log s v) ([Constraint v], w) (Constraint v)
+procEq _ b@(Bool _) _ = throw $ "procEq: only Boolean value: " .+. log b
+procEq _ v@(Var _) _ = throw $ "procEq: only Variable: " .+. log v
+procEq _ (l :<= r) False = greatThan <$> poly l <*> poly r
+procEq _ (l :<= r) True = greatEqualThan <$> poly r <*> poly l
+procEq vb (l :== Bool r) b = procEq vb l (r == b)
+procEq vb (Bool l :== r) b = procEq vb r (l == b)
+procEq vb e@(l :== Var r) b | Just br <- vb !? r = case l of
+	_ :== _ -> procEq vb l (br == b); _ :<= _ -> procEq vb l (br == b)
+	_ -> throw $ "procEq: can't interpret: " .+. log e
+procEq vb e@(Var l :== r) b | Just bl <- vb !? l = case r of
+	_ :== _ -> procEq vb r (bl == b); _ :<= _ -> procEq vb r (bl == b)
+	_ -> throw $ "procEq: can't interpret: " .+. log e
+procEq _ e@(l :== r) True = case (l, r) of
+	(Const _, _) -> equal <$> poly l <*> poly r
+	(_ :+ _, _) -> equal <$> poly l <*> poly r
+	(_ :- _, _) -> equal <$> poly l <*> poly r
+	(_, Const _) -> equal <$> poly l <*> poly r
+	(_, _ :+ _) -> equal <$> poly l <*> poly r
+	(_, _ :- _) -> equal <$> poly l <*> poly r
+	(Var v, Var w) -> equal <$> poly (Var v) <*> poly (Var w)
+	_ -> throw $ "procEq: can't interpret: " .+. log e .+. " == True"
+procEq _ e@(_ :== _) False =
+	throw $ "procEq: can't interpret: " .+. log e .+. " == False"
+
+---------------------------------------------------------------------------
+-- POLYNOMIAL
+---------------------------------------------------------------------------
+
+poly :: (Monoid s, IsString e, Ord v) =>
+	Exp v 'Number -> Try e ([Constraint v], s) (Poly v)
+poly = \case
+	Const n	| n < 0 -> throw
+			. fromString $ "poly: Negative constant " ++ show n
+		| 0 <- n -> pure empty
+		| otherwise -> pure $ singleton Nothing n
+	Var v -> let p = singleton (Just v) 1 in
+		p <$ tell [p `greatEqualThan` empty]
+	l :+ r -> (.+) <$> poly l <*> poly r
+	l :- r -> (,) <$> poly l <*> poly r >>= \(pl, pr) ->
+		pl .- pr <$ tell [pl `greatEqualThan` pr]
+
+---------------------------------------------------------------------------
+-- MAP FROM VARIABLES TO BOOL
+---------------------------------------------------------------------------
+
+type VarBool v = Map v Bool
+
+varBool :: Ord v => [Exp v 'Boolean] -> VarBool v
+varBool = snd . untilFixed (uncurry vbStep) . vbInit
+
+vbInit :: Ord v => [Exp v 'Boolean] -> ([(v, v)], VarBool v)
+vbInit [] = ([], empty)
+vbInit (Var l :== Var r : es) = ((l, r) :) `first` vbInit es
+vbInit (Var l :== Bool r : es) = insert l r `second` vbInit es
+vbInit (Bool l :== Var r : es) = insert r l `second` vbInit es
+vbInit (_ : es) = vbInit es
+
+vbStep :: Ord v => [(v, v)] -> VarBool v -> ([(v, v)], VarBool v)
+vbStep [] vb = ([], vb)
+vbStep ((l, r) : vs) vb = case (vb !? l, vb !? r) of
+	(Just bl, _) -> vbStep vs $ insert r bl vb
+	(Nothing, Just br) -> vbStep vs $ insert l br vb
+	(Nothing, Nothing) -> ((l, r) :) `first` vbStep vs vb
+
+untilFixed :: Eq a => (a -> a) -> a -> a
+untilFixed f x = fst . fromJust . find (uncurry (==)) $ zip xs (tail xs)
+	where xs = iterate f x
diff --git a/src/Data/Derivation/Parse.hs b/src/Data/Derivation/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Derivation/Parse.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Derivation.Parse (
+	-- * PARSE CONSTRAINT
+	parseConstraint, Var ) where
+
+import Control.Applicative (empty, (<|>), many)
+import Control.Arrow (second)
+import Data.Function ((&))
+import Data.Maybe (listToMaybe)
+import Data.List (uncons, unfoldr)
+import Data.Char (isDigit, isLower)
+import Data.Parse (Parse, parse, unparse, (>>!))
+import Data.Derivation.Expression (Exp(..), ExpType(..))
+
+import qualified Data.Bool as B (bool)
+
+---------------------------------------------------------------------------
+
+-- * PARSE CONSTRAINT
+-- * MEMO
+-- * GRAMMAR
+-- * PICK AND CHECK
+
+---------------------------------------------------------------------------
+-- PARSE CONSTRAINT
+---------------------------------------------------------------------------
+
+parseConstraint :: String -> Maybe (Exp Var 'Boolean)
+parseConstraint = (fst <$>) . constraint . memo . unfoldr (listToMaybe . lex)
+
+---------------------------------------------------------------------------
+-- MEMO
+---------------------------------------------------------------------------
+
+data Memo = Memo {
+	constraint, equal, bool, lessEqual :: M (Exp Var 'Boolean),
+	polynomial, number :: M (Exp Var 'Number), token :: M String }
+
+type M a = Maybe (a, Memo); type Var = String
+
+memo :: [String] -> Memo
+memo ts = m where
+	m = Memo ct eq bl le pl nm tk
+	ct = pConstraint `unparse` m
+	eq = pEqual `unparse` m
+	bl = pBool `unparse` m
+	le = pLessEqual `unparse` m
+	pl = pPolynomial `unparse` m
+	nm = pNumber `unparse` m
+	tk = (memo `second`) <$> uncons ts
+
+---------------------------------------------------------------------------
+-- GRAMMAR
+---------------------------------------------------------------------------
+
+-- Constraint <- Equal / LessEqual
+-- Equal <-
+--	var "==" var !("+" / "-" / "<=") /
+--	var "==" Polynomial !"<=" /
+--	var "==" Bool /
+--	Polynomial "==" Polynomial /
+--	Bool "==" Bool
+-- Bool <- LessEqual / "F" / "T" / var
+-- LessEqual <- Polynomial "<=" Polynomial
+-- Polynomial <- Number ("+" Number / "-" Number)*
+-- Number <- <digit string> / var / "(" Polynomial ")"
+
+pConstraint :: Parse Memo (Exp Var 'Boolean)
+pConstraint = parse equal <|> parse lessEqual
+
+pEqual :: Parse Memo (Exp Var 'Boolean)
+pEqual =
+	(:==) <$> var <* pick "==" <*> var
+		>>! (pick "+" <|> pick "-" <|> pick "<=") <|>
+	(:==) <$> var <* pick "==" <*> parse polynomial >>! pick "<=" <|>
+	(:==) <$> var <* pick "==" <*> parse bool <|>
+	(:==) <$> parse polynomial <* pick "==" <*> parse polynomial <|>
+	(:==) <$> parse bool <* pick "==" <*> parse bool
+
+pBool :: Parse Memo (Exp Var 'Boolean)
+pBool =	parse lessEqual <|>
+	Bool False <$ pick "F" <|> Bool True <$ pick "T" <|> var
+
+pLessEqual :: Parse Memo (Exp Var 'Boolean)
+pLessEqual = (:<=) <$> parse polynomial <* pick "<=" <*> parse polynomial
+
+pPolynomial :: Parse Memo (Exp Var 'Number)
+pPolynomial = foldl (&) <$> parse number <*> many (
+	flip (:+) <$> (pick "+" *> parse number) <|>
+	flip (:-) <$> (pick "-" *> parse number) )
+
+pNumber :: Parse Memo (Exp Var 'Number)
+pNumber = Const . read <$> check (all isDigit) <|> var <|>
+	pick "(" *> parse polynomial <* pick ")"
+
+var :: Parse Memo (Exp Var t)
+var = Var <$> check (all isLower)
+
+---------------------------------------------------------------------------
+-- PICK AND CHECK
+---------------------------------------------------------------------------
+
+pick :: String -> Parse Memo String
+pick = check . (==)
+
+check :: (String -> Bool) -> Parse Memo String
+check p = parse token >>= B.bool empty <$> pure <*> p
diff --git a/src/Data/Log.hs b/src/Data/Log.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Log.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE BlockArguments, LambdaCase, OverloadedStrings #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Log (
+	-- * LOG
+	-- ** DATA LOG
+	Log, logVar, (.+.), intersperse, unwords,
+	-- ** CLASS
+	Loggable(..), Message(..),
+	-- * SDOC
+	IsSDoc(..), SDocStr ) where
+
+import Prelude hiding (unwords, log)
+
+import Outputable (Outputable, SDoc, empty, ppr, text, ($$))
+import Data.String (IsString(..))
+
+import qualified Outputable as O ((<>))
+
+---------------------------------------------------------------------------
+
+-- * LOG
+--	+ NEWTYPE LOG
+--	+ INSTANCE
+--	+ FUNCTION
+--	+ CLASS
+-- * SDOC
+
+---------------------------------------------------------------------------
+-- LOG
+---------------------------------------------------------------------------
+
+-- NEWTYPE LOG
+
+newtype Log s v = Log ([[Either s v]] -> [[Either s v]])
+
+-- INSTANCE
+
+instance Semigroup (Log s v) where Log l <> Log r = Log $ l . r
+instance Monoid (Log s v) where mempty = Log id
+
+instance (Show s, Show v) => Show (Log s v) where
+	show (Log k) = "(Log (" ++ show (k []) ++ " ++))"
+
+instance (Outputable s, Outputable v) => Outputable (Log s v) where
+	ppr (Log k) = foldr ($$) empty $ pprLog1 <$> k []
+
+pprLog1 :: (Outputable s, Outputable v) => [Either s v] -> SDoc
+pprLog1 = foldr (O.<>) empty . (either ppr ppr <$>)
+
+instance (Message s, Show v) => Message (Log s v) where
+	message (Log k) = unlines $ messageLog1 <$> k []
+
+messageLog1 :: (Message s, Show v) => [Either s v] -> String
+messageLog1 = concatMap $ either message show
+
+instance IsString s => IsString (Log s v) where
+	fromString = Log . (++) . ((: []) . Left . fromString <$>) . lines
+
+instance IsSDoc s => IsSDoc (Log s v) where
+	fromSDoc = Log . (:) . (: []) . Left . fromSDoc
+
+-- FUNCTION
+
+logVar :: v -> Log s v
+logVar v = Log ([Right v] :)
+
+infixr 7 .+.
+
+(.+.) :: Log s v -> Log s v -> Log s v
+Log l .+. Log r = Log $ (l [] %) . r where
+	[] % yss = yss
+	[xs] % (ys : yss) = (xs ++ ys) : yss
+	(xs : xss) % yss = xs : (xss % yss)
+
+intersperse :: Log s v -> [Log s v] -> Log s v
+intersperse s = \case [] -> mempty; ls -> foldr1 (\l -> (l .+.) . (s .+.)) ls
+
+unwords :: IsString s => [Log s v] -> Log s v
+unwords = intersperse " "
+
+-- CLASS
+
+class Loggable s v a where log :: a -> Log s v
+
+class Message s where
+	message :: s -> String
+	messageList :: [s] -> String
+	messageList = unlines . (message <$>)
+
+instance Message s => Message [s] where message = messageList
+instance Message Char where message = (: []); messageList = id
+
+---------------------------------------------------------------------------
+-- SDOC STRING
+---------------------------------------------------------------------------
+
+class IsSDoc s where fromSDoc :: SDoc -> s
+
+data SDocStr = SDocStrEmpty | SDocStr SDoc
+
+instance Semigroup SDocStr where
+	SDocStrEmpty <> r = r; l <> SDocStrEmpty = l
+	SDocStr l <> SDocStr r = SDocStr $ l $$ r
+
+instance Monoid SDocStr where mempty = SDocStrEmpty
+instance Outputable SDocStr where ppr SDocStrEmpty = empty; ppr (SDocStr s) = s
+instance IsString SDocStr where fromString = SDocStr . text
+instance IsSDoc SDocStr where fromSDoc = SDocStr
diff --git a/src/Data/Parse.hs b/src/Data/Parse.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Parse.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE BlockArguments #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Data.Parse (Parse, parse, unparse, (>>!)) where
+
+import Control.Applicative (empty)
+import Control.Monad ((>=>))
+import Control.Monad.StateT (StateT(..))
+
+type Parse s = StateT s Maybe
+
+parse :: (s -> Maybe (a, s)) -> Parse s a
+parse = StateT
+
+unparse :: Parse s a -> s -> Maybe (a, s)
+unparse = runStateT
+
+(>>!) :: Parse s a -> Parse s b -> Parse s a
+p >>! nla = parse $ unparse p >=> \r@(_, s) ->
+	maybe (pure r) (const empty) $ nla `unparse` s
diff --git a/src/Plugin/TypeCheck/Nat/Simple.hs b/src/Plugin/TypeCheck/Nat/Simple.hs
new file mode 100644
--- /dev/null
+++ b/src/Plugin/TypeCheck/Nat/Simple.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE BlockArguments, OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Plugin.TypeCheck.Nat.Simple (
+	-- * PLUGIN
+	plugin ) where
+
+import Prelude hiding (log)
+
+import GhcPlugins (Plugin, Var, ppr)
+import Control.Monad.Try (tell)
+import Data.Log (Log, (.+.), fromSDoc, SDocStr)
+import Data.Derivation.CanDerive (canDerive, givens, wanted)
+import Plugin.TypeCheck.Nat.Simple.TypeCheckWith (typeCheckWith)
+import Plugin.TypeCheck.Nat.Simple.Decode (decode, decodeAll)
+
+type L = Log SDocStr Var
+
+-- | > type L = Log SDocStr Var
+--   >
+--   > plugin :: Plugin
+--   > plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w ->
+--   >	tell @L $ "givens: " .+. fromSDoc (ppr gs)
+--   >	tell @L $ "wanted: " .+. fromSDoc (ppr w)
+--   >	uncurry canDerive
+--   >		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)
+
+plugin :: Plugin
+plugin = typeCheckWith @L "Plugin.TypeCheck.Nat.Simple" \gs _ w -> do
+	tell @L $ "givens: " .+. fromSDoc (ppr gs)
+	tell @L $ "wanted: " .+. fromSDoc (ppr w)
+	uncurry canDerive
+		=<< (,) <$> (givens =<< decodeAll gs) <*> (wanted =<< decode w)
diff --git a/src/Plugin/TypeCheck/Nat/Simple/Decode.hs b/src/Plugin/TypeCheck/Nat/Simple/Decode.hs
new file mode 100644
--- /dev/null
+++ b/src/Plugin/TypeCheck/Nat/Simple/Decode.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE BlockArguments, OverloadedStrings #-}
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Plugin.TypeCheck.Nat.Simple.Decode (
+	-- * DECODE CT
+	decodeAll, decode ) where
+
+import TcRnTypes (Ct)
+import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon, typeNatLeqTyCon)
+import TysWiredIn (promotedFalseDataCon, promotedTrueDataCon)
+import TyCoRep (Type(..), TyLit(..))
+import Var (Var)
+import Outputable (ppr, text, (<+>))
+import Control.Applicative ((<|>))
+import Control.Monad ((<=<))
+import Control.Monad.Try (Try, throw, rights, Set)
+import Data.Log (IsSDoc, fromSDoc)
+import Data.Derivation.Expression (Exp(..), ExpType(..))
+import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)
+
+---------------------------------------------------------------------------
+
+-- * DECODE
+-- * BOOLEAN AND NUMBER
+
+---------------------------------------------------------------------------
+-- DECODE
+---------------------------------------------------------------------------
+
+decodeAll :: (Monoid w, IsSDoc w, Set w w) => [Ct] -> Try w w [Exp Var 'Boolean]
+decodeAll = rights . (decode <$>)
+
+decode :: (Monoid w, IsSDoc w) => Ct -> Try w w (Exp Var 'Boolean)
+decode = uncurry decodeTs <=< unNomEq
+
+decodeTs :: (Monoid w, IsSDoc w) => Type -> Type -> Try w w (Exp Var 'Boolean)
+decodeTs (TyVarTy l) (TyVarTy r) = pure $ Var l :== Var r
+decodeTs l r = (:==) <$> exBool l <*> exBool r <|> (:==) <$> exNum l <*> exNum r
+
+---------------------------------------------------------------------------
+-- BOOLEAN AND NUMBER
+---------------------------------------------------------------------------
+
+exBool :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Boolean)
+exBool (TyVarTy v) = pure $ Var v
+exBool (TyConApp tc [])
+	| tc == promotedFalseDataCon = pure $ Bool False
+	| tc == promotedTrueDataCon = pure $ Bool True
+exBool (TyConApp tc [l, r])
+	| tc == typeNatLeqTyCon = (:<=) <$> exNum l <*> exNum r
+exBool t = throw . fromSDoc $ text "exBool: not boolean:" <+> ppr t
+
+exNum :: (Monoid s, IsSDoc e) => Type -> Try e s (Exp Var 'Number)
+exNum (TyVarTy v) = pure $ Var v
+exNum (LitTy (NumTyLit n)) = pure $ Const n
+exNum (TyConApp tc [l, r])
+	| tc == typeNatAddTyCon = (:+) <$> exNum l <*> exNum r
+	| tc == typeNatSubTyCon = (:-) <$> exNum l <*> exNum r
+exNum t = throw . fromSDoc $ text "exNum: not number:" <+> ppr t
diff --git a/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs b/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs
new file mode 100644
--- /dev/null
+++ b/src/Plugin/TypeCheck/Nat/Simple/TypeCheckWith.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Plugin.TypeCheck.Nat.Simple.TypeCheckWith (
+	-- * TYPE CHECK WITH
+	typeCheckWith ) where
+
+import GhcPlugins (
+	Plugin(..), defaultPlugin, Expr(..), mkUnivCo, Role(..),
+	Outputable, ppr, text )
+import TcPluginM (TcPluginM, tcPluginTrace)
+import TcRnTypes (TcPlugin(..), Ct, TcPluginResult(..))
+import TcEvidence (EvTerm(..))
+import TyCoRep (UnivCoProvenance(..))
+import Control.Monad.Try (Try, gatherSuccess, throw, Set)
+import Data.Bool (bool)
+import Data.Log (IsSDoc, fromSDoc)
+import Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq)
+
+---------------------------------------------------------------------------
+
+typeCheckWith :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>
+	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) -> Plugin
+typeCheckWith hd ck = defaultPlugin { tcPlugin = const $ Just TcPlugin {
+	tcPluginInit = pure (), tcPluginSolve = const $ solve hd ck,
+	tcPluginStop = const $ pure () } }
+
+solve :: (Monoid w, Outputable w, IsSDoc w, Set w w) =>
+	String -> ([Ct] -> [Ct] -> Ct -> Try w w Bool) ->
+	[Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
+solve hd ck gs ds ws = TcPluginOk rs [] <$ tcPluginTrace hd (ppr lgs)
+	where (rs, lgs) = gatherSuccess $ result hd ck gs ds <$> ws
+
+result :: (Monoid s, IsSDoc e) =>
+	String -> ([Ct] -> [Ct] -> Ct -> Try e s Bool) ->
+	[Ct] -> [Ct] -> Ct -> Try e s (EvTerm, Ct)
+result hd ck gs ds w = unNomEq w >>= \(l, r) ->
+	bool (throw em) (pure (et l r, w)) =<< ck gs ds w
+	where
+	em = fromSDoc $ text "result: type checker: return False"
+	et = ((EvExpr . Coercion) .) . mkUnivCo (PluginProv hd) Nominal
diff --git a/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs b/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs
new file mode 100644
--- /dev/null
+++ b/src/Plugin/TypeCheck/Nat/Simple/UnNomEq.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+module Plugin.TypeCheck.Nat.Simple.UnNomEq (unNomEq) where
+
+import TcRnTypes (Ct, ctEvidence, ctEvPred)
+import Type (Type, PredTree(..), EqRel(..), classifyPredType)
+import Outputable (ppr, text, (<+>))
+import Control.Monad.Try (Try, throw)
+import Data.Log (IsSDoc, fromSDoc)
+
+unNomEq :: (Monoid w, IsSDoc e) => Ct -> Try e w (Type, Type)
+unNomEq ct = case classifyPredType . ctEvPred $ ctEvidence ct of
+	EqPred NomEq l r -> pure (l, r)
+	_ -> throw . fromSDoc
+		$ text "unNomEq: no match to EqPred NomEq l r:" <+> ppr ct
diff --git a/test/log.hs b/test/log.hs
new file mode 100644
--- /dev/null
+++ b/test/log.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds, TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}
+
+import GHC.TypeNats
+import Data.Proxy
+
+foo :: 1 <= n => Proxy (n - 1 + 1) -> Proxy (n + 1 - 1)
+foo = id
+
+main :: IO ()
+main = putStrLn "test log"
diff --git a/test/spec.hs b/test/spec.hs
new file mode 100644
--- /dev/null
+++ b/test/spec.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import Data.Derivation.CanDerive
+import Data.Derivation.Parse
+
+import Control.Monad.Try
+
+main :: IO ()
+main = do
+	print $ wanted @String @String =<< maybeToTry "parse error" (parseConstraint "0 == n - n")
diff --git a/test/tryLog.hs b/test/tryLog.hs
new file mode 100644
--- /dev/null
+++ b/test/tryLog.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE BlockArguments, OverloadedStrings #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
+
+import Outputable
+import Control.Monad.Try hiding (Message)
+import Data.String
+import Data.Log
+
+main :: IO ()
+main = do
+	let	(r, l) = runTry do
+			n <- 8 `devide` 3 :: Try (Log String Int) (Log String Int) Int
+			(15 `devide` 0) `catch` \e -> tell e >> pure (n + 0)
+	putStr $ message l
+	putStrLn . showSDocUnsafe $ ppr l
+	print r
+
+devide :: forall s . (IsString s, Message s) => Int -> Int -> Try (Log s Int) (Log s Int) Int
+m `devide` 0 = throw $ logVar m .+. " is devided by " .+. logVar 0
+m `devide` n = do
+	tell (logVar m .+. " is devided by " .+. logVar n :: Log s Int)
+	pure $ m `div` n
diff --git a/typecheck-plugin-nat-simple.cabal b/typecheck-plugin-nat-simple.cabal
new file mode 100644
--- /dev/null
+++ b/typecheck-plugin-nat-simple.cabal
@@ -0,0 +1,106 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 37e93024d7892b53d4f73b5eaf1a2fd50b85d7b7ccf19998c52119e2bfdee1b8
+
+name:           typecheck-plugin-nat-simple
+version:        0.1.0.0
+synopsis:       Simple type check plugin which calculate addition, subtraction and less-or-equal-than
+description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple#readme>
+category:       Compiler Plugin
+homepage:       https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple#readme
+bug-reports:    https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple/issues
+author:         Yoshikuni Jujo
+maintainer:     yoshikuni.jujo.pc@gmail.com
+copyright:      Yoshikuni Jujo
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+data-files:
+    lengthed_tail.hs
+    plus1minus1.hs
+    two_equations.hs
+    minus1plus1.hs
+    complex.hs
+    mplus1_nplus1.hs
+data-dir:       sample
+
+source-repository head
+  type: git
+  location: https://github.com/YoshikuniJujo/typecheck-plugin-nat-simple
+
+library
+  exposed-modules:
+      Plugin.TypeCheck.Nat.Simple
+      Plugin.TypeCheck.Nat.Simple.TypeCheckWith
+      Plugin.TypeCheck.Nat.Simple.Decode
+      Data.Derivation.CanDerive
+      Data.Derivation.Expression
+      Data.Derivation.Parse
+      Control.Monad.Try
+      Data.Log
+  other-modules:
+      Control.Monad.StateT
+      Data.Derivation.Constraint
+      Data.Derivation.Expression.Internal
+      Data.Parse
+      Plugin.TypeCheck.Nat.Simple.UnNomEq
+      Paths_typecheck_plugin_nat_simple
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , ghc
+  default-language: Haskell2010
+
+test-suite typecheck-plugin-nat-simple-test-log
+  type: exitcode-stdio-1.0
+  main-is: log.hs
+  other-modules:
+      Paths_typecheck_plugin_nat_simple
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , ghc
+    , typecheck-plugin-nat-simple
+  default-language: Haskell2010
+
+test-suite typecheck-plugin-nat-simple-test-spec
+  type: exitcode-stdio-1.0
+  main-is: spec.hs
+  other-modules:
+      Paths_typecheck_plugin_nat_simple
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , ghc
+    , typecheck-plugin-nat-simple
+  default-language: Haskell2010
+
+test-suite typecheck-plugin-nat-simple-test-tryLog
+  type: exitcode-stdio-1.0
+  main-is: tryLog.hs
+  other-modules:
+      Paths_typecheck_plugin_nat_simple
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , ghc
+    , typecheck-plugin-nat-simple
+  default-language: Haskell2010