--- a/src/insert_verification/akashaLLRBContext.c	Mon Jun 13 01:35:37 2016 +0000
+++ b/src/insert_verification/akashaLLRBContext.c	Mon Jun 13 11:47:37 2016 +0900
@@ -107,7 +107,10 @@
     context->data[Iter] = context->heap;
     context->heap += sizeof(struct Iterator);
 
-    context->dataNum = Iter;
+    context->data[AkashaInfo] = context->heap;
+    context->heap += sizeof(struct AkashaInfo);
+
+    context->dataNum = AkashaInfo;
 
     struct Tree* tree = &context->data[Tree]->tree;
     tree->root = 0;

--- a/src/insert_verification/include/akashaLLRBContext.h	Mon Jun 13 01:35:37 2016 +0000
+++ b/src/insert_verification/include/akashaLLRBContext.h	Mon Jun 13 11:47:37 2016 +0900
@@ -62,6 +62,7 @@
     Tree,
     Node,
     Iter,
+    AkashaInfo,
 };
 
 struct Context {
@@ -126,4 +127,14 @@
         unsigned long iteratedPointDataNum;
         void*         iteratedPointHeap;
     } iterator;
+    struct AkashaInfo {
+        unsigned int minHeight;
+        unsigned int maxHeight;
+        struct AkashaNode* akashaNode;
+    } akashaInfo;
+    struct AkashaNode {
+        unsigned int       height;
+        struct Node*       node;
+        struct AkashaNode* nextAkashaNode;
+    } akashaNode;
 };

--- a/src/insert_verification/main.c	Mon Jun 13 01:35:37 2016 +0000
+++ b/src/insert_verification/main.c	Mon Jun 13 11:47:37 2016 +0900
@@ -101,7 +101,7 @@
 }
 
 __code verifySpecification_stub(struct Context* context) {
-    goto verifySpecification(context, &context->data[Tree]->tree, &context->data[Iter]->iterator);
+    goto verifySpecification(context, &context->data[Allocate]->allocate, &context->data[Tree]->tree, &context->data[AkashaInfo]->akashaInfo);
 }
 
 __code duplicateIterator_stub(struct Context* context) {

--- a/src/insert_verification/verifySpecification.c	Mon Jun 13 01:35:37 2016 +0000
+++ b/src/insert_verification/verifySpecification.c	Mon Jun 13 11:47:37 2016 +0900
@@ -1,6 +1,8 @@
 #include <stdio.h>
 #include "akashaLLRBContext.h"
 
+extern void allocator(struct Context*);
+
 /* C functions (TODO: convert to code segment) */
 
 unsigned int min_height(struct Node* node, unsigned int height) {
@@ -55,10 +57,87 @@
     goto meta(context, context->next);
 }
 
-__code verifySpecification(struct Context* context, struct Tree* tree, struct Iterator* iter) {
-    unsigned const int min_h = min_height(tree->root, 1);
-    unsigned const int max_h = max_height(tree->root, 1);
+__code getMinHeight_stub(struct Context* context) {
+    goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);
+}
+
+__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) {
+    const struct AkashaNode* akashaNode = akashaInfo->akashaNode;
+
+    if (akashaNode == NULL) {
+        goto getMaxHeight_stub(context);
+    }
+
+    const struct Node* node = akashaInfo->akashaNode->node;
+    if (node->left == NULL && node->right == NULL) {
+        if (akashaInfo->minHeight > akashaNode->height) {
+            akashaInfo->minHeight  = akashaNode->height;
+            akashaInfo->akashaNode = akashaNode->nextAkashaNode;
+            goto getMinHeight_stub(context);
+        }
+    }
+
+    akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode;
+
+    if (node->left != NULL) {
+        allocate->size = sizeof(struct AkashaNode);
+        allocator(context);
+        struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum];
+        left->height           = akashaNode->height+1;
+        left->node             = node->left;
+        left->nextAkashaNode   = akashaInfo->akashaNode;
+        akashaInfo->akashaNode = left;
+    }
 
+    if (node->right != NULL) {
+        allocate->size = sizeof(struct AkashaNode);
+        allocator(context);
+        struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum];
+        right->height            = akashaNode->height+1;
+        right->node              = node->right;
+        right->nextAkashaNode    = akashaInfo->akashaNode;
+        akashaInfo->akashaNode   = right;
+    }
+
+    goto getMinHeight_stub(context);
+}
+
+__code getMaxHeight_stub(struct Context* context) {
+    goto getMaxHeight(context);
+}
+__code getMaxHeight(struct Context* context) {
+    goto verifySpecificationFinish(context);
+}
+
+__code verifySpecification(struct Context* context, struct Allocate* allocate, struct Tree* tree, struct AkashaInfo* akashaInfo) {
+    akashaInfo->minHeight = -1;
+    akashaInfo->maxHeight = 0;
+
+    if (tree->root == NULL) {
+        goto verifySpecificationFinish(context);
+    }
+
+    allocate->size = sizeof(struct AkashaNode);
+    allocator(context);
+    akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
+
+    akashaInfo->akashaNode->height = 1;
+    akashaInfo->akashaNode->node   = tree->root;
+
+
+    //unsigned const int max_h = max_height(tree->root, 1);
+
+    goto getMinHeight_stub(context);
+}
+
+__code verifySpecificationFinish(struct Context* context) {
+
+    printf(">>>>>>>>>>\n");
+    printTree(context->data[Tree]->tree.root, 0);
+    printf("%d\n", context->data[AkashaInfo]->akashaInfo.minHeight);
+    printf("<<<<<<<<<<\n");
+
+    /*
     if (max_h > 2*min_h) {
         printf("llrb-condition violated.\n");
         printf("\tmin-height %u\n", min_h);
@@ -67,6 +146,6 @@
         context->next = Exit;
         goto meta(context, ShowTrace);
     }
-
+    */
     goto meta(context, DuplicateIterator);
 }