diff --git a/GL.hs b/GL.hs
--- a/GL.hs
+++ b/GL.hs
@@ -17,7 +17,6 @@
 		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
@@ -54,14 +53,7 @@
 			vertex2 (0,0.9)
 			vertex2 (-1,-0.5)
 			vertex2 (1,-0.5)
-		renderString $ show $ level node
-	Delimiter {} → 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)
-		renderString $ show $ level node
+		renderString $ label node
 	Case      {} → drawNode ("case [" ++ foldr1 (\x y → x ++ ", " ++ y) (names node) ++ "]")
 	Operator  {} → drawNode (name node)
 
diff --git a/Graph.hs b/Graph.hs
--- a/Graph.hs
+++ b/Graph.hs
@@ -15,18 +15,15 @@
 	| 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}
+	| Duplicator  {label ∷ String, inp, out1, out2 ∷ 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] → Maybe String, name ∷ String}
 
--- | equality as defined in the paper with only the relevant cases included
 instance Eq NodeLS where
-	Eraser     {}           == Eraser     {} = True
-	Duplicator {level = l1} == Duplicator {level = l2} = l1 ≡ l2
-	Delimiter  {level = l1} == Delimiter  {level = l2} = l1 ≡ l2
+	Eraser     {} == Eraser     {} = True
+	Duplicator {label = l1} == Duplicator {label = l2} = l1 ≡ l2
 	_ == _ = False
 
 instance View [Port] NodeLS where
@@ -37,7 +34,6 @@
 		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
@@ -48,7 +44,6 @@
 		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
@@ -64,7 +59,6 @@
 	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
@@ -79,6 +73,5 @@
 	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
@@ -93,9 +93,8 @@
 	[Leaf "Beta Reduction" beta,
 	 Branch "All but Beta"
 	 	[Leaf "Duplicate" duplicate,
-	 	 Leaf "Eliminate" (eliminateDelimiterEraser <|> eliminateDelimiterConstant <|> eliminateDuplicator),
+	 	 Leaf "Eliminate" eliminateDuplicator,
 	 	 Leaf "Annihilate" annihilate,
-	 	 Leaf "Commute Delimiter" commuteDelimiter,
 	 	 Leaf "Erase" eraser,
 		 Leaf "Case" caseNode,
 	 	 Branch "Primitive"
diff --git a/Resolver.hs b/Resolver.hs
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -44,12 +44,7 @@
 		[  ] → 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
+			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
diff --git a/Rules.hs b/Rules.hs
--- a/Rules.hs
+++ b/Rules.hs
@@ -24,7 +24,7 @@
 		[i] → rewire [[o,i]]
 		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 $ Duplicator {label = "", inp = o, out1 = o1, out2 = o2}
 			byNode $ Multiplexer {out = o1, ins = ins1}
 			byNode $ Multiplexer {out = o2, ins = ins2}
 
@@ -44,7 +44,7 @@
 commute ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 commute = do
 	n1 :-: n2 ← activePair
-	require (n1 ≢ n2) -- TODO: replace by linear
+	require (n1 ≢ n2)
 	let ports1 = inspect n1 ∷ [Port]
 	let ports2 = inspect n2 ∷ [Port]
 	let (pp1,pp1idx) = head [(p,i) | (p,i) ← ports1 `zip` [0..], p ≡ pp n1]
@@ -57,16 +57,8 @@
 		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
-		_ → me
-		where maybeLevelUp = case you of
-			Delimiter  {} → if level you ≤ level me then me {level = level me + 1} else me
-			Abstractor {} → me {level = level me + 1}
-			_ → me
+		mconcat [byNode $ update (insertIdx pp1idx pp1 auxs) n1 | (pp1,auxs) ← zip aux2 edges1]
+		mconcat [byNode $ update (insertIdx pp2idx pp2 auxs) n2 | (pp2,auxs) ← zip aux1 edges2]
 
 annihilate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 annihilate = do
@@ -76,25 +68,6 @@
 	let aux2 = pp n2 `delete` inspect n2
 	rewire $ [[a1,a2] | (a1,a2) ← aux1 `zip` aux2]
 
-annihilateDelimiters ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
-annihilateDelimiters = do
-	rewrite ← annihilate
-	Delimiter {} ← liftReader . inspectNode =<< previous
-	return rewrite
-
--- 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
@@ -111,23 +84,29 @@
 	return rewrite
 
 duplicate ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
-duplicate = do
-	rewrite ← commute
-	Duplicator {} ← liftReader . inspectNode =<< previous
-	return rewrite
+duplicate = duplicateAbstractor <|> duplicateSthElse where
+	duplicateAbstractor = do
+		Duplicator {label = l, inp = di, out1 = o1, out2 = o2}
+			:-: Abstractor {name = n, inp = ai, body = b, var = v} ← activePair
+		replace $ do
+			(b1,v1,b2,v2) ← (,,,) <$> byEdge <*> byEdge <*> byEdge <*> byEdge
+			byNode Abstractor {name = n ⧺ "1", inp = o1, body = b1, var = v1}
+			byNode Abstractor {name = n ⧺ "2", inp = o2, body = b2, var = v2}
+			byNode Duplicator {label = n, inp = b, out1 = b1, out2 = b2}
+			byNode Duplicator {label = n, inp = v, out1 = v1, out2 = v2}
+	duplicateSthElse = do
+		rewrite ← commute
+		Duplicator {} ← liftReader . inspectNode =<< previous
+		requireFailure $ do
+			h ← history
+			Abstractor {} ← liftReader $ inspectNode (h !! 1)
+			return ()
+		return rewrite
 
 beta ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 beta = do
 	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
-	rewrite ← commute
-	Delimiter {} ← liftReader . inspectNode =<< previous
-	return rewrite
+	rewire [[ai,b], [a,v]]
 
 applyConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 applyConstant = do
@@ -191,10 +170,3 @@
 		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]]
diff --git a/examples/2times2.l b/examples/2times2.l
new file mode 100644
--- /dev/null
+++ b/examples/2times2.l
@@ -0,0 +1,2 @@
+let two = λx. λy. x (x y)
+in two two
diff --git a/examples/WW-beta-saving-0.l b/examples/WW-beta-saving-0.l
new file mode 100644
--- /dev/null
+++ b/examples/WW-beta-saving-0.l
@@ -0,0 +1,1 @@
+(\F. (\f. f (f 0)) (F 0)) (\y. \x. x) 
diff --git a/examples/WW-beta-saving-1.l b/examples/WW-beta-saving-1.l
new file mode 100644
--- /dev/null
+++ b/examples/WW-beta-saving-1.l
@@ -0,0 +1,1 @@
+(\F. (\f. f (f 0)) (F (F 0 0))) (\y. \x. x) 
diff --git a/examples/asperti_guerrini_p14.l b/examples/asperti_guerrini_p14.l
new file mode 100644
--- /dev/null
+++ b/examples/asperti_guerrini_p14.l
@@ -0,0 +1,1 @@
+(λx. x (λi. i)) λy. (λd. d d) (y z)
diff --git a/examples/exp.l b/examples/exp.l
--- a/examples/exp.l
+++ b/examples/exp.l
@@ -1,14 +1,5 @@
 let
 	id    = λx.x
-	zero  = λf x. x
-	one   = λf x. f x
-	two   = λf x. f (f x)
+	two   = λg y. g (g y)
 	three = λf x. f (f (f x))
-	four  = λf x. f (f (f (f x)))
-	five  = λf x. f (f (f (f (f x))))
-	six   = λf x. f (f (f (f (f (f x)))))
-	seven = λf x. f (f (f (f (f (f (f x))))))
-	eight = λf x. f (f (f (f (f (f (f (f x)))))))
-	nine  = λf x. f (f (f (f (f (f (f (f (f x))))))))
-	ten   = λf x. f (f (f (f (f (f (f (f (f (f x)))))))))
-in (λx.x two two id id) four
+in three two two id id
diff --git a/examples/exp_simpl.l b/examples/exp_simpl.l
new file mode 100644
--- /dev/null
+++ b/examples/exp_simpl.l
@@ -0,0 +1,5 @@
+let
+	f x = let g y z = let h a = y (y a)
+	                  in h (h z)
+	      in g (g x)
+in f (f (λx.x)) (λx.x)
diff --git a/examples/lamping_p20r_qp.l b/examples/lamping_p20r_qp.l
new file mode 100644
--- /dev/null
+++ b/examples/lamping_p20r_qp.l
@@ -0,0 +1,3 @@
+(λx.(λy.((λf.((λh.(h(λp.(h(λq.p)))))
+              (λl.(((f(λn.(l n))) x) y))))
+         (λg.(λu.(λv.((g u) (g v))))))))
diff --git a/examples/lamping_p20r_qp_simpl.l b/examples/lamping_p20r_qp_simpl.l
new file mode 100644
--- /dev/null
+++ b/examples/lamping_p20r_qp_simpl.l
@@ -0,0 +1,4 @@
+let
+	s = λd. let t = λe. d e
+		in t (λco. λnst. co) (t (λk. λl. l))
+in s (λc. s (λx. c)) 2 3
diff --git a/examples/lamping_p20r_qq.l b/examples/lamping_p20r_qq.l
new file mode 100644
--- /dev/null
+++ b/examples/lamping_p20r_qq.l
@@ -0,0 +1,3 @@
+(λx.(λy.((λf.((λh.(h(λp.(h(λq.q)))))
+              (λl.(((f(λn.(l n))) x) y))))
+         (λg.(λu.(λv.((g u) (g v))))))))
diff --git a/examples/lamping_p20r_qq_simpl.l b/examples/lamping_p20r_qq_simpl.l
new file mode 100644
--- /dev/null
+++ b/examples/lamping_p20r_qq_simpl.l
@@ -0,0 +1,4 @@
+let
+	s = λd. let t = λe. d e
+		in t (λco. λnst. co) (t (λk. λl. l))
+in s (λc. s (λx. x)) 2 3
diff --git a/examples/lamping_simpl.l b/examples/lamping_simpl.l
--- a/examples/lamping_simpl.l
+++ b/examples/lamping_simpl.l
@@ -1,6 +1,5 @@
 let
-	id = λx.x
-	shared = λa. let
-			shared = λb. a (b id)
-		in shared (shared id)
-in shared (shared id)
+	h = λh. let
+			w = λw. h (w (λy.y))
+		in w (w (λz.z))
+in h (h (λx.x))
diff --git a/examples/levy-1988-p184bottom.l b/examples/levy-1988-p184bottom.l
new file mode 100644
--- /dev/null
+++ b/examples/levy-1988-p184bottom.l
@@ -0,0 +1,6 @@
+let I0    = \x0.x0
+    I1    = \x1.x1
+    J     = \z.b
+    Delta = \y.I1 (y y) 
+in (\f.(f I0)(f J)) (\x. Delta (x a))
+
diff --git a/examples/sum1.l b/examples/sum1.l
new file mode 100644
--- /dev/null
+++ b/examples/sum1.l
@@ -0,0 +1,5 @@
+let
+	Cons x xs = λcons nil. cons x xs
+	Nil = λcons nil. nil
+	sum list = list (λx xs . (λx y . Plus x y) x (sum xs)) 0
+in sum (Cons 1 Nil)
diff --git a/examples/vincent-0-ww.l b/examples/vincent-0-ww.l
new file mode 100644
--- /dev/null
+++ b/examples/vincent-0-ww.l
@@ -0,0 +1,3 @@
+let delta = \x. x x
+    Delta = (\y. y y) (\z. z z)
+in  delta Delta
diff --git a/examples/vincent-1-ww.l b/examples/vincent-1-ww.l
new file mode 100644
--- /dev/null
+++ b/examples/vincent-1-ww.l
@@ -0,0 +1,4 @@
+let G = \g. g (g x) 
+    F x = F x
+    I x = x 
+in  G (F I)
diff --git a/examples/wadsworth-thesis-p172.l b/examples/wadsworth-thesis-p172.l
new file mode 100644
--- /dev/null
+++ b/examples/wadsworth-thesis-p172.l
@@ -0,0 +1,2 @@
+let epsilon = (\f.f(f(f a)))((\x.\y.y x)b)
+in  epsilon
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.5.2
+Version:        0.5.3
 Copyright:      (c) 2010, Jan Rochel
 License:        BSD3
 License-File:   LICENSE
@@ -10,22 +10,22 @@
 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". Use the "--lmo" flag for leftmost outermost evalution and "--bench" for non-graphical evaluation to weak head normal form.
-Category:       Graphs, Application
+Category:       Compilers/Interpreters, Application
 Cabal-Version:  >= 1.6
 Data-Files:     examples/*.l
 
-Executable lambdascope
+Executable bad-context-sharing
   Main-Is:        Main.hs
   Build-Depends:
-    base >= 4 && < 4.5,
+    base >= 4 && < 4.6,
     base-unicode-symbols >= 0.2 && < 0.3,
     graph-rewriting >= 0.7.1 && < 0.8,
     graph-rewriting-layout >= 0.5.1 && < 0.6,
     graph-rewriting-gl >= 0.7.1 && < 0.8,
     graph-rewriting-strategies >= 0.2 && < 0.3,
-    parsec >= 2.1 && < 2.2,
-    GLUT >= 2.2 && < 2.3,
-    OpenGL >= 2.4 && < 2.5,
+    parsec >= 2.1 && < 3.2,
+    GLUT >= 2.2 && < 2.4,
+    OpenGL >= 2.4 && < 2.6,
     IndentParser >= 0.2 && < 0.3
   Extensions:
     UnicodeSyntax