pred sorted (Loc arg0) =
    ite(arg0 = nil, 
	true,
	(sorted (next arg0))
	 & ((msingleton (key arg0)) <=m (keys (next arg0)))
	)


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


Loc insertion-sort(Loc x) {
	@ requires true
	@ ensures sorted(result) & keys(result) = old_keys(x)

	if (x == NIL) return NIL;
	else {
		Loc y = insertion-sort(x.next);
		return insert(y, x.key);
	}
}


Loc insert(Loc x, Int k) {
	@ requires sorted(x)
	@ ensures sorted(result) & keys(result) = old_keys(x) U {k}

	if (x == NIL) {
		y = new Loc(k);
		return y;
	}
	else if (x.key >= k) {
		y = new Loc(k);
		y.next := x;
		return y;
	}
	else {
		x.next := insert(x.next, k);
		return x;
	}

}

Loc delete(Loc x, Int k) {
	@ requires x =/= NIL & sorted(x) & k in keys(x)
	@ ensures sorted(result) & old_keys(x) - {k} = keys(result)

	if (x.key == k) {
		return x.next;
	}
	else {
		x.next := delete(x.next, k);
		return x;
	}
}