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

Enables a contract to move `t` from `h` to `r`, ensuring that a `Transfer` event is emitted. This is useful for scenarios where a contract is authorized to manage user funds.


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