import java.io.*;
import java.util.HashMap;

public class Heap {
    private /*@ spec_public @*/ /*@ rep rep @*/ HeapElem[] elems;
    private /*@ spec_public @*/ int numElems;

    public Heap() {
	elems = new /*@ rep rep @*/ HeapElem[5];
	numElems = 0;
    }

    /*@ invariant (\forall int i; i >= 0 && i < numElems; 
				       elems[i].heapPos == i &&
				       (readonly Object) elems[i].owner == (readonly Object) this);
      @*/

    /*@ ensures elems.length > \old(elems.length)
      @       && numElems == \old(numElems);
      @*/
    private void grow() {
	/*@ rep rep @*/ HeapElem[] newElems = new /*@ rep rep @*/ HeapElem[elems.length*2];
	for (int i = 0; i < numElems; ++i)
	    newElems[i] = elems[i];
	elems = newElems;
    }

    /*@ requires e.heapPos == -1;
      @ ensures e.heapPos >= 0 && e.heapPos < numElems &&
      @         (readonly Object) elems[e.heapPos] == (readonly Object) e &&
      @         (\forall int i; i >= 0 && i < numElems; i == e.heapPos || 
      @                  (readonly Object) elems[i] != (readonly Object) e);
      @*/
    public void enqueue(/*@ peer @*/ HeapElem e) {
	if (numElems >= elems.length)
	    grow();
	int pos = numElems++;
	int parent = pos / 2;
	while (pos > 0 && elems[parent].compareTo(e) > 0) {
	    elems[parent].heapPos = pos;
	    elems[pos] = elems[parent];
	    pos = parent;
	    parent = pos / 2;
	}
	elems[pos] = e;
	e.heapPos = pos;
    }

    public /*@ rep @*/ HeapElem getFirst() {
	return elems[0];
    }

    /*@
      @ requires e.heapPos >= 0 && e.heapPos < numElems && 
      @          (readonly Object) elems[e.heapPos] == (readonly Object) e;
      @ ensures (\forall int i; i >= 0 && i < numElems; 
      @                  (readonly Object) elems[i] != (readonly Object) e);
      @*/
    public void remove(/*@ peer @*/ HeapElem e) {
	/*@ rep @*/ HeapElem last = elems[--numElems];
	int pos = e.heapPos;
	e.heapPos = -1;
	if ((/*@ readonly @*/ Object) last == (/*@ readonly @*/ Object) e)
	    return;
	int child = 2*pos+1;
	elems[pos] = last;
	last.heapPos = pos;
	while (child < numElems) {
	    if (child + 1 < numElems
		&& elems[child].compareTo(elems[child+1]) > 0) {
		child++;
	    }

	    if (elems[child].compareTo(last) > 0)
		break;

	    elems[pos] = elems[child];
	    elems[pos].heapPos = pos;
	    pos = child;
	    child = 2*pos+1;
	}
	elems[pos] = last;
	last.heapPos = pos;
    }

    public boolean isEmpty() {
	return numElems == 0;
    }

    public String toString() {
	StringBuilder sb = new /*@ rep @*/ StringBuilder("[");
	String comma = "";
	for (int i = 0; i < numElems; ++i) {
	    sb.append(comma).append(elems[i]);
	    comma = ", ";
	}
	return sb.append(']').toString();
    }

    public static void main(String[] args) {
	BufferedReader in  = new BufferedReader(new InputStreamReader(System.in));
	Heap h = new Heap();
	HashMap map = new HashMap();
	while (true) {
	    try {
		System.out.println("Heap:");
		System.out.println(h);
		System.out.println("a <num> | r <num> | x");
		System.out.print("> ");
		String line = in.readLine();
		if (line == null || line.charAt(0) == 'x')
		    break;
		if (line.length() < 3) {
		    System.out.println("Wrong input");
		    continue;
		}
		int num = Integer.parseInt(line.substring(1).trim());
		switch (line.charAt(0)) {
		    case 'a':
		    {
			IntHeapElem elem = new IntHeapElem(num);
			map.put(new Integer(num), elem);
			h.enqueue(elem);
			break;
		    }
		    case 'r':
		    {
			IntHeapElem elem = (IntHeapElem) map.remove(new Integer(num));
			if (elem != null)
			    h.remove(elem);
			break;
		    }
		    default:
			System.out.println("Wrong input");
		}
	    } catch (Exception exc) {
		System.out.println("Wrong input");
	    }
	}
    }
}