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

Requirements:
Sends `_valueTokens` to the 'to' address.
The function should revert if the msg.sender does not have enough balance

Obs.:
Transfers of 0 value must be handled like any other and fire the `Transfer` event.
``` js
function transfer(address to, uint256 _valueTokens) public returns (bool success)
```
assistant
/// @notice postcondition ( _balances[msg.sender] == __verifier_old_uint(_balances[msg.sender]) - _value && msg.sender != _to )
/// @notice postcondition ( _balances[_to] == __verifier_old_uint(_balances[_to]) + _value && msg.sender != _to )
function transfer(address _to, uint256 _value) public returns (bool success);