Как закончить доказательство TLAPS для уточнения отображения с участием записей?

Question

У меня есть некоторые трудности в доказательстве сопоставления записей. Ниже приведен упрощенный пример, иллюстрирующий спецификации TLA @ github (обратите внимание, что этот пост также находится в tlaplus-googlegroup, но пока без ответов.):

---

SimpleVoting.tla:

Это поддерживает для каждого участника maxBal который является натуральным числом. В IncreaseMaxBal(p, b), maxBal[p] увеличивается до большего значения b,

---------------------------- MODULE SimpleVoting ----------------------------
EXTENDS Naturals
-----------------------------------------------------------------------------
CONSTANT Participant

VARIABLE maxBal

TypeOK == maxBal \in [Participant -> Nat]
-----------------------------------------------------------------------------
Init == maxBal = [p \in Participant |-> 0]

IncreaseMaxBal(p, b) ==
  /\ maxBal[p] < b
  /\ maxBal' = [maxBal EXCEPT ![p] = b]
-----------------------------------------------------------------------------
Next == \E p \in Participant, b \in Nat : IncreaseMaxBal(p, b)

Spec == Init /\ [][Next]_maxBal
=============================================================================

---

Record.tla:

Поддерживает 2D "массив" state, где state[p][q] это состояние q с точки зрения p а государство это запись:State == [maxBal : Nat, maxVBal : Nat],

В Prepare(p, b), state[p][p].maxBal увеличивается до большего значения b,

------------------------------- MODULE Record -------------------------------
EXTENDS Naturals, TLAPS
---------------------------------------------------------------------------
CONSTANTS Participant  \* the set of partipants

VARIABLES state \* state[p][q]: the state of q \in Participant from the view of p \in Participant

State == [maxBal: Nat, maxVBal: Nat]

TypeOK == state \in [Participant -> [Participant -> State]]
---------------------------------------------------------------------------
InitState == [maxBal |-> 0, maxVBal |-> 0]

Init == state = [p \in Participant |-> [q \in Participant |-> InitState]] 

Prepare(p, b) == 
    /\ state[p][p].maxBal < b
    /\ state' = [state EXCEPT ![p][p].maxBal = b]
---------------------------------------------------------------------------
Next == \E p \in Participant, b \in Nat : Prepare(p, b)

Spec == Init /\ [][Next]_state
---------------------------------------------------------------------------

---

Наглядно, Record поддерживает maxBal[p] из SimpleVoting как state[p][p].maxBal, Поэтому я хочу показать, что Record рафинирует SimpleVoting под следующим уточнением отображения:

maxBal == [p \in Participant |-> state[p][p].maxBal]

SV == INSTANCE SimpleVoting

Тем не менее, шаг <3>2 в следующем доказательстве не получается.

THEOREM Spec => SV!Spec
  <1>1. Init => SV!Init
    BY DEF Init, SV!Init, maxBal, InitState
  <1>2. [Next]_state => [SV!Next]_maxBal
    <2>1. UNCHANGED state => UNCHANGED maxBal
      BY DEF maxBal
    <2>2. Next => SV!Next
      <3> SUFFICES ASSUME NEW p \in Participant, NEW b \in Nat,
                          Prepare(p, b)
                   PROVE  SV!IncreaseMaxBal(p, b)
        BY DEF Next, SV!Next
      <3>1. maxBal[p] < b
        BY DEF Prepare, maxBal
      <3>2. maxBal' = [maxBal EXCEPT ![p] = b] \* failed here!
        BY DEF Prepare, maxBal
      <3>3. QED
        BY <3>1, <3>2 DEF SV!IncreaseMaxBal
    <2>3. QED
      BY <2>1, <2>2
  <1>3. QED

Обязательство в <3>2 составляет. Разве не state' = [state EXCEPT ![p] = ...] в предположении так же, как заключение [p_1 \in Participant |-> state[p_1][p_1].maxBal]' ...? Чего не хватает? Что не так с моим доказательством?

ASSUME NEW CONSTANT Participant,
       NEW VARIABLE state,
       NEW CONSTANT p \in Participant,
       NEW CONSTANT b \in Nat,
       /\ state[p][p].maxBal < b
       /\ state'
          = [state EXCEPT
               ![p] = [state[p] EXCEPT
                         ![p] = [state[p][p] EXCEPT !.maxBal = b]]] 
PROVE  [p_1 \in Participant |-> state[p_1][p_1].maxBal]'
       = [[p_1 \in Participant |-> state[p_1][p_1].maxBal] EXCEPT ![p] = b]