TLA + Проблема с удалением элемента

В настоящее время изучаю TLA + и застряли на этом простом методе удаления человека из реестра. Насколько я могу судить, проблема связана с состоянием разрешения.

Моя функция TLA + выглядит так и удаляет человека из реестра вместе с разрешениями.

DeRegister(p) == 
/\ p \in register
/\ register' = register \ {p}
/\ permission' = [x \in DOMAIN permission \ {p} |-> permission[x]]
/\ UNCHANGED <<location>>

Мой типок, который я проверяю, имеет следующие ограничения

TypeOk 
    /\ register \subseteq PERSON
    /\ permission \in [register -> SUBSET BUILDING]
    /\ location \in [register -> (BUILDING \union {OUTSIDE})]

Я получаю ошибку модели, что нарушен typeOK. В трассировке стека ошибка выглядит так

/\  location = [p1 |-> OUTSIDE]
/\  permission = << >>
/\  register = {}

Спасибо за понимание

РЕДАКТИРОВАТЬ:

Предыдущее состояние может быть полезно,

/\  location = [p2 |-> OUTSIDE]
/\  permission = [p2 |-> {}]
/\  register = {"p2"}