Ошибка доказательства Изабель при вызове последовательных операций записи

Я новичок в Изабель и обязательствах по доказательству, и в настоящее время я перевожу модель VDM, которую я сделал для игры «Точки и квадраты» (базовые переводы типа VDM были предоставлены нам).

Пока у меня есть два типа записей, Dot:

record Dot =
    pos_x :: VDMNat1
    pos_y :: VDMNat1

..и Move (состоящий из двух Dot):

record Move =
    dot_a :: Dot
    dot_b :: Dot

... но теперь я пытаюсь перевести последовательность этих Move и получаю странную ошибку с инвариантом:

type_synonym Moves = "Move VDMSet"

definition inv_Moves :: "Moves ⇒ ????"
    where "inv_Moves ms ≡
        int (card ms) ≤ MAX_MOVES ∧
        (∀ m . m ∈ ms ⟶
            inv_Move m ∧
            pos_x dot_a m > 0 ∧
            pos_y dot_a m > 0 ∧
            pos_x dot_b m > 0 ∧
            pos_y dot_b m > 0 ∧
            pos_x dot_a m ≤ BOARD_WIDTH ∧
            pos_y dot_a m ≤ BOARD_HEIGHT ∧
            pos_x dot_b m ≤ BOARD_WIDTH ∧
            pos_y dot_b m ≤ BOARD_HEIGHT ∧
            inverse_move m ∉ ms)"

Я знаю, что инвариант, вероятно, хуже, чем просто эта ошибка, но, насколько я могу судить по ошибке, у него проблема с несколькими вызовами полей записи; то есть передача dot_a в pos_x вместо результата dot_a m. Единственное решение, которое я могу придумать, - это манипулировать порядком операций, но я не уверен, как этого добиться, поскольку pos_x dot_a m = pos_x (dot_a m).

Любая помощь приветствуется!