system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Enable or disable an operator's ability to control all of msg.sender's assets.
/// @dev Emits the ApprovalForAll event and supports having more than one operator per owner.
/// @param _operator The account to authorize or unauthorize as an operator.
/// @param _approved True to authorize, false to deauthorize.

function setApprovalForAll(address _operator, bool _approved) external;
assistant
/// @notice postcondition _operatorApprovals[msg.sender][_operator] == _approved
function setApprovalForAll(address _operator, bool _approved) external;