Maybe we should just introduce some update notation ``` return true and become (balances[receiver := new_receiver_balance]) ``` and remove assignments into arrays.