diff --git a/GL.hs b/GL.hs
--- a/GL.hs
+++ b/GL.hs
@@ -1,10 +1,12 @@
-{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE UnicodeSyntax, FlexibleInstances #-}
 module GL () where
 
+import Prelude.Unicode
 import Graph
 import GraphRewriting.Layout.PortSpec
 import qualified Graphics.UI.GLUT as GL
 import GraphRewriting.GL.Render
+import GraphRewriting.Strategies.Control
 
 
 instance PortSpec NodeLS where
@@ -12,59 +14,76 @@
 		Initiator  {} → [sd s]
 		Applicator {} → [sd n, sd s, sd e]
 		Abstractor {} → [sd n, sd s, sd e]
-		Constant   {} → [sd n]
-		Function   {} → [sd n, sd s]
+		Constant   {} → sd n : [sd $ rm (alpha args*x) `mmul` sws | x <- [0..la args - 1]]
 		Eraser     {} → [sd n]
 		Duplicator {} → [(Vector2 0 0.9, n), (Vector2 (-0.6) (-0.5), s), (Vector2 0.6 (-0.5), s)]
 		Delimiter  {} → [sd $ Vector2 0 0.7, sd $ Vector2 0 (-0.7)]
+		Case       {} → sd n : sd e : [sd $ rm (alpha alts * x) `mmul` sws | x <- [0..la alts - 1]]
+		Operator   {} → sd n : [sd $ rm (alpha ops*x) `mmul` sws | x <- [0..la ops - 1]]
 		where
-			n = Vector2 0 1
-			w = Vector2 (-1) 0
-			e = Vector2 1 0
-			s = Vector2 0 (-1)
+			n  = Vector2 0 1
+			w  = Vector2 (-1) 0
+			e  = Vector2 1 0
+			s  = Vector2 0 (-1)
 			sw = Vector2 (-1) (-1)
 			se = Vector2 1 (-1)
 
+			la field = toEnum $ length (field node)
+			alpha f  = pi/(2*la f)
+			rm t     = ((cos t, sin t), (-sin t, cos t))
+			mmul ((x1,y1),(x2,y2)) (Vector2 x y) = Vector2 (x1*x+x2*y) (y1*x+y2*y)
+			sws = Vector2 (-0.7) (-0.7)
+
 instance Render NodeLS where render = renderNode
 
+instance Render n ⇒ Render (Wrapper n) where
+	render c = do
+		render $ wrapped c
+		case control c of
+			NoControl  → return ()
+			Control {} → GL.renderPrimitive GL.LineLoop (circle 1.2 1.2 20)
+
 renderNode node = drawPorts node >> case node of
 	Initiator  {} → drawNode "I"
 	Applicator {} → drawNode "@"
 	Abstractor {} → drawNode (name node)
 	Constant   {} → drawNode (name node)
-	Function   {} → drawNode (name node)
 	Eraser     {} → drawNode ""
 	Duplicator {} → do
 		GL.preservingMatrix $ GL.renderPrimitive GL.LineLoop $ do
 			vertex2 (0,0.9)
 			vertex2 (-1,-0.5)
 			vertex2 (1,-0.5)
-		drawString $ show $ level node
+		renderString $ show $ level node
 	Delimiter {} → do
-		GL.renderPrimitive GL.LineStrip $ do
+		GL.preservingMatrix $ GL.renderPrimitive GL.LineStrip $ do
 			vertex2 (-0.8,-0.3)
 			vertex2 (-0.8,0)
 			vertex2 (0.8,0)
 			vertex2 (0.8,-0.3)
-		drawString $ show $ level node
+		renderString $ show $ level node
+	Case      {} → drawNode ("case [" ++ foldr1 (\x y → x ++ ", " ++ y) (names node) ++ "]")
+	Operator  {} → drawNode (name node)
 
-drawPorts ∷ NodeLS -> IO ()
-drawPorts = mapM_ drawPort . relPortPos
+drawPorts ∷ NodeLS → IO ()
+drawPorts n = sequence_ [drawPort (factor p) pos | (pos, p) ← positions `zip` ports] where
+	positions = relPortPos n
+	ports = inspect n
+	isLmo p = maybe False (p ≡) (lmo n)
+	factor p
+		| isLmo p   = 1.5
+		| p ≡ pp n  = 2.0
+		| otherwise = 1
 
 circle r1 r2 step = mapM_ vertex2 vs where
 	is = take (truncate step + 1) [0, i' .. ]
 	i' = 2 * pi / step
 	vs = [ (r1 * cos i, r2 * sin i) | i <- is ]
 
-drawPort pos = GL.preservingMatrix $ do
+drawPort factor pos = GL.preservingMatrix $ do
 	GL.translate $ vector pos
-	GL.renderPrimitive GL.Polygon (circle 0.15 0.15 10)
+	GL.renderPrimitive GL.Polygon (circle (factor * 0.15) (factor * 0.15) 20)
 
 drawNode label = do
 	GL.renderPrimitive GL.LineLoop (circle 1 1 20)
-	drawString label
-
-drawString label = GL.preservingMatrix $ do
-	GL.translate $ vector2 (-0.3,-0.3)
-	GL.scale 0.007 0.007 (0 ∷ GL.GLdouble)
-	GL.renderString GL.MonoRoman label
+	renderString label
diff --git a/Graph.hs b/Graph.hs
--- a/Graph.hs
+++ b/Graph.hs
@@ -5,18 +5,22 @@
 import Data.View
 import GraphRewriting.Graph.Types
 import GraphRewriting.Pattern.InteractionNet
-
+-- import Control
+import GraphRewriting.Strategies.LeftmostOutermost
 
+-- | The signature of our graph
 data NodeLS
-	= Initiator  {out ∷ Port}
-	| Applicator {inp, func, arg ∷ Port}
-	| Abstractor {inp, body, var ∷ Port, name ∷ String}
-	| Constant   {inp ∷ Port, name ∷ String}
-	| Function   {inp ∷ Port, out ∷ Port , name ∷ String}
-	| Eraser     {inp ∷ Port}
-	| Duplicator {level ∷ Int, inp, out1, out2 ∷ Port}
-	| Delimiter  {level ∷ Int, inp, out ∷ Port}
-	| Multiplier {out ∷ Port, ins ∷ [Port]} -- only intermediate compilation result
+	= Initiator   {out ∷ Port}
+	| Applicator  {inp, func, arg ∷ Port}
+	| Abstractor  {inp, body, var ∷ Port, name ∷ String}
+	| Constant    {inp ∷ Port, args ∷ [Port], name ∷ String}
+	| Eraser      {inp ∷ Port}
+	| Duplicator  {level ∷ Int, inp, out1, out2 ∷ Port}
+	| Delimiter   {level ∷ Int, inp, out ∷ Port}
+	| Multiplexer {out ∷ Port, ins ∷ [Port]} -- only intermediate compilation result
+	| Case        {inp ∷ Port, out ∷ Port, alts ∷ [Port], names ∷ [String]}
+	| Operator    {inp ∷ Port, ops ∷ [Port], arity ∷ Int, lmop ∷ Int,
+	               function ∷ [String] → String, name ∷ String}
 
 -- | equality as defined in the paper with only the relevant cases included
 instance Eq NodeLS where
@@ -27,35 +31,54 @@
 
 instance View [Port] NodeLS where
 	inspect node = case node of
-		Initiator  {out = o}                       → [o]
-		Applicator {inp = i, func = f, arg = a}    → [i,f,a]
-		Abstractor {inp = i, body = b, var = v}    → [i,b,v]
-		Constant   {inp = i}                       → [i]
-		Function   {inp = i, out = o}              → [i,o]
-		Eraser     {inp = i}                       → [i]
-		Duplicator {inp = i, out1 = o1, out2 = o2} → [i,o1,o2]
-		Delimiter  {inp = i, out = o}              → [i,o]
-		Multiplier {out = o, ins = is}             → o:is
+		Initiator   {out = o}                       → [o]
+		Applicator  {inp = i, func = f, arg = a}    → [i,f,a]
+		Abstractor  {inp = i, body = b, var = v}    → [i,b,v]
+		Constant    {inp = i, args = as}            → i:as
+		Eraser      {inp = i}                       → [i]
+		Duplicator  {inp = i, out1 = o1, out2 = o2} → [i,o1,o2]
+		Delimiter   {inp = i, out = o}              → [i,o]
+		Multiplexer {out = o, ins = is}             → o:is
+		Case        {inp = i, out = o, alts = as}   → i:o:as
+		Operator    {inp = i, ops = os}             → i:os
 	update ports node = case node of
-		Initiator  {} → node {out = o}                       where [o]       = ports
-		Applicator {} → node {inp = i, func = f, arg = a}    where [i,f,a]   = ports
-		Abstractor {} → node {inp = i, body = b, var = v}    where [i,b,v]   = ports
-		Constant   {} → node {inp = i}                       where [i]       = ports
-		Function   {} → node {inp = i, out = o}              where [i,o]     = ports
-		Eraser     {} → node {inp = i}                       where [i]       = ports
-		Duplicator {} → node {inp = i, out1 = o1, out2 = o2} where [i,o1,o2] = ports
-		Delimiter  {} → node {inp = i, out = o}              where [i,o]     = ports
-		Multiplier {} → node {out = o, ins = is}             where o:is      = ports
+		Initiator   {} → node {out = o}                       where [o]       = ports
+		Applicator  {} → node {inp = i, func = f, arg = a}    where [i,f,a]   = ports
+		Abstractor  {} → node {inp = i, body = b, var = v}    where [i,b,v]   = ports
+		Constant    {} → node {inp = i, args = as}            where i:as      = ports
+		Eraser      {} → node {inp = i}                       where [i]       = ports
+		Duplicator  {} → node {inp = i, out1 = o1, out2 = o2} where [i,o1,o2] = ports
+		Delimiter   {} → node {inp = i, out = o}              where [i,o]     = ports
+		Multiplexer {} → node {out = o, ins = is}             where o:is      = ports
+		Case        {} → node {inp = i, out = o, alts = as}   where i:o:as    = ports
+		Operator    {} → node {inp = i, ops = os}             where i:os      = ports
 
-instance INet NodeLS where principalPort = pp 
-	
-pp ∷ NodeLS → Int 
+instance INet NodeLS where principalPort = pp
+
+-- The number is an index that specifies which port is the principal port out of the list of ports
+pp ∷ NodeLS → Port
 pp node = case node of
-	Initiator  {} → 0
-	Applicator {} → 1
-	Abstractor {} → 0
-	Delimiter  {} → 0
-	Constant   {} → 0
-	Function   {} → 1
-	Duplicator {} → 0
-	Eraser     {} → 0
+	Initiator   {out = o}                       → o
+	Applicator  {inp = i, func = f, arg = a}    → f
+	Abstractor  {inp = i, body = b, var = v}    → i
+	Constant    {inp = i, args = as}            → i
+	Eraser      {inp = i}                       → i
+	Duplicator  {inp = i, out1 = o1, out2 = o2} → i
+	Delimiter   {inp = i, out = o}              → i
+	Multiplexer {out = o, ins = is}             → o
+	Case        {inp = i, out = o, alts = as}   → o
+	Operator    {lmop = i, ops = os}            → inspect node !! i
+
+instance LeftmostOutermost NodeLS where lmoPort = lmo
+
+lmo ∷ NodeLS → Maybe Port
+lmo node = case node of
+	Initiator   {out = o}                       → Just o
+	Applicator  {inp = i, func = f, arg = a}    → Just f
+	Abstractor  {inp = i, body = b, var = v}    → Nothing
+	Constant    {inp = i, args = as}            → Nothing
+	Eraser      {inp = i}                       → Just i
+	Duplicator  {inp = i, out1 = o1, out2 = o2} → Just i
+	Delimiter   {inp = i, out = o}              → Just i
+	Case        {inp = i, out = o, alts = as}   → Just o
+	Operator    {lmop = i, ops = os}            → Just $ inspect node !! i
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -1,6 +1,8 @@
-{-# LANGUAGE UnicodeSyntax, FlexibleInstances #-}
+{-# LANGUAGE UnicodeSyntax, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
 module Main where
 
+import Prelude.Unicode
+import Data.List (delete)
 import GraphRewriting.Graph
 import GraphRewriting.GL.Render
 import GraphRewriting.GL.UI as UI
@@ -16,22 +18,45 @@
 import GraphRewriting.Layout.Coulomb
 import GraphRewriting.Layout.SpringEmbedder
 import GraphRewriting.Layout.Gravitation
-import GraphRewriting.Layout.Wrapper
+import GraphRewriting.Layout.Wrapper as Layout
 
+import GraphRewriting.Strategies.Control as Control
+import GraphRewriting.Strategies.LeftmostOutermost
 
-instance Render (Wrapper NodeLS) where render = render . wrappee
 
+instance Render n ⇒ Render (Layout.Wrapper n) where render = render . wrappee
+instance PortSpec n ⇒ PortSpec (Control.Wrapper n) where portSpec = portSpec . wrapped
+instance LeftmostOutermost n ⇒ LeftmostOutermost (Layout.Wrapper n) where lmoPort = lmoPort . wrappee
+
+
 main ∷ IO ()
 main = do
 	(prog,args) ← UI.initialise
+	let lmo = "--lmo" ∈ args
+	args ← return $ "--lmo" `delete` args
 	file ← case args of
 		[f] → return f
-		___ → error "usage: lambdascope [GLUT-options] <file>"
+		___ → error "usage: lambdascope [GLUT-options] [--lmo] <file>"
 	term ← parseFile file
-	let hypergraph = resolve term
-	let graph = execGraph (apply $ exhaustive compileShare) (wrapGraph hypergraph)
-	UI.run 50 id layoutStep graph ruleTree
+	let hypergraph = execGraph (apply $ exhaustive compileShare) (resolve term)
+	let layoutGraph = Layout.wrapGraph hypergraph
 
+	if lmo
+		then UI.run 50 id layoutStep (Control.wrapGraph layoutGraph) (lmoTree ruleTree)
+		else UI.run 50 id layoutStep layoutGraph ruleTree
+
+-- | Modifies the rules of the rule tree with a given function.
+-- This can be used to for example wrap a strategy rule around the existing rules.
+mapRules :: (n -> m) -> LabeledTree n -> LabeledTree m
+mapRules f (Leaf n r)    = Leaf n (f r)
+mapRules f (Branch n rs) = Branch n (map (mapRules f) rs)
+
+-- Appends a rule to the top branch of a rule tree
+appendRule :: n -> LabeledTree n -> LabeledTree n
+appendRule r l@(Leaf n rr) = Branch n [l, Leaf "moveControl" r]
+appendRule r (Branch n rs) = Branch n (rs ++ [Leaf "moveControl" r])
+
+-- layoutStep :: (View Rotation n, View [Port] n, View Position n) => n -> IO ()
 layoutStep n = do
 	(cgf, cf, sf, rot) ← readOnly $ do
 		cgf ← centralGravitation n
@@ -39,16 +64,24 @@
 		sf ← springForce 1.5 n
 		rot ← angularMomentum n
 		return (cgf, cf, sf, rot)
-	Unsafe.adjustNode (Position . sf (\x → min 10 (x*0.9)) . cgf (\x → min 10 (x*0.01)) . cf (\x → min 10 (100/(x^2+0.1))) . position) n
-	Unsafe.adjustNode (rot (*0.9)) n
+	Unsafe.adjustNode n $ Position . sf (\x → min 10 (x*0.9)) . cgf (\x → min 10 (x*0.01)) . cf (\x → min 10 (100/(x^2+0.1))) . position
+	Unsafe.adjustNode n $ rot (*0.9)
 
+lmoTree ∷ (LeftmostOutermost n, View [Port] n, View Control n) ⇒ LabeledTree (Rule n) -> LabeledTree (Rule n)
+lmoTree = appendRule moveControl . mapRules leftmostOutermost
+
+ruleTree :: (View NodeLS n, View [Port] n) => LabeledTree (Rule n)
 ruleTree = Branch "All"
 	[Leaf "Beta Reduction" beta,
 	 Branch "All but Beta"
 	 	[Leaf "Duplicate" duplicate,
-	 	 Leaf "Eliminate" (eliminateDelimiter <|> eliminateDuplicator),
+	 	 Leaf "Eliminate" (eliminateDelimiterEraser <|> eliminateDelimiterConstant <|> eliminateDuplicator),
 	 	 Leaf "Annihilate" annihilate,
 	 	 Leaf "Commute Delimiter" commuteDelimiter,
-	 	 Leaf "Erase" eraser, 
-	 	 Branch "Primitive" [Leaf "Constant" applyConstant, Leaf "Function" applyFunction]],
-	 Leaf "All but Beta (exhaustively)" $ exhaustive $ anyOf [duplicate, eliminateDelimiter, eliminateDuplicator, annihilate, commuteDelimiter, eraser, applyConstant, applyFunction]]
+	 	 Leaf "Erase" eraser,
+		 Leaf "Case" caseNode,
+	 	 Branch "Primitive"
+			[Leaf "Constant" applyConstant,
+			 Leaf "Apply Operator" applyOperator,
+			 Leaf "Exec Operator" execOperator,
+			 Leaf "Reduce Operator Args" reduceOperatorArgs]]]
diff --git a/Resolver.hs b/Resolver.hs
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -7,7 +7,8 @@
 import Graph
 import GraphRewriting.Graph
 import GraphRewriting.Graph.Write
-import Control.Monad (liftM, zipWithM)
+import Control.Monad
+import Data.Maybe (fromMaybe)
 
 
 type Compiler = Rewrite NodeLS
@@ -26,34 +27,48 @@
 	A func arg → do
 		f ← newEdge
 		x ← newEdge
-		newNode Applicator {inp = p, func = f, arg = x}
+		void $ newNode Applicator {inp = p, func = f, arg = x}
 		compile env f func
 		compile env x arg
 	Λ x e → do
 		b ← newEdge
 		(v, name) ← bindName True x
-		newNode Abstractor {inp = p, body = b, var = v, name = x}
+		void $ newNode Abstractor {inp = p, body = b, var = v, name = x}
 		compile (name : env) b e
-	V var → case env of
-		[  ] → newNode Constant {inp = p, name = var} >> return ()
-		n:ns → if var ≡ symbol n
-			then mergeEdges p =<< reference n
-			else if boundByLambda n
-				then do
-					p' ← newEdge
-					newNode Delimiter {level = 0, inp = p', out = p}
-					compile ns p' term
-				else compile ns p term
 	L binds e → do
 		(es, names) ← liftM unzip $ mapM (bindName False) (map fst binds)
 		let env' = names ⧺ env
-		zipWithM (compile env') es (Prelude.map snd binds)
+		void $ zipWithM (compile env') es (Prelude.map snd binds)
 		compile env' p e
+	C name [] → case env of
+		[  ] → void $ newNode $ fromMaybe (Constant {inp = p, name = name, args = []}) (operator name p)
+		n:ns → if name ≡ symbol n
+			then mergeEdges p =<< reference n
+			else if boundByLambda n
+					then do
+						p' ← newEdge
+						void $ newNode Delimiter {level = 0, inp = p', out = p}
+						compile ns p' term
+					else compile ns p term
+	Term.Case exp cases → do
+		let (pats, _) = unzip cases
+		alts ← replicateM (length cases) newEdge -- edges going from the Case node to the CaseAlts
+		o    ← newEdge
+		void $ newNode Graph.Case {inp = p, out = o, alts = alts, names = map constr pats}
+		mapM_ (\(alt, (pat,exp)) → compile env alt (foldr Λ exp (vars pat))) (zip alts cases) -- compile the different cases
+		compile env o exp -- compile the scrutiny
 
+operator ∷ String → Edge → Maybe NodeLS
+operator name p = case name of
+	"+" → op 2 $ show . sum . map (read :: String → Int)
+	_ → Nothing
+	where op a f = Just Operator
+		{inp = p, ops = [], arity = a, lmop = 0, function = f, name = "+"}
+
 bindName ∷ Bool → String → Compiler (Edge, Name)
 bindName lambda sym = do
 	v ← newEdge
-	s ← newNode Multiplier {out = v, ins = []}
+	s ← newNode Multiplexer {out = v, ins = []}
 	let ref = do
 		e ← newEdge
 		modifyNode s $ \s → s {ins = e : ins s}
diff --git a/Rules.hs b/Rules.hs
--- a/Rules.hs
+++ b/Rules.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UnicodeSyntax, FlexibleContexts #-}
+{-# LANGUAGE UnicodeSyntax, FlexibleContexts, ScopedTypeVariables #-}
 module Rules where
 
 import Prelude.Unicode
@@ -7,19 +7,26 @@
 import GraphRewriting.Pattern
 import GraphRewriting.Pattern.InteractionNet
 import GraphRewriting.Graph.Read
-import Data.List (transpose)
+import GraphRewriting.Graph.Write
+import Data.List (transpose, elemIndex, delete)
+import Control.Applicative
+import Data.Monoid
+import Control.Monad
 
+import Data.Maybe (fromJust)
 
+
 compileShare ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 compileShare = do
-	Multiplier {out = o, ins = is} ← node
+	Multiplexer {out = o, ins = is} ← node
 	case is of
-		[ ] → replace0 [Node $ Eraser {inp = o}]
+		[ ] → replace $ byNode Eraser {inp = o}
 		[i] → rewire [[o,i]]
-		ins → let (ins1, ins2) = splitAt (length ins `div` 2) ins in replace2 $ \o1 o2 → 
-			[Node $ Duplicator {level = 0, inp = o, out1 = o1, out2 = o2},
-			 Node $ Multiplier {out = o1, ins = ins1},
-			 Node $ Multiplier {out = o2, ins = ins2}]
+		ins → let (ins1, ins2) = splitAt (length ins `div` 2) ins in replace $ do
+			(o1,o2) ← (,) <$> byEdge <*> byEdge
+			byNode $ Duplicator {level = 0, inp = o, out1 = o1, out2 = o2}
+			byNode $ Multiplexer {out = o1, ins = ins1}
+			byNode $ Multiplexer {out = o2, ins = ins2}
 
 withoutIdx ∷ [a] → Int → [a]
 withoutIdx xs i = let (ys,zs) = splitAt i xs in ys ⧺ tail zs
@@ -37,16 +44,21 @@
 commute ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 commute = do
 	n1 :-: n2 ← activePair
-	require (n1 ≢ n2)
-	let aux1 = inspect n1 `withoutIdx` pp n1
-	let aux2 = inspect n2 `withoutIdx` pp n2
+	require (n1 ≢ n2) -- TODO: replace by linear
+	let ports1 = inspect n1 ∷ [Port]
+	let ports2 = inspect n2 ∷ [Port]
+	let (pp1,pp1idx) = head [(p,i) | (p,i) ← ports1 `zip` [0..], p ≡ pp n1]
+	let (pp2,pp2idx) = head [(p,i) | (p,i) ← ports2 `zip` [0..], p ≡ pp n2]
+	let aux1 = pp1 `delete` inspect n1
+	let aux2 = pp2 `delete` inspect n2
 	let es1 = length aux1
 	let es2 = length aux2
-	replace (es1 * es2) $ \edges → let
-			edges1 = split es1 es2 edges
-			edges2 = transpose' es1 edges1
-		in [Node $ updateLevel n2 $ update (insertIdx (pp n1) pp1 auxs) n1 | (pp1,auxs) ← zip aux2 edges1]
-		 ⧺ [Node $ updateLevel n1 $ update (insertIdx (pp n2) pp2 auxs) n2 | (pp2,auxs) ← zip aux1 edges2]
+	replace $ do
+		edges ← replicateM (es1 * es2) byEdge
+		let edges1 = split es1 es2 edges
+		let edges2 = transpose' es1 edges1
+		mconcat [byNode $ updateLevel n2 $ update (insertIdx pp1idx pp1 auxs) n1 | (pp1,auxs) ← zip aux2 edges1]
+		mconcat [byNode $ updateLevel n1 $ update (insertIdx pp2idx pp2 auxs) n2 | (pp2,auxs) ← zip aux1 edges2]
 	where updateLevel you me = case me of
 		Duplicator {} → maybeLevelUp
 		Delimiter  {} → maybeLevelUp
@@ -59,9 +71,9 @@
 annihilate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 annihilate = do
 	n1 :-: n2 ← activePair
-	require (n1 ≡ n2)
-	let aux1 = inspect n1 `withoutIdx` pp n1
-	let aux2 = inspect n2 `withoutIdx` pp n2
+	require (n1 ≡ n2) -- TODO: ???
+	let aux1 = pp n1 `delete` inspect n1
+	let aux2 = pp n2 `delete` inspect n2
 	rewire $ [[a1,a2] | (a1,a2) ← aux1 `zip` aux2]
 
 annihilateDelimiters ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
@@ -70,20 +82,19 @@
 	Delimiter {} ← liftReader . inspectNode =<< previous
 	return rewrite
 
-eliminateDelimiter ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
-eliminateDelimiter = do
-	let
-		eraser = do
-			e@Eraser {} ← node
-			return e
-		constant = do
-			c@Constant {} ← node
-			return c
-	n ← eraser <|> constant
-	Delimiter {inp = iD} ← neighbour =<< previous
-	require (inp n ≢ iD)
-	replace0 [Node $ n {inp = iD}]
+-- This rule doesn't trigger for constants with arguments
+eliminateDelimiterConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
+eliminateDelimiterConstant = do
+	c@Constant {args = as, name = n} :-: Delimiter {inp = iD} <- activePair
+	require (inp c ≢ iD && as == [])
+	replace $ byNode $ Constant {inp = iD, args = [], name = n}
 
+eliminateDelimiterEraser ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
+eliminateDelimiterEraser = do
+	c@Eraser {} :-: Delimiter {inp = iD} <- activePair
+	require (inp c ≢ iD)
+	replace $ byNode $ Eraser {inp = iD}
+
 eliminateDuplicator ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 eliminateDuplicator = do
 	Eraser {inp = iE} ← node
@@ -107,17 +118,10 @@
 
 beta ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 beta = do
-	Abstractor {body = b, var = v} :-: Applicator {inp = ai, func = f, arg = a} ← activePair
-	replace0
-		[Node $ Delimiter {level = 0, inp = ai, out = b},
-		 Node $ Delimiter {level = 0, inp = a, out = v}]
-
-commuteDelimiterRed ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
-commuteDelimiterRed = do
-	rewrite ← commuteDelimiter
-	ports ← liftReader . inspectNode . (!!1) =<< history -- next to previous
-	require $ length (ports ∷ [Port]) ≤ 2
-	return rewrite
+	Applicator {inp = ai, func = f, arg = a} :-: Abstractor {body = b, var = v} ← activePair
+	replace $ do
+		byNode $ Delimiter {level = 0, inp = ai, out = b}
+		byNode $ Delimiter {level = 0, inp = a, out = v}
 
 commuteDelimiter ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 commuteDelimiter = do
@@ -127,17 +131,107 @@
 
 applyConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 applyConstant = do
-	Constant {name = n} :-: Applicator {inp = i, arg = a} ← activePair
-	replace0 [Node $ Function {inp = i, out = a, name = n}]
+	Applicator {inp = i, arg = a} :-: Constant {name = n, args = as} ← activePair
+	replace $ byNode $ Constant {inp = i, name = n, args = as ++ [a]}
 
-applyFunction ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
-applyFunction = do
-	Function {inp = i, name = fn} :-: Constant {name = cn} ← activePair
-	replace0 [Node $ Constant {inp = i, name = fn ⧺ " " ⧺ cn}]
+applyOperator ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
+applyOperator = do
+	Applicator {inp = i, arg = a} :-: Operator {ops = os, arity = ar, lmop = l, function = fn, name = n} ← activePair
+	require (ar > length os)
+	replace $ byNode $ Operator {inp = i, ops = os ++ [a], arity = ar, lmop = l, function = fn, name = n}
 
+-- TODO: Require that the lmoPort is not on one of the unreduced ports yet
+-- Do we only reduce operator args, if the operator has all args already?
+reduceOperatorArgs ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
+reduceOperatorArgs = do
+	o@(Operator {ops = os, lmop = lmo}) <- node
+	opid <- previous
+	let ports = inspect o :: [Port]
+	let lmoport = ports !! lmo
+	-- only change the lmo port if it is on top or if it is attached to a Constant
+	require (lmo == 0) <|> do {Constant {} <- nodeWith lmoport; return ()}
+	port <- branch os -- get a pattern that matches each port in os
+	-- we require that at least one node attached to the operator is not a constant
+	requireFailure $ do
+		Constant {} <- nodeWith port
+		return ()
+	-- we need to add one, since the input port is not part of os, but is part of the port numbering
+	let unreducedport = 1 + fromJust (elemIndex port os)
+	return $ do
+		updateNode opid (o {lmop = unreducedport})
+
+execOperator ∷ forall n. (View [Port] n, View NodeLS n) ⇒ Rule n
+execOperator = do
+	Operator {inp = i, ops = os, arity = ar, function = fn, name = n} <- node
+	opid <- previous
+	require (length os == ar)
+	-- check that all args are constants
+	argss ← forM os $ \o -> do
+			c@Constant {} <- adverse o opid
+			return c
+	replace $ byNode $ Constant {inp = i, args = [], name = fn (map name argss)}
+
+caseNode :: (View [Port] n, View NodeLS n) ⇒ Rule n
+caseNode = do
+	-- the order of constant and case here is important, otherwise strategies don't work
+	Case {inp = i, alts = alts, names = names} :-: Constant {name = n, args = as} <- activePair
+	let matchingport = alts !! (fromJust $ elemIndex n names)
+	let nn = length alts
+	let m = length as
+	-- We generate m new applicator nodes with m+1 new edges connecting them
+	if m > 0 then
+		replace $ do
+			es ← replicateM (m+1) byEdge
+			byWire matchingport (es !! 0) -- We merge the first new edge with the matching port from the Case node
+			byWire i (es !! m) -- We merge the last new edge with the input edge of the Case node
+			mconcat [byNode $ Applicator {inp = es !! (i+1), func = es !! i, arg = as !! i} | i <- [0..m-1]]
+			mconcat [byNode $ Eraser {inp = alts !! i} | i <- filter (/= fromJust (elemIndex n names)) [0..nn-1]]
+			 else do
+		replace $ do
+			byWire i matchingport -- Attach the alternative directly to the input of the case node
+			mconcat [byNode $ Eraser {inp = alts !! i} | i <- filter (/= fromJust (elemIndex n names)) [0..nn-1]]
+
 -- | Not the readback semantics as defined in the paper. Just a non semantics preserving erasure of all
 -- delimiters to make the graph more readable
 readback ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 readback = do
 	Delimiter {inp = i, out = o} ← node
 	rewire [[i,o]]
+
+-- getLmoPort ∷ (View [Port] n, LeftmostOutermost n) ⇒ Node → Pattern n Port
+-- getLmoPort n = do
+-- 	node ← liftReader $ readNode n
+-- 	let ports = inspect node
+-- 	case lmoPort node of
+-- 		Nothing → fail "Term is in WHNF"
+-- 		Just ix → return $ ports !! ix
+--
+-- moveControl :: (View [Port] n, View Control n, LeftmostOutermost n, View NodeLS n) => Rule n
+-- moveControl = do
+-- 	Control {stack = s} ← node
+-- 	control ← previous
+-- 	lmo1 ← getLmoPort control
+-- 	n ← branchNodes =<< liftReader . adverseNodes control =<< getLmoPort control
+-- 	return $ do
+-- 		updateNode control NoControl
+-- 		updateNode n (Control {stack = control : s})
+--
+-- leftmostOutermost :: (View [Port] n, View Control n, LeftmostOutermost n, View NodeLS n) => Rule n -> Rule n
+-- leftmostOutermost r = do
+-- 	rewrite <- r
+-- 	ns <- history -- we want the first node of the matching pattern
+-- 	let topnode = last ns
+-- 	Control {stack = s} ← liftReader $ inspectNode topnode
+-- 	return $ do
+-- 		updateNode topnode NoControl -- First we set the topnode to not be the control node any more
+-- 		oldNodes ← readNodeList
+-- 		rewrite -- then we perform the rewrite
+-- 		newNodes ← readNodeList
+-- 		let s' = intersect s newNodes -- only consider nodes for the control marker that exist
+-- 		if null s' -- even the topmost node has been replaced
+-- 			then do -- we assign the control marker to one of the newly created nodes
+-- 				let addedNodes = newNodes \\ oldNodes
+-- 				updateNode (head addedNodes) (Control {stack = []}) -- finally we set the previous node on the stack as the control node
+-- 			else do -- set the previous node on the stack as the control node
+-- 				updateNode (head s') (Control {stack = tail s'})
+--
diff --git a/Term.hs b/Term.hs
--- a/Term.hs
+++ b/Term.hs
@@ -3,73 +3,118 @@
 
 import Prelude.Unicode
 import Text.ParserCombinators.Parsec as Parsec
+	hiding (space, eof, notFollowedBy, anyChar, many, optional, (<|>))
 import Text.ParserCombinators.Parsec.IndentParser as Indent
 import Text.ParserCombinators.Parsec.Language
 import Text.ParserCombinators.Parsec.IndentParser.Token
-import Control.Monad (liftM)
+import qualified Text.ParserCombinators.Parsec.Token as T
+import Control.Monad
+import Data.Functor
+import Control.Applicative
 
 
+instance Applicative (GenParser s a) where
+	pure  = return
+	(<*>) = ap
+
+instance Alternative (GenParser s a) where
+	empty = mzero
+	(<|>) = mplus
+
+-- | The AST of a lambda expression
 data Λ = A Λ Λ            -- ^ application
-       | Λ String Λ       -- ^ abstraction
-       | V String         -- ^ variable
-       | L [(String,Λ)] Λ -- ^ let binding
+	| Λ String Λ           -- ^ abstraction
+	| L [(String,Λ)] Λ     -- ^ let binding
+	| Case Λ [(Pattern,Λ)] -- ^ case expression
+	| C String [Λ]         -- ^ constructor
 	deriving (Show,Eq,Ord)
 
-parse ∷ String → Λ
-parse str = either (error ∘ show) id (Indent.parse parser "(null)" str)
+-- | The LHS of a case expression. Numbers are parsed as strings.
+data Pattern = Pat {constr :: String, vars :: [String]} deriving (Show, Eq, Ord)
 
+testParser :: [tok] -> IndentParser tok () c -> c
+testParser str parser = either (error ∘ show) id (Indent.parse parser "(null)" str)
+
+parse :: [Char] -> Λ
+parse str = testParser str expression
+
 parseFile ∷ FilePath → IO Λ
-parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile parser
+parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile expression
 
-parser ∷ IndentCharParser st Λ
-parser = expression where
+expression ∷ IndentCharParser st Λ
+expression = flip label "expression" $ letBinding <|> caseExpr <|> application
 
-	expression = flip label "expression" $ application <|> letBinding
+application ∷ IndentCharParser st Λ
+application = foldl1 A <$> many1 (parenthetic <|> abstraction <|> variable <|> numeral)
 
-	application = liftM (foldl1 A) $ many1 $ choice [parenthetic, abstraction, variable]
+variable ∷ IndentCharParser st Λ
+variable = C <$> ident <*> pure []
 
-	parenthetic = parens haskell expression
+numeral ∷ IndentCharParser st Λ
+numeral = C <$> numeric <*> pure []
 
-	abstraction = flip label "abstraction" $ do
-		sym "λ" <|> sym "\\"
-		vars ← many1 ident
-		sym "." <|> sym "→" <|> sym "->"
-		body ← expression
-		return $ foldr Λ body vars
+numeric ∷ IndentCharParser st String
+numeric = either show show <$> naturalOrFloat haskell
 
-	variable = liftM V $ ident <|> liftM (either show show) (naturalOrFloat haskell)
+parenthetic ∷ IndentCharParser st Λ
+parenthetic = parens haskell expression
 
-	-- Ugly, but works. Keyword "in" terminates binding blocks and bindings. Allows empty lets
-	letBinding = flip label "let binding" $ do
-		keyword "let"
-		let parseBindings = do
-			e ← optionMaybe $ keyword "in" >> expression
-			case e of
-				Just je → return ([], Just je)
-				Nothing → do
-					(b,e) ← lineFold $ do
-						b ← binding
-						e ← optionMaybe $ keyword "in" >> expression
-						return (b,e)
-					case e of
-						Nothing → do
-							rec ← optionMaybe parseBindings
-							case rec of
-								Nothing → return ([b], Nothing)
-								Just (bs, me) → return (b:bs, me)
-						Just je → return ([b], Just je)
-		(binds, e) ← block parseBindings
+tokP :: T.TokenParser st
+tokP = T.makeTokenParser haskellDef
+
+caseExpr ∷ IndentCharParser st Λ
+caseExpr = flip label "case expression" $
+	Case <$> (keyword "case" *> expression <* keyword "of") <*> bracesOrBlock tokP patterns
+
+patterns :: IndentCharParser st [(Pattern, Λ)]
+patterns = semiOrNewLineSep tokP pattern
+
+arrow ∷ IndentCharParser st String
+arrow = sym "->" <|> sym "→"
+
+pattern :: IndentCharParser st (Pattern, Λ)
+pattern = (,) <$> lhs <*> (arrow *> expression) where
+	lhs = Pat <$> (ident <|> numeric) <*> many (ident <|> numeric)
+
+lambda ∷ IndentCharParser st String
+lambda = sym "λ" <|> sym "\\"
+
+abstraction ∷ IndentCharParser st Λ
+abstraction = flip label "abstraction" $
+	flip (foldr Λ) <$> (lambda *> many1 ident) <*> ((sym "." <|> arrow) *> expression)
+
+-- Ugly, but works. Keyword "in" terminates binding blocks and bindings. Allows empty lets
+letBinding ∷ IndentCharParser st Λ
+letBinding = flip label "let binding" $ do
+	let parseBindings = do
+		e ← optionMaybe $ keyword "in" *> expression
 		case e of
-			Nothing → liftM (L binds) (keyword "in" >> expression)
-			Just je → return $ L binds je
+			Just je → return ([], Just je)
+			Nothing → do
+				(b,e) ← lineFold $ (,) <$> binding <*> (optionMaybe $ keyword "in" *> expression)
+				case e of
+					Nothing → do
+						rec ← optionMaybe parseBindings
+						case rec of
+							Nothing → return ([b], Nothing)
+							Just (bs, me) → return (b:bs, me)
+					Just je → return ([b], Just je)
+	(binds, e) ← keyword "let" *> block parseBindings
+	case e of
+		Nothing → L binds <$> (keyword "in" *> expression)
+		Just je → return $ L binds je
 
-	binding ∷ IndentCharParser st (String,Λ)
-	binding = flip label "binding" $ do
-		funct  ← ident
-		params ← many ident
-		body   ← sym "=" >> expression
-		return (funct, foldr Λ body params)
+binding ∷ IndentCharParser st (String,Λ)
+binding = flip label "binding" $ do
+	funct ← ident
+	rhs ← flip (foldr Λ) <$> many ident <*> (sym "=" *> expression)
+	return (funct, rhs)
 
-	keyword = reserved haskell
-	ident = identifier haskell
-	sym = symbol haskell
+keyword :: String -> IndentCharParser st ()
+keyword = reserved haskell
+
+ident :: IndentCharParser st String
+ident = identifier haskell
+
+sym :: String -> IndentCharParser st String
+sym = symbol haskell
diff --git a/examples/case.l b/examples/case.l
new file mode 100644
--- /dev/null
+++ b/examples/case.l
@@ -0,0 +1,6 @@
+λx.case x of
+	Test -> 1
+	B y  -> y y
+	Cons x xs -> x xs
+	Bla       -> λy.y y
+(Cons 5 Nil)
diff --git a/examples/sum.l b/examples/sum.l
new file mode 100644
--- /dev/null
+++ b/examples/sum.l
@@ -0,0 +1,5 @@
+let
+	sum list = case list of
+		Nil -> 0
+		Cons z zs -> (\x.λy -> + x y) z (sum zs)
+in sum (Cons 1 Nil)
diff --git a/graph-rewriting-lambdascope.cabal b/graph-rewriting-lambdascope.cabal
--- a/graph-rewriting-lambdascope.cabal
+++ b/graph-rewriting-lambdascope.cabal
@@ -1,5 +1,5 @@
 Name:           graph-rewriting-lambdascope
-Version:        0.4.11
+Version:        0.5
 Copyright:      (c) 2010, Jan Rochel
 License:        BSD3
 License-File:   LICENSE
@@ -9,7 +9,7 @@
 Stability:      alpha
 Build-Type:     Simple
 Synopsis:       Implementation of Lambdascope as an interactive graph-rewriting system
-Description:    Lambdascope is an optimal implementation of the λβ-calculus described in the paper "Lambdascope - Another optimal implementation of the lambda-calculus" by Vincent van Oostrom, Kees-Jan van de Looij, and Marijn Zwitserlood. Call "lambdascope" with one of the files from the "examples" directory as an argument. For usage of the GUI see "GraphRewriting.GL.UI".
+Description:    Lambdascope is an optimal implementation of the λβ-calculus described in the paper "Lambdascope - Another optimal implementation of the lambda-calculus" by Vincent van Oostrom, Kees-Jan van de Looij, and Marijn Zwitserlood. Call "lambdascope" with one of the files from the "examples" directory as an argument. For usage of the GUI see "GraphRewriting.GL.UI". Use the "--lmo" flag for leftmost outermost evalution
 Category:       Graphs, Application
 Cabal-Version:  >= 1.6
 Data-Files:     examples/*.l
@@ -19,9 +19,10 @@
   Build-Depends:
     base >= 4 && < 4.5,
     base-unicode-symbols >= 0.2 && < 0.3,
-    graph-rewriting >= 0.4.4 && < 0.6,
-    graph-rewriting-layout >= 0.4.1 && < 0.5,
-    graph-rewriting-gl >= 0.6.7 && < 0.7,
+    graph-rewriting >= 0.7 && < 0.8,
+    graph-rewriting-layout >= 0.5.0 && < 0.6,
+    graph-rewriting-gl >= 0.6.9 && < 0.7,
+    graph-rewriting-strategies >= 0.2 && < 0.3,
     parsec >= 2.1 && < 2.2,
     GLUT >= 2.2 && < 2.3,
     OpenGL >= 2.4 && < 2.5,
@@ -31,5 +32,5 @@
     FlexibleInstances
     FlexibleContexts
     MultiParamTypeClasses
-  GHC-Options:    -fno-warn-duplicate-exports
+  GHC-Options:    -fno-warn-duplicate-exports -fwarn-unused-binds -fwarn-unused-imports -fwarn-unused-do-bind -fwarn-wrong-do-bind -fwarn-unrecognised-pragmas
   Other-Modules:   GL Graph Resolver Rules Term