--- a/src/parallel_execution/rb_tree.cbc	Tue Nov 15 17:53:40 2016 +0900
+++ b/src/parallel_execution/rb_tree.cbc	Tue Nov 15 19:02:36 2016 +0900
@@ -71,16 +71,13 @@
 }
 
 __code insertNode(struct Traverse* traverse, struct Node* node, struct Node* newNode) {
-    Stack* nodeStack = new Stack();
     *newNode = *node;
     newNode->color = Red;
     traverse->current = newNode;
-    nodeStack->stack = (union Data*)traverse->nodeStack;
-    nodeStack->next = insertCase1;
-    goto traverse->nodeStack->get2();
+    goto traverse->nodeStack->get2(traverse, tree, insertCase1);
 }
 
-__code insertCase1(struct Traverse* traverse, struct Tree* tree,struct Node *parent, struct Node *grandparent) {
+__code insertCase1(struct Node *parent, struct Node *grandparent, struct Traverse* traverse, struct Tree* tree)  {
     if (parent != NULL) {
         traverse->parent = parent;
         traverse->grandparent = grandparent;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parallel_execution/stack.agda	Tue Nov 15 19:02:36 2016 +0900
@@ -0,0 +1,16 @@
+module stack where
+
+pushSingleLinkedStack : Stack -> Data -> (Code : Stack -> ?) -> ?
+pushSingleLinkedStack stack data next = next stack1
+  where
+    element = record {next = top stack; data = data}
+    stack1  = record {top = just element}
+
+
+popSingleLinkedStack : Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
+popSingleLinkedStack stack data next with (top stack) =
+  ... | nothing = next stack nothing
+  ... | just a  = next stack1 data1
+    where
+      data1 = data a
+      stack1 = record { top = (next a)}

--- a/src/parallel_execution/stack.cbc	Tue Nov 15 17:53:40 2016 +0900
+++ b/src/parallel_execution/stack.cbc	Tue Nov 15 19:02:36 2016 +0900
@@ -38,6 +38,15 @@
     goto next(...);
 }
 
+
+
+/* Stack -> Data -> (Code : Stack -> ?) -> ?
+  pushSingleLinkedStack stack data next = next stack1
+    where
+       element = record {next = top stack; data = data}
+       stack1  = record {top = just element}
+*/
+
 __code pushSingleLinkedStack(struct SingleLinkedStack* stack,union Data* data, __code next(...)) {
     Element* element = new Element();
     element->next = stack->top;
@@ -46,6 +55,15 @@
     goto next(...);
 }
 
+/* Stack Maybe ?? -> Data -> (Code : Stack -> (Maybe ??) -> ?) -> ?
+  popSingleLinkedStack stack data next with (top stack) =
+  ... | nothing = next stack nothing
+  ... | just a  = next stack1 data1
+    where
+      data1 = data a
+      stack1 = record { top = (next a)}
+*/
+
 __code popSingleLinkedStack(struct SingleLinkedStack* stack, union Data** data, __code next(...)) {
     if (stack->top) {
         *data = stack->top->data;
@@ -73,6 +91,7 @@
     goto next(...);
 }
 
+
 __code getSingleLinkedStack(struct SingleLinkedStack* stack, union Data** data, __code next(...)) {
     if (stack->top)
         *data = stack->top->data;
@@ -81,19 +100,21 @@
     goto next(...);
 }
 
-__code get2SingleLinkedStack(struct SingleLinkedStack* stack, union Data** data, union Data** data1, __code next(...)) {
+__code get2SingleLinkedStack(struct SingleLinkedStack* stack,..., __code next(...)) {
+    union Data* data, *data1;
+
     if (stack->top) {
-        *data = stack->top->data;
+        data = stack->top->data;
         if (stack->top->next) {
-            *data1 = stack->top->next->data;
+            data1 = stack->top->next->data;
         } else {
-            *data1 = NULL;
+            data1 = NULL;
         }
     } else {
-        *data = NULL;
-        *data1 = NULL;
+        data = NULL;
+        data1 = NULL;
     }
-    goto next(...);
+    goto next(data, data1, ...);
 }
 
 __code isEmptySingleLinkedStack(struct SingleLinkedStack* stack, __code next(...), __code whenEmpty(...)) {