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

Displays how much `_authorizedUser` is permitted to use from `_holder`'s balance.

``` js
function allowance(address _holder, address _authorizedUser) public view returns (uint256 fundsAvailable)
```
assistant
/// @notice postcondition _allowed[_accountHolder][_operator] == withdrawableAmount
function allowance(address _accountHolder, address _operator) public view returns (uint256 withdrawableAmount);