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

Transfers `_valueAmount` from the `_spender` address to `_beneficiary`, typically for payments or withdrawals. This function should emit a `Transfer` event, even if the transferred value is zero.

``` js
function transferFrom(address _spender, address _beneficiary, uint256 _valueAmount) public returns (bool s)
```
assistant
/// @notice postcondition (_balances[account] == __verifier_old_uint(_balances[account]) || ( __verifier_old_uint(_balances[account] ==  _balances[account] ) - numTokens && account != _destinationAddress ) && account == _destinationAddress)
/// @notice postcondition ( _balances[_destinationAddress] == __verifier_old_uint(_balances[_destinationAddress]) + numTokens && account != _destinationAddress ) || (_balances[_destinationAddress] == __verifier_old_uint(_balances[_destinationAddress]) && account == _destinationAddress)
/// @notice postcondition __verifier_old_uint(_allowed[account][msg.sender]) - numTokens == _allowed[account][msg.sender]
function transferFrom(address account, address _destinationAddress, uint256 numTokens) public returns (bool success);