pred heap (Loc arg0) =
    ite(arg0 = nil,
	true,
	(heap (l arg0))
	(heap (r arg0))
	((keys (l arg0)) <=m (msingleton (key arg0)))
	((keys (r arg0)) <=m (msingleton (key arg0)))
	)

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


Loc max-heapify(Loc x){
	@ requires x =/= NIL & max-heap(x.l) & max-heap(x.r)
	@ ensures max-heap(result) & keys(result) = old_keys(x)

	if (x.r = NIL & x.l =/= NIL & x.l.key > x.key) {
		x.key := x.key + x.l.key ;
		x.l.key := x.key - x.l.key ;
		x.key := x.key - x.l.key ;
		x.l := max-heapify(x.l) ;
	}
	else if (x.l = NIL & x.r =/= NIL & x.r.key > x.key) {
		x.key := x.key + x.r.key ;
		x.r.key := x.key - x.r.key ;
		x.key := x.key - x.r.key ;
		x.r := max-heapify(x.r) ;
	}
	else if (x.l =/= NIL & x.r =/= NIL & x.l.key > x.key & x.l.key >= x.r.key) {
		x.key := x.key + x.l.key ;
		x.l.key := x.key - x.l.key ;
		x.key := x.key - x.l.key ;
		x.l := max-heapify(x.l) ;
	}
	else if (x.l =/= NIL & x.r =/= NIL & x.r.key > x.key & x.r.key > x.l.key) {
		x.key := x.key + x.r.key ;
		x.r.key := x.key - x.r.key ;
		x.key := x.key - x.r.key ;
		x.r := max-heapify(x.r) ;
	}
	
	return x ;
}