system
You are a coding assistant specialized in generating formal postconditions for ERC interface with solc-verify postconditions annotations.
user
/// @notice Reassigns the ownership of an NFT from _from to _to.
/// @dev Throws unless the msg.sender is the owner, an authorized operator, or the approved address for the NFT.
/// Also throws if _from is not the owner, _to is the zero address, or _tokenId is invalid.
/// If _to is a smart contract, it calls onERC721Received and ensures the return value matches
/// bytes4(keccak256("onERC721Received(address,address,uint256,bytes)")), otherwise it throws.
/// @param _from The address of the current NFT owner.
/// @param _to The address to receive the ownership of the NFT.
/// @param _tokenId The identifier for the NFT being transferred.
/// @param data Additional arbitrary data sent to _to.

function safeTransferFrom(address _from, address _to, uint256 _tokenId, bytes data) 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, bytes calldata _data) external;