removeStudentId(ident uid, ident username) { assume exists /account[uid]/admin; assume exists /account[username]/student; # implies the account exists, which is implicitly true anyway assume size(/exercise/student[/account[username]/student/id]) = 0; assume size(/exam/participant[/account[username]/student/id]) = 0; remove /account[username]/student; }