system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
#### transfer

Transfers `_amount` of tokens to the `_recipient` address.
The function triggers a `Transfer` event and reverts if the sender’s balance is insufficient.

It is worth mentioning that transfers with a value of 0 must still trigger the `Transfer` event.

``` js
function transfer(address _recipient, uint256 _amount) public returns (bool success)
```
assistant
/// @notice postcondition (  __verifier_old_uint(_balances[msg.sender]) - _tokens == _balances[msg.sender] && msg.sender != receiver  )
/// @notice postcondition ( _balances[receiver] == __verifier_old_uint(_balances[receiver]) + _tokens && msg.sender != receiver )
/// @notice emits Transfer
function transfer(address receiver, uint256 _tokens) public returns (bool success);