system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Verify if a given address is authorized to operate on all NFTs owned by another address.
/// @param _owner Address of the NFT owner.
/// @param _operator Address to verify for operator approval.
/// @return Returns true if _operator is authorized, false otherwise.

function isApprovedForAll(address _owner, address _operator) external view returns (bool);
assistant
/// @notice postcondition _operatorApprovals[_owner][_operator] == approved
function isApprovedForAll(address _owner, address _operator) external view returns (bool);