diff --git a/test/concurrent/templates/give-up-lock_wip.rav b/test/concurrent/templates/give-up-lock_wip.rav
index 652eeb7..a51e233 100644
--- a/test/concurrent/templates/give-up-lock_wip.rav
+++ b/test/concurrent/templates/give-up-lock_wip.rav
@@ -24,12 +24,12 @@ interface SearchStructureSpec {
 
   type Op = data { case searchOp ; case insertOp ; case deleteOp }
 
-	pred opSpec(op: Op, k: K, c_in: Set[K], c_out: Set[K], res: Bool) {
+	func opSpec(op: Op, k: K, c_in: Set[K]) returns (c_out_res: (Set[K], Bool)) {
     op == searchOp() ? 
-      c_in == c_out && res == (k in c_in) :
+      ((c_in, (k in c_in))) :
     (op == insertOp() ?
-      c_out == c_in ++ {| k |} && res == (k !in c_in) :
-      c_out == c_in -- {| k |} && res == (k in c_in))
+      ((c_in ++ {| k |}, (k !in c_in))) :
+      ((c_in -- {| k |}, (k in c_in))))
 	}
 }
 
@@ -89,7 +89,7 @@ interface NodeImpl {
     requires k in keyset(i_n)
     requires node(n, c, i_n)
     ensures node(n, c1, i_n)
-    ensures succ ==> opSpec(dop, k, c, c1, res) 
+    ensures succ ==> opSpec(dop, k, c) == ((c1, res)) 
     ensures !succ ==> c == c1
 
   proc findNext(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
@@ -173,63 +173,62 @@ interface GiveUpTemplate[Node: NodeImpl, LockF: Lock] {
     own(r.authSet, AuthSetRef.frag(SetRefRA.set_constr({|n|})) )
   }
 
-  pred cssR(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int]) {
+  pred cssR(r: Ref, c: Set[K], g_i: Flow_K) {
     (forall n: Ref :: n in g_i.dom ==> 
-      (exists l: Ref ::
-        L.is_lock(l, (r, n), lockval[n] == 1) && own(n.lock, l, 1.0)))
-        && 
-    globalRes(r, c, g_i)
+      (exists l: Ref, b: Bool ::
+        own(n.lock, l, 1.0) && L.is_lock(l, (r, n), b)))
+    && globalRes(r, c, g_i)
   }
 
   pred css(r: Ref, c: Set[K]) {
-    exists g_i: Flow_K, lockval: Map[Ref, Int] :: 
-      cssR(r, c, g_i, lockval)
+    exists g_i: Flow_K :: 
+      cssR(r, c, g_i)
   }
 
-  lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int])
-    requires cssR(r, c, g_i, lockval)
+  lemma cssInFp(r: Ref, n:Ref, c: Set[K], g_i: Flow_K)
+    requires cssR(r, c, g_i)
     requires inFP(r, n)
     ensures n in g_i.dom
-    ensures cssR(r, c, g_i, lockval)
+    ensures cssR(r, c, g_i)
     ensures inFP(r, n)
   {
-    unfold cssR(r, c, g_i, lockval);
+    unfold cssR(r, c, g_i);
     unfold globalRes(r, c, g_i);
     unfold inFP(r, n);
 
     fold globalRes(r, c, g_i);
     fold inFP(r, n);
-    fold cssR(r, c, g_i, lockval);
+    fold cssR(r, c, g_i);
   }
 
 
-  lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int])
-    requires cssR(r, c, g_i, lockval)
+  lemma fpInCss(r: Ref, n:Ref, c: Set[K], g_i: Flow_K)
+    requires cssR(r, c, g_i)
     requires n in g_i.dom
     ensures inFP(r, n)
-    ensures cssR(r, c, g_i, lockval)
+    ensures cssR(r, c, g_i)
   {
-    unfold cssR(r, c, g_i, lockval);
+    unfold cssR(r, c, g_i);
     unfold globalRes(r, c, g_i);
 
     fpu(r, authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom)), AuthSetRef.auth_frag(SetRefRA.set_constr(g_i.dom), SetRefRA.set_constr(g_i.dom)));
 
     fold globalRes(r, c, g_i);
     fold inFP(r, n);
-    fold cssR(r, c, g_i, lockval);
+    fold cssR(r, c, g_i);
   }
 
-  lemma root_fp(r: Ref, c: Set[K], g_i: Flow_K, lockval: Map[Ref, Int])
-    requires cssR(r, c, g_i, lockval)
-    ensures cssR(r, c, g_i, lockval)
+  lemma root_fp(r: Ref, c: Set[K], g_i: Flow_K)
+    requires cssR(r, c, g_i)
+    ensures cssR(r, c, g_i)
     ensures r in g_i.dom
   {
-    unfold cssR(r, c, g_i, lockval);
+    unfold cssR(r, c, g_i);
     unfold globalRes(r, c, g_i);
     unfold globalinv(g_i, r);
 
     fold globalinv(g_i, r);
     fold globalRes(r, c, g_i);
-    fold cssR(r, c, g_i, lockval);
+    fold cssR(r, c, g_i);
   }
 }
\ No newline at end of file
diff --git a/test/concurrent/templates/give-up-simplified.rav b/test/concurrent/templates/give-up-simplified.rav
new file mode 100644
index 0000000..7678609
--- /dev/null
+++ b/test/concurrent/templates/give-up-simplified.rav
@@ -0,0 +1,549 @@
+include "./flows_ra.rav"
+include "./ccm_instances.rav"
+include "./keyset_ra.rav"
+
+import Library.Type
+import Library.CancellativeResourceAlgebra
+
+interface Keyspace {
+  rep type T
+
+  val ks: Set[T]
+}
+
+module IntKeyspace : Keyspace {
+  rep type T = Int
+
+  val ks: Set[T] = {| k: Int :: true |}
+}
+
+interface SearchStructureSpec {
+  type K
+  val keyspace: Set[K]
+
+  type Op = data { case searchOp ; case insertOp ; case deleteOp }
+
+	func opSpec(op: Op, k: K, c_in: Set[K]) returns (c_out_res: (Set[K], Bool)) {
+    op == searchOp() ? 
+      ((c_in, (k in c_in))) :
+    (op == insertOp() ?
+      ((c_in ++ {| k |}, (k !in c_in))) :
+      ((c_in -- {| k |}, (k in c_in))))
+	}
+}
+
+interface NodeImpl {
+
+  module Spec : SearchStructureSpec
+  import Spec._
+
+  module K_Type : Library.Type {
+    rep type T = K
+  }
+
+  module Multiset_K = Multiset[K_Type]
+  module Flow_K = FlowsRA[Multiset_K]
+
+  import Flow_K._
+  import Multiset_K.elem
+
+  pred node(n: Ref; c: Set[K], flow_int: Flow_K)
+
+  func inset(i: Flow_K.T, n: Ref) returns (ret: Set[K])
+  {
+    {| k : K :: (i.inf[n])[k] > 0 |}
+  }
+
+  func insets(i: Flow_K.T) returns (ret: Set[K])
+  {
+    {| k : K :: exists n: Ref :: n in i.dom && k in inset(i, n) |}
+  }
+
+  func outset(i: Flow_K.T, n: Ref) returns (ret: Set[K])
+  {
+    {| k : K :: (i.out[n])[k] > 0 |}
+  }
+
+  func outsets(i: Flow_K.T) returns (ret: Set[K])
+  {
+    {| k: K :: exists n: Ref :: {outset(i,n)} n !in i.dom && k in outset(i,n) |}
+  }
+
+  func keyset(i: Flow_K.T) returns (ret: Set[K])
+  {
+    insets(i) -- outsets(i)
+  }
+
+  proc createRoot()
+    returns (r: Ref)
+    ensures node(r, {||}, 
+    Flow_K.int({| l:Ref :: l == r ? Multiset_K.fromSet(keyspace) : Multiset_K.id |}, zeroFlow, {| r |}))
+
+  proc decisiveOp(dop: Op, n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
+    returns (succ: Bool, res: Bool, implicit ghost c1: Set[K])
+    requires k in keyset(i_n)
+    requires node(n, c, i_n)
+    ensures node(n, c1, i_n)
+    ensures succ ==> opSpec(dop, k, c) == ((c1, res)) 
+    ensures !succ ==> c == c1
+
+  proc findNext(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
+    returns (ret: Bool, n1: Ref)
+    requires k in inset(i_n, n)
+    requires node(n, c, i_n)
+    ensures node(n, c, i_n) && 
+      (ret ?   
+        k in outset(i_n, n1) :
+        k !in outsets(i_n))
+
+  proc inRange(n: Ref, k: K, implicit ghost c: Set[K], implicit ghost i_n: Flow_K)
+    returns (ret: Bool)
+    requires node(n, c, i_n)
+    ensures node(n, c, i_n) && (ret ==> k in inset(i_n, n))
+
+
+  lemma nodeSepStar(n: Ref, implicit ghost c1: Set[K], implicit ghost c2: Set[K], implicit ghost i_n1: Flow_K, implicit ghost i_n2: Flow_K)
+    requires node(n, c1, i_n1) && node(n, c2, i_n2)
+    ensures false
+}
+
+interface SearchStructure {
+   module Spec: SearchStructureSpec
+   import Spec._
+
+   pred css(r: Ref; c: Set[K])
+
+   proc create()
+     returns (r: Ref)
+     ensures css(r, {||})
+
+    proc cssOp(dop: Op, r: Ref, k: K, implicit ghost c: Set[K])
+      returns (res: Bool, implicit ghost cc: Set[K])
+      requires k in keyspace
+      atomic requires css(r, c)
+      atomic ensures css(r, cc) && opSpec(dop, k, c) == ((cc, res))
+}
+
+
+interface GiveUpTemplate[Node: NodeImpl] {
+  module Spec: SearchStructureSpec = Node.Spec
+  import Node.Spec._
+  import Node._
+  import Node.Flow_K._
+  import Node.Multiset_K.elem
+  import Node.Multiset_K.fromSet
+
+  module Ref_Type : Library.Type {
+    rep type T = Ref
+  }
+
+  module SetRefRA = Library.SetRA[Ref_Type]
+
+  module AuthSetRef = Library.Auth[SetRefRA]
+    
+  module Keyset_K = KeysetRA[K_Type]
+  module AuthKeyset_K = Library.Auth[Keyset_K]
+  module AuthFlow_K = Library.Auth[Flow_K]
+
+  ghost field authSet: AuthSetRef
+  ghost field authKS: AuthKeyset_K
+  ghost field authFlow: AuthFlow_K
+  field lock: Bool
+
+  func globalinv(g_i: Flow_K, r: Ref) returns (res: Bool) 
+  {
+      Flow_K.valid(g_i) &&
+      r in g_i.dom &&
+      outsets(g_i) == {||} &&
+      inset(g_i, r) == keyspace  
+  }
+
+  pred globalRes(r: Ref; c: Set[K], g_i: Flow_K) {
+    own(r.authKS, AuthKeyset_K.auth( Keyset_K.prodKS( keyspace, c ))) &&
+    own(r.authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom))) && 
+    own(r.authFlow, AuthFlow_K.auth(g_i)) &&
+    globalinv(g_i, r)
+  }
+
+  pred nodePred(r: Ref, n: Ref; c: Set[K], i_n: Flow_K) {
+    own(r.authKS, AuthKeyset_K.frag( Keyset_K.prodKS( keyset(i_n), c ) )) &&
+    own(r.authFlow, AuthFlow_K.frag(i_n)) &&
+    i_n.dom == {|n|} && 
+    node(n, c, i_n)
+  }
+
+  pred inFP(r: Ref, n: Ref) {
+    own(r.authSet, AuthSetRef.frag(SetRefRA.set_constr({|n|})) )
+  }
+
+  pred cssR(r: Ref; c: Set[K], g_i: Flow_K) {
+      globalRes(r, c, g_i) &&
+      (forall n: Ref :: n in g_i.dom ==> 
+        (exists b: Bool, cn: Set[K], intfn: Flow_K ::
+          own(n.lock, b, 1.0) && (b ? true : nodePred(r, n, cn, intfn))))
+  }
+
+  pred css(r: Ref; c: Set[K]) {
+    exists g_i: Flow_K :: cssR(r, c, g_i)
+  }
+
+  proc lockNode(n: Ref, implicit ghost b: Bool)
+    atomic requires own(n.lock, b, 1.0)
+    atomic ensures own(n.lock, true, 1.0) && b == false
+
+  proc unlockNode(n: Ref)
+    atomic requires own(n.lock, true, 1.0)
+    atomic ensures own(n.lock, false, 1.0)
+
+  proc lockNodeHigh(r: Ref, n: Ref, implicit ghost c: Set[K])
+    returns (ghost c_n : Set[K], ghost i_n: Flow_K)
+    requires inFP(r, n)
+    atomic requires css(r, c)
+    atomic ensures css(r, c) && nodePred(r, n, c_n, i_n) && inFP(r, n)
+  {
+    ghost var phi: AtomicToken := bindAU();
+
+    ghost var g_i0: Flow_K;
+    
+    ghost val c0: Set[K] := openAU(phi);
+    unfold css(r, c0);
+    cssInFp(r, n, c0);
+
+    unfold cssR(r);
+
+    lockNode(n);
+    c_n, i_n :| nodePred(r, n, c_n, i_n);
+    fold cssR(r, c0);
+    fold css(r, c0);
+
+    commitAU(phi, c_n, i_n);
+  }
+
+  proc unlockNodeHigh(r: Ref, n: Ref, ghost c_n: Set[K], ghost i_n: Flow_K, implicit ghost c: Set[K])
+    requires inFP(r, n)
+    requires nodePred(r, n, c_n, i_n)
+    atomic requires css(r, c)
+    atomic ensures css(r, c) && inFP(r, n)
+  {
+    ghost var phi: AtomicToken := bindAU();
+
+    ghost var g_i1: Flow_K;
+    
+    ghost val c1: Set[K] := openAU(phi);
+    unfold css(r, c1);
+    cssInFp(r, n, c1);
+    
+    unfold cssR(r, c1);
+    
+    {!
+      ghost var b: Bool;
+      b :| own(n.lock, b, 1.0);
+      if (!b) {
+        unfold nodePred(r, n, c_n, i_n);
+        unfold nodePred(r, n, c_n, i_n);
+        Node.nodeSepStar(n);
+      }
+    !}
+
+    unlockNode(n);    
+    fold cssR(r, c1, g_i1);
+    assert cssR(r, c1, g_i1);
+    fold css(r, c1);
+
+    commitAU(phi);
+  }
+  
+  
+  lemma cssInFp(r: Ref, n:Ref, c: Set[K], implicit ghost g_i: Flow_K)
+    requires cssR(r, c, g_i)
+    requires inFP(r, n)
+    ensures n in g_i.dom
+    ensures cssR(r, c, g_i)
+    ensures inFP(r, n)
+  {
+    unfold cssR(r, c, g_i);
+    unfold globalRes(r, c, g_i);
+    unfold inFP(r, n);
+
+    fold globalRes(r, c, g_i);
+    fold inFP(r, n);
+    fold cssR(r, c, g_i);
+  }
+
+
+  lemma fpInCss(r: Ref, n:Ref, c: Set[K], implicit ghost g_i: Flow_K)
+    requires cssR(r, c, g_i)
+    requires n in g_i.dom
+    ensures inFP(r, n)
+    ensures cssR(r, c, g_i)
+  {
+    unfold cssR(r, c, g_i);
+    unfold globalRes(r, c, g_i);
+
+    fpu(r, authSet, AuthSetRef.auth(SetRefRA.set_constr(g_i.dom)), AuthSetRef.auth_frag(SetRefRA.set_constr(g_i.dom), SetRefRA.set_constr(g_i.dom)));
+
+    fold globalRes(r, c, g_i);
+    fold inFP(r, n);
+    fold cssR(r, c, g_i);
+  }
+
+  lemma root_fp(r: Ref, c: Set[K], implicit ghost g_i: Flow_K)
+    requires cssR(r, c, g_i)
+    ensures cssR(r, c, g_i)
+    ensures r in g_i.dom
+  {
+    unfold cssR(r, c, g_i);
+    unfold globalRes(r, c, g_i);
+    
+    fold globalRes(r, c, g_i);
+    fold cssR(r, c, g_i);
+  }
+
+  proc create()
+    returns (r: Ref)
+    ensures css(r, {||})
+  {
+    r := Node.createRoot();
+
+    var i_r: Flow_K := int(
+        {| l:Ref :: l == r ? fromSet(keyspace) : fromSet({||})  |},
+        zeroFlow(),
+        {|r|}
+      );
+    var contents: Map[Ref, Set[K]] := {| l: Ref :: {||} |};
+    var lockval: Map[Ref, Int] := {| l: Ref :: 0 |};
+    var intf: Map[Ref, Flow_K] := {| l: Ref :: l == r ? i_r : Flow_K.id |};
+
+    r := new(
+      authKS: AuthKeyset_K.auth_frag(
+        Keyset_K.prodKS(keyspace, {||}),
+        Keyset_K.prodKS(keyspace, {||})
+      ),
+      authSet:AuthSetRef.auth(SetRefRA.set_constr({|r|})),
+      authFlow: AuthFlow_K.auth_frag(
+        i_r, i_r
+      ),
+      lock:false
+    );
+
+    fold nodePred(r, r, {||}, i_r);
+
+    fold globalRes(r, {||}, i_r);
+    fold cssR(r, {||}, i_r);
+    assert cssR(r, {||}, i_r);
+    fold css(r, {||});
+  }
+
+  lemma fpInStep(r: Ref, n: Ref, n1: Ref, k: K, c: Set[K], c_n: Set[K], i_n: Flow_K, implicit ghost g_i: Flow_K)
+    requires cssR(r, c, g_i)
+    requires nodePred(r, n, c_n, i_n)
+    requires k in outset(i_n, n1)
+    requires n in g_i.dom
+    ensures cssR(r, c, g_i)
+    ensures nodePred(r, n, c_n, i_n)
+    ensures n1 in g_i.dom
+  {
+    if (n1 !in g_i.dom) {
+      unfold cssR(r, c, g_i);
+      unfold nodePred(r, n, c_n, i_n);
+
+      unfold globalRes(r, c, g_i);
+      
+      ghost var i_o: Flow_K = Flow_K.frame(g_i, i_n);
+      
+      assert i_o.out[n1] == Multiset_K.frame(g_i.out[n1], i_n.out[n1]);
+      assert k !in outset(g_i, n1);
+      
+      fold nodePred(r, n, c_n, i_n);
+      fold globalRes(r, c, g_i);
+      fold cssR(r, c, g_i);
+    }
+  }
+
+  proc traverse(r: Ref, n: Ref, k: K, implicit ghost c: Set[K])
+    returns (nn: Ref, ghost cnn: Set[K], ghost i_nn: Flow_K)
+    requires inFP(r, n)
+    atomic requires css(r, c)
+    atomic ensures css(r, c)
+    ensures nodePred(r, nn, cnn, i_nn)
+    ensures inFP(r, nn)
+    ensures k in keyset(i_nn)
+  {
+    ghost val phi: AtomicToken := bindAU();
+        
+    ghost var c_n: Set[K];
+    ghost var i_n: Flow_K;
+    
+    ghost val c0: Set[K] := openAU(phi);
+    c_n, i_n := lockNodeHigh(r, n, c0);
+    abortAU(phi);
+    
+    unfold nodePred(r, n, c_n, i_n);
+    
+    var in_range: Bool := Node.inRange(n, k, c_n, i_n);
+
+    if (in_range) {
+      var succ: Bool;
+      var n1: Ref;
+      succ, n1 := Node.findNext(n, k, c_n, i_n);
+
+      fold nodePred(r, n, c_n, i_n);
+
+      if (succ) {
+        
+        ghost val c1: Set[K] := openAU(phi);
+        unfold css(r, c1);
+        
+        cssInFp(r, n, c1);
+        fpInStep(r, n, n1, k, c1, c_n, i_n);
+        fpInCss(r, n1, c1);
+
+        fold css(r, c1);
+
+        unlockNodeHigh(r, n, c_n, i_n, c1);
+
+        abortAU(phi);
+
+        ghost val c2: Set[K] := openAU(phi);
+
+        nn, cnn, i_nn := traverse(r, n1, k, c2);
+
+        commitAU(phi, nn, cnn, i_nn);
+        return nn, cnn, i_nn;
+      } else {
+        ghost val c0: Set[K] := openAU(phi);
+        unlockNodeHigh(r, n, c_n, i_n, c0);
+        abortAU(phi);
+       
+        ghost val c1: Set[K] := openAU(phi);
+
+        commitAU(phi, n, c_n, i_n);
+        return n, c_n, i_n;
+      }
+    } else {
+
+      fold nodePred(r, n, c_n, i_n);
+
+      ghost val c0: Set[K] := openAU(phi);
+      unlockNodeHigh(r, n, c_n, i_n, c0);
+      abortAU(phi);
+     
+      ghost val c1: Set[K] := openAU(phi);
+
+      unfold css(r, c1);
+
+      unfold cssR(r, c1);
+      unfold globalRes(r, c1);
+      
+      fold globalRes(r, c1);
+      fold cssR(r, c1);
+
+      fpInCss(r, r, c1);
+      
+      fold css(r, c1);
+      nn, cnn, i_nn := traverse(r, r, k, c1);
+
+      commitAU(phi, nn, cnn, i_nn);
+    }
+  }
+
+  lemma keyset_theorem(r: Ref, dop: Op, k: K, c_n: Set[K], c_n1: Set[K], c: Set[K], res: Bool, k_n: Set[K])
+    returns (c1: Set[K])
+    requires opSpec(dop, k, c_n) == ((c_n1, res))
+    requires own(r.authKS, AuthKeyset_K.auth(Keyset_K.prodKS(keyspace, c)))
+    requires own(r.authKS, AuthKeyset_K.frag(Keyset_K.prodKS(k_n, c_n)))
+    requires c_n1 subseteq k_n
+    requires k in k_n
+    requires k in keyspace
+
+    ensures opSpec(dop, k, c) == ((c1, res))
+    ensures own(r.authKS, AuthKeyset_K.auth(Keyset_K.prodKS(keyspace, c1)))
+    ensures own(r.authKS, AuthKeyset_K.frag(Keyset_K.prodKS(k_n, c_n1)))
+  {
+    if (dop == searchOp || !res) {
+      c1 := c;
+    } else {
+      if (dop == insertOp) {
+        c1 := c ++ {| k |};
+      } else {
+        c1 := c -- {| k |};
+      }
+        
+      fpu(r, authKS, 
+        AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c), Keyset_K.prodKS(k_n, c_n)),
+        AuthKeyset_K.auth_frag(Keyset_K.prodKS(keyspace, c1), Keyset_K.prodKS(k_n, c_n1)));
+    }
+  }
+
+  proc cssOp(dop: Op, r: Ref, k: K, implicit ghost c: Set[K])
+    returns (res: Bool, implicit ghost cc: Set[K])
+    requires k in keyspace
+    atomic requires css(r, c)
+    atomic ensures css(r, cc) && opSpec(dop, k, c) == ((cc, res))
+  {
+    ghost val phi: AtomicToken := bindAU();
+
+    var n: Ref;
+    var c_n: Set[K];
+    var i_n: Flow_K;
+    
+    ghost val c0: Set[K] := openAU(phi);
+    unfold css(r, c0);
+
+    root_fp(r, c0);
+    fpInCss(r, r, c0);
+    fold css(r, c0);
+    
+    n, c_n, i_n := traverse(r, r, k, c0);
+
+    abortAU(phi);
+
+    var succ: Bool;
+    var c_n1: Set[K];
+
+    unfold nodePred(r, n, c_n, i_n);
+    
+    succ, res, c_n1 := Node.decisiveOp(dop, n, k, c_n, i_n);
+    if (succ) {
+
+      ghost val c1: Set[K] := openAU(phi);
+      unfold css(r, c1);
+      cssInFp(r, n, c1);
+      unfold cssR(r, c1);
+      
+      {!
+        ghost var b: Bool;
+        b :| own(n.lock, b, 1.0); 
+        if (!b) {
+          unfold nodePred(r, n, c_n1, i_n);
+          Node.nodeSepStar(n);
+        }
+      !}
+
+      unlockNode(n);
+
+      unfold globalRes(r, c1);
+      cc := keyset_theorem(r, dop, k, c_n, c_n1, c1, res, keyset(i_n));      
+      fold globalRes(r, cc);
+      
+      fold nodePred(r, n, c_n1, i_n);
+      fold cssR(r, cc);
+      fold css(r, cc);
+
+      commitAU(phi, res, cc);
+
+      return res, cc;
+    } else {
+      fold nodePred(r, n, c_n, i_n);
+      ghost val c0: Set[K] := openAU(phi);
+      unlockNodeHigh(r, n, c_n, i_n, c0);
+      abortAU(phi);
+      
+      ghost val c1: Set[K] := openAU(phi);
+      res, cc := cssOp(dop, r, k, c1);
+      commitAU(phi, res, cc);
+      
+      return res, cc;
+    }
+  }
+}
\ No newline at end of file