pred treap (Loc arg0) =
    ite(arg0 = nil,
	true,
	(treap (l arg0))
	& (treap (r arg0))
	& ((singleton (priority arg0)) <m (priorities (l arg0)))
	& ((singleton (priority arg0)) <m (priorities (r arg0)))
	& ((keys (l arg0)) <m (singleton (key arg0)))
	& ((singleton (key arg0)) <m (keys (r arg0)))
	& (disjoint (priorities (l arg0)) (priorities (r arg0)))
	)


mset keys (Loc arg0) =
    ite(arg0 = nil, 
	emptymset,
	(((msingleton (key arg0)) Um (keys (l arg0))) Um (keys (r arg0)))
	)

mset priorities (Loc arg0) =
    ite(arg0 = nil, 
	emptymset,
	(((msingleton (priority arg0)) Um (priorities (l arg0))) Um (keys (r arg0)))
	)


Loc treap-insert(Loc x, Int k, Int p){
	@ requires treap(x) & k notin keys(x) & p notin priorities(x)
	@ ensures result =/= nil & treap'(result) & keys'(result) = keys(x) U {k} & priorities'(result) = priorities(x) U {p}

	if (x == nil) {
		new y;
		y.key := k;
		y.priority := p;
		return y;
	}
	else if (k < x.key) {
		x.l := treap-insert(x.l, k, p);
		if (x.priority > x.l.priority) {
			Loc y := x.l;
			x.l := y.r;
			y.r := x
			return y;
		}
		return x;
	}
	else {
		x.r := treap-insert(x.r, k, p);
		if (x.priority > x.r.priority) {
			Loc y := x.r;
			x.r := y.l;
			y.l := x;
			return y;
		}
		return x;
	}
}


Loc treap-delete(Loc x, Int k){
	@ requires x =/= NIL & treap(x) & k in keys(x)
	@ ensures treap'(result) & keys'(result) U {k} = keys(x) & priorities'(result) \subset priorities(x)

	if (x.key > k) {
		x.l := treap-delete(x.l, k);
		return x;
	}
	else if (x.key < k) {
		x.r := treap-delete(x.r, k);
		return x;
	}
	else {
		return remove(x);
	}
}


Loc remove(Loc x) {
	@ requires x =/= NIL & treap(x.l) & treap(x.r) & keys(x.l) < keys(x.r) & disjoint(priorities(x.l), priorities(x.r))
	@ ensures treap'(result) & keys'(result) = keys(x.l) U keys(x.r) & priorities'(result) = priorities(x.l) U priorities(x.r)

	if (x.l == NIL & x.r == NIL) {
		return NIL;
	}
	else if (x.l =/= NIL & x.r == NIL) {
		return x.l;
	}
	else if (x.l == NIL & x.r =/= NIL) {
		return x.r;
	}
	else if (x.l.priority <= x.r.priority) {
		Loc y := x.l;
		x.l := y.r;
		y.r := remove(x);
		return y;
	}
	else {
		Loc y := x.r;
		x.r := y.l;
		y.l := remove(x);
		return y;
	}
}