# Fix Apalache Assignment Error ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-01-11]] ## Synopsis Apalache fails to verify the bounded FIFO example: ```tla Next == /\ Inner!Next /\ Inner!BufRecv => (Len(q) < N) ``` Because the `implies` breaks the Apalache [assignments principle](https://apalache-mc.org/docs/apalache/principles/assignments.html). The solution is expanding the `Next` action ```tla Next == \/ \E m \in Message: Inner!SSend(m) \/ /\ Inner!BufRecv /\ Len(q) < N \/ Inner!BufSend \/ Inner!RRecv ```