class SearchTree {
    SearchTree left, right;
    int value;
    
    SearchTree() {
    }

    SearchTree(int v, SearchTree l, SearchTree r) 
    /*@SearchTree_pre@*/
    {
	value = v;
	left = l;
	right = r;
    }
    /*@SearchTree_post@*/

    boolean isEmpty() 
    /*@isEmpty_pre@*/
    {
	return (left == null) && (right == null);
    }
    /*@isEmpty_post@*/

    void insert(int v) 
    /*@insert_pre@*/
    {
	SearchTree current = this;
	while (!current.isEmpty()) {
	    if (v <= current.value) current = current.left;
	    else current = current.right;
	}
	current.value = v;
	current.left = new SearchTree();
	current.right = new SearchTree();
    }
    /*@insert_post@*/

    SearchTree findOrNil(int v) 
    /*@findOrNil_pre@*/
    {
	SearchTree current = this;
	while (!current.isEmpty() && (current.value != v)) {
	    if (v <= current.value) current = current.left;
	    else current = current.right;
	}
	SearchTree result = current.isEmpty() ? null: current;
	return result;
    }
    /*@findOrNil_post@*/

    SearchTree findMin() 
    /*@findMin_pre@*/
    {
	SearchTree parent = this;
	SearchTree current = this;
	while (!current.isEmpty()) {
	    parent = current;
	    current = current.left;
	}
	return parent;
    }
    /*@findMin_post@*/

    SearchTree findMax() 
    /*@findMax_pre@*/
    {
	SearchTree parent = this;
	SearchTree current = this;
	while (!current.isEmpty()) {
	    parent = current;
	    current = current.right;
	}
	return parent;
    }
    /*@findMax_post@*/

    void remove(int v) 
    /*@remove_pre@*/
    {
	SearchTree node = findOrNil(v);
	while (node != null) {
	    if (!node.left.isEmpty()) {
		SearchTree max = node.left.findMax();
//		node.value = max.value;
		node = node.left.findOrNil(max.value);
	    }
	    else if (!node.right.isEmpty()) {
		SearchTree min = node.right.findMin();
//		node.value = min.value;
		node = node.right.findOrNil(min.value);
	    }
	    else {
		node.value = 0;
		node.left = null;
		node.right = null;
		node = null;
	    }
	}
    }
    /*@remove_post@*/

    static void demo() 
    /*@demo_pre@*/
    {
	SearchTree t = new SearchTree();
	t.insert(3);
	t.insert(5);
	t.insert(2);
	t.insert(1);
	t.insert(2);
	t.insert(6);
	t.insert(4);  
        t.remove(5);
    }
    /*@demo_post@*/

    static void demo2(int e1, int e2, int e3, int e4,
		      int e5, int e6, int r1, int r2) 
    /*@demo2_pre@*/
    {
	SearchTree t = new SearchTree();
	t.insert(e1);
	t.insert(e2);
	t.insert(e3);
	t.insert(e4);
	t.insert(e5);
	t.remove(r1);
 	t.insert(e6);
	t.remove(r2);

	SearchTree max = t.findMax();
	SearchTree min = t.findMin();
	SearchTree el3 = t.findOrNil(e3);
	SearchTree rem = t.findOrNil(r1);
    }
    /*@demo2_post@*/
}