system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Transfer an NFT's ownership from one account to another.
/// @dev Operates like the other function with an additional data parameter,
/// but this implementation uses an empty string for the data.
/// @param _from The current holder of the NFT.
/// @param _to The recipient of the NFT.
/// @param _tokenId The unique ID of the NFT to transfer.

function safeTransferFrom(address _from, address _to, uint256 _tokenId) external payable;
assistant
/// @notice  postcondition ( ( _ownedTokensCount[_from] ==  __verifier_old_uint (_ownedTokensCount[_from] ) - 1  &&  _from  != _to ) || ( _from == _to )  )
/// @notice  postcondition ( ( _ownedTokensCount[_to] ==  __verifier_old_uint ( _ownedTokensCount[_to] ) + 1  &&  _from  != _to ) || ( _from  == _to ) )
/// @notice  postcondition  _tokenOwner[_tokenId] == to
function safeTransferFrom(address _from, address _to, uint256 _tokenId) external;