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

Transfers `_value` amount of tokens from address `_from` to address `_to`, and MUST fire the `Transfer` event.

The `transferFrom` method is used for a withdraw workflow, allowing contracts to transfer tokens on your behalf.
This can be used for example to allow a contract to transfer tokens on your behalf and/or to charge fees in sub-currencies.
The function SHOULD `throw` unless the `_from` account has deliberately authorized the sender of the message via some mechanism.

*Note* Transfers of 0 values MUST be treated as normal transfers and fire the `Transfer` event.

``` js
function transferFrom(address _from, address _to, uint256 _value) public returns (bool success)
```
assistant
/// @notice postcondition ( _balances[_from] == __verifier_old_uint(_balances[_from]) - _value && _from != _to ) || (_balances[_from] == __verifier_old_uint(_balances[_from]) && _from == _to)
/// @notice postcondition ( _balances[_to] == __verifier_old_uint(_balances[_to]) + _value && _from != _to ) || (_balances[_to] == __verifier_old_uint(_balances[_to]) && _from == _to)
/// @notice postcondition _allowed[_from][msg.sender] == __verifier_old_uint(_allowed[_from][msg.sender]) - _value
function transferFrom(address _from, address _to, uint256 _value) public returns (bool success);