#include <stdio.h>
#include <stdlib.h>

typedef struct node tree;
struct node {
    int data;
    tree *left;
    tree *right;
};

tree* insert(tree *t,int x){
    if(t==NULL) {
        t=(tree*)malloc(sizeof(tree));
        t->data = x;
        t->left=NULL;
        t->right=NULL;
    }
    else if(x<t->data)
       t->left = insert(t->left,x);
    else if(x>t->data)
       t->right = insert(t->right,x);
    return t;
}

/*@ 
logic integer max2(integer a, integer b) = (a>b)?a:b;
*/

/*@
axiomatic Depth {
logic integer depth(tree* t);
axiom base:
	depth(\null)==0;
axiom recursive:
	\forall tree* t;
	depth(t) == max2(depth(t->left)+1,depth(t->right)+1);
}
*/

/*@
ensures \result == depth(\old(t));
assigns \nothing;
*/
int maxdepth(tree* t) {
    if(t==NULL)
	return 0;
    else {
	int lheight = maxdepth(t->left)+1;
        int rheight = maxdepth(t->right)+1;
	return lheight>rheight?lheight:rheight;
    }
}

int main() {
    tree *t=NULL;
    /*int n,x;
    printf("Enter how many element in tree");
    scanf("%d",&n);
    for(int i=0;i<n;i++){
        scanf("%d",&x);
        t=insert(t,x);
    }*/
    //printf("%d",maxdepth(t));
}