\documentclass{article}
\usepackage{fuzz}
\usepackage[pdftitle={Formal Specification of XML Information Set}, pdfauthor={Arthur Ryman}]{hyperref}

\title{Formal Specification of XML Information Set}
\author{Arthur Ryman}
\date{\today}

\begin{document}

\maketitle

\section*{Abstract}

This document is a formal specification of 
\href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204}{XML Information Set (Second Edition), 
W3C Recommendation 4 February 2004}.
The purpose of this document is to define terms used in the
WSDL 2.0 formal specification.
The Z Notation formal specification language is used.

\clearpage

\section{Introduction}

An XML document's information set is a set of information items.
An information set is like a DOM tree
and an information item is like a node in the tree.
A subset of information items do in fact form a tree based on a parent-child relation.

Each information item in the information set has a set of properties 
whose values may be either simple data objects or references 
to other information items.
In order to model references, it is convenient to add a unique identifier to each
information item.

\subsection{II}

Let $II$ be the set of information item identifiers:
\begin{zed}
	[II]
\end{zed}

\subsection{Item}

Every information item has an identifier.
Let $Item$ be the set of information items identifier properties.
\begin{schema}{Item}
	id : II
\end{schema}

\subsection{The Eleven Kinds of Information Item}

There are eleven kinds of information item.
We therefore partition the set of information item identifiers as follows.
Let 
$AII$,
$CII$,
$ChII$,
$DII$,
$DTDII$,
$EII$,
$NII$,
$NsII$,
$PIII$,
$UEII$,
$UERII$ 
be the subsets of
attribute,
comment,
character,
document,
document type declaration,
element,
notation,
namespace,
processing instruction,
unparsed entity,
unexpanded entity reference
information item identifiers.
\begin{axdef}
	AII, CII, ChII, DII, DTDII, EII, NII, \\
	\t1	NsII, PIII, UEII, UERII : \power II
\where
	\langle AII, CII, ChII, DII, DTDII, EII, NII, \\
	\t1	NsII, PIII, UEII, UERII \rangle \partition II
\end{axdef}
Every information item identifier 
is exactly one of the eleven kinds of information item identifiers.

\subsection{Property Types}

Information items have properties. 
Each property has a name 
and takes values of a specified type.

Although the XML Information Set specification uses square brackets to denote
property names, they will not be used here in order to avoid possible 
confusion with the standard
usage of square brackets in Z Notation.

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#intro.null}{``Unknown'' and ``No Value''}
\end{description}

A property value may be unknown or the property may have no value,
and it is necessary to distinguish between these two cases.
The specification models this situation by extending the normal
domain of values with two additional special values to represent unknown and undefined values.

The following sections define property types that are used by information items.

\subsubsection{ExtendedII and ExtendedIIs}

Let $ExtendedII$ be the set of information item identifiers extended with values
that represent no value and unknown:
\begin{zed}
	ExtendedII ::= valueII \ldata II \rdata | \\
	\t1	noValueII | unknownII
\end{zed}

Let $ExtendedIIs$ be the set of sequences of information item identifiers extended with values
that represent no value and unknown:
\begin{zed}
	ExtendedIIs ::= valueIIs \ldata \seq II \rdata | \\
	\t1	noValueIIs | unknownIIs
\end{zed}

\subsubsection{URI, ExtendedURI, and OptionalURI}

Let $URI$ be the set of URIs:
\begin{zed}
	[URI]
\end{zed}

Let $ExtendedURI$ be the set of URIs extended with values
that represent no value and unknown:
\begin{zed}
	ExtendedURI ::= valueURI \ldata URI \rdata | \\
	\t1	noValueURI | unknownURI
\end{zed}

Let $OptionalURI$ be the set of optional URIs:
\begin{zed}
	OptionalURI == ExtendedURI \setminus \{unknownURI\}
\end{zed}

\subsubsection{CharacterEncodingScheme}

Let $CharacterEncodingScheme$ be the set of character encoding scheme names:
\begin{zed}
	[CharacterEncodingScheme]
\end{zed}

\subsubsection{ISO10646}

Let $ISO10646$ be the set of ISO 10646 character codes that represent valid XML characters:
\begin{axdef}
	ISO10646 : \power (0 \upto 1114111)
\end{axdef}

Note that this set depends on the XML version. XML 1.1 introduced additional valid
characters.

For the purposes of this specification we'll assume that this set is the largest
set of character codes in the ISO 10646 range that excludes the explicitly
illegal XML characters.

\subsubsection{String, ExtendedString, and OptionalString}

Let $String$ be the set of strings:
\begin{zed}
	[String]
\end{zed}

Let $ExtendedString$ be the set of strings extended with values
that represent no value and unknown.
\begin{zed}
	ExtendedString ::= valueString \ldata String \rdata | \\
	\t1	noValueString | unknownString
\end{zed}

Let $OptionalString$ represent an optional set string value.
\begin{zed}
	OptionalString == ExtendedString \setminus \{unknownString\}
\end{zed}

\subsubsection{YesNo and OptionalYesNo}

Let $YesNo$ be the set of `Yes' and `No':
\begin{zed}
	YesNo ::= Yes | No
\end{zed}

Let $OptionalYesNo$ represent an optionally set yes or no value:
\begin{zed}
	OptionalYesNo ::= valueYesNo \ldata YesNo \rdata | noValueYesNo
\end{zed}

\subsubsection{Boolean, ExtendedBoolean, and OptionalBoolean}

Let $Boolean$ be the set of `True' and `False':
\begin{zed}
	Boolean ::= True | False
\end{zed}

Let $ExtendedBoolean$ be the set of Boolean values extends with values
that represent no value and unknown:
\begin{zed}
	ExtendedBoolean ::= valueBoolean\ldata Boolean \rdata | \\
	\t1	noValueBoolean | unknownBoolean
\end{zed}

Let $OptionalBoolean$ be the set of optional Boolean values:
\begin{zed}
	OptionalBoolean == ExtendedBoolean \setminus \{unknownBoolean\}
\end{zed}

\subsubsection{NCName}

Let $NCName$ be the set of XML NCNames:
\begin{zed}
	[NCName]
\end{zed}

Note that this set also depends on the XML version, but we'll take it to be
the largest set that excludes the explicitly illegal names.

\subsubsection{AttributeType and ExtendedAttributeType}

Let $AttributeType$ be the set of attribute types:
\begin{zed}
	AttributeType ::= \\
	\t1	ID | IDREF | IDREFS | \\
	\t1	ENTITY | ENTITIES | \\
	\t1	NMTOKEN | NMTOKENS | \\
	\t1	NOTATION | CDATA | ENUMERATION
\end{zed}

Let $ExtendedAttributeType$ be the set of attribute types extended with values
that represent no value and unknown:
\begin{zed}
	ExtendedAttributeType ::= valueAttributeType \ldata AttributeType \rdata | \\
	\t1	noValueAttributeType | unknownAttributeType
\end{zed}

\subsubsection{ReferenceType and NonReferenceType}

Let $ReferenceType$ be the set of attribute types that refer to information items:
\begin{zed}
	ReferenceType == \\
	\t1	\{IDREF, IDREFS, ENTITY, ENTITIES, NOTATION\}
\end{zed}

Let $NonReferenceType$ be the set of attribute types that do not refer to information items:
\begin{zed}
	NonReferenceType == AttributeType \setminus ReferenceType
\end{zed}

\subsubsection{NormalizedValue and typeValue}

Let $NormalizedValue$ be the set of normalized attribute values:
\begin{axdef}
	NormalizedValue : \power String
\end{axdef}

Let $typeValue$ be the relation that associates an attribute type with its set of syntactically
valid normalized attribute values:
\begin{axdef}
	typeValue : AttributeType \rel NormalizedValue
\end{axdef}

\section{Information Items}

The following sections define the properties taken by each kind of information item.

\subsection{The Document Information Item}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.document}{2.1 The Document Information Item}
\end{description}

There is exactly one document information item in the information set
of a document, and all the other informations items in the information
set are accessible directly or indirectly through the properties of the
document information item.

\subsubsection{DocumentItem1}

Let $DocumentItem1$ be the set of unconstrained document information item properties:
\begin{description}

\item[children] Let $children$ be the sequence of child information items, in document order. 
Each child appears exactly once in the children sequence, so the sequence is injective.

\item[document element] Let $documentElement$ be the unique child element information item of the document information item.

\item[notations] Let $notations$ be the finite set of notation element items.

\item[unparsed entities] Let $unparsedEntities$ be the finite set of unparsed entity information items.

\item[base URI] Let $baseURI$ be the base URI of the document entity.

\item[character encoding scheme] Let $characterEncodingScheme$ be the character encoding scheme used by the document entity.

\item[standalone] Let $standalone$ be the optional indication of the standalone status of the document.
The standalone status of the document is derived from the optional XML declaration at the beginning of the document entity.
If there is no XML declaration then this property has no value.

\item[version] Let $version$ be the optional indication of the version of the document entity.
The version of the document entity is derived from the optionally present XML declaration.
If there is no XML declaration then this property has no value.

\item[all declarations processed] Let $allDeclarationsProcessed$ be the indication of 
whether the processor has read the complete DTD.
If the DTD has been read certain other properties, described below, are never unknown.
Otherwise, they may be unknown.

\end{description}
\begin{schema}{DocumentItem1}
	Item \\
	children : \iseq II \\
	documentElement : EII \\
	notations : \finset NII \\
	unparsedEntities : \finset UEII \\
	baseURI : URI \\
	characterEncodingScheme : CharacterEncodingScheme \\
	standalone : OptionalYesNo \\
	version : OptionalString \\
	allDeclarationsProcessed : Boolean
\where
	id \in DII
\end{schema}
The identifier is a document information item identifier.

There are constraints on these properties which will be described in the following sections.

\subsubsection{DocumentItemChildren}

There are several constraints on the $children$ property.

Let $DocumentItemChildren$ be the set of document information item properties that satisfy the constraints
on the $children$ property.
It is convenient to define the following derived properties:
\begin{itemize}
\item Let $child$ be the set of child information items defined by the $children$
property.
\item Let $dtdiis$ be the subset of child DTD information items.
\end{itemize}
\begin{schema}{DocumentItemChildren}
	DocumentItem1 \\
	child : \finset II \\
	dtdiis : \finset DTDII
\where
	child = \ran children \\
	child \subset EII \cup PIII \cup CII \cup DTDII \\
	child \cap EII = \{documentElement\}
\also
	dtdiis = child \cap DTDII \\
	\# dtdiis \leq 1
\end{schema}
\begin{itemize}

\item $child$ is the set of information items that appear in the children sequence.

\item Each child information item is either an  element, processing instruction, comment, or DTD information item.

\item The only child element information item is the document element.

\item $dtdiis$ is the subset of child DTD information items.

\item There is at most one child DTD information item.

\end{itemize}

\subsubsection{DocumentItemNotations}

The notations of a document information item are defined in the DTD, so if the DTD
is absent there can be no notations.

Let $DocumentItemNotations$ be the set of document information item properties
that satisfy this constraint on notations:
\begin{schema}{DocumentItemNotations}
	DocumentItemChildren
\where
	dtdiis = \emptyset \implies notations = \emptyset
\end{schema}
If there is no DTD then there are no notations.

\subsubsection{DocumentItemUnparsedEntities}

The unparsed entities of a document information item are defined in the DTD, so if the DTD
is absent there can be no unparsed entities.

Let $DocumentItemUnparsedEntities$ be the set of document information item properties
that satisfy this constraint on unparsed entities:
\begin{schema}{DocumentItemUnparsedEntities}
	DocumentItemChildren
\where
	dtdiis = \emptyset \implies unparsedEntities = \emptyset
\end{schema}
If there is no DTD then there are no unparsed entities.

\subsubsection{DocumentItemAllDeclarationsProcessed}

The indication of whether the processor has read the complete DTD
can never be false if there is no DTD.

Let $DocumentItemAllDeclarationsProcessed$ be the set of document information item
properties that satisfy this constraint:
\begin{schema}{DocumentItemAllDeclarationsProcessed}
	DocumentItemChildren
\where
	dtdiis = \emptyset \implies allDeclarationsProcessed = True
\end{schema}
If there is no DTD then all declarations have been processed.

\subsubsection{DocumentItem}

Let $DocumentItem$ be the set of all document information item properties
that satisfy all the constraints:
\begin{zed}
	DocumentItem \defs \\
	\t1 DocumentItemChildren \land \\
	\t1 DocumentItemNotations \land \\
	\t1 DocumentItemUnparsedEntities \land \\
	\t1 DocumentItemAllDeclarationsProcessed
\end{zed}

\subsection{Element Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.element}{2.2 Element Information Items}
\end{description}

The information set of a document has an element information item for 
each element in the document.

\subsubsection{ElementItem}

Let $ElementItem$ be the set of element information item properties:
\begin{description}

\item[namespace name] Let $namespaceName$ be the URI namespace name, if any of the element type.
If the element does not belong to a namespace, this property has no value.

\item[local name] Let $localName$ be the NCName local part of the element name.

\item[prefix] Let $prefex$ be the string prefix part of the element-type name.
If the element has no prefix, this property has no value.

\item[children] Let $children$ be the sequence of child information items in document order.
Each child information item appears exactly once in this sequence, so the sequence is injective.
This sequence contains element, processing instruction, unexpanded entity reference, character, and comment
information items.

\item[attributes] Let $attributes$ be the finite set of attribute information items, one for each
attribute of the element (specified or defaulted), except for namespace attributes.

\item[namespace attributes] Let $namespaceAttributes$ be the finite set of attribute information items,
one for each namespace attribute of the element (specified or defaulted).
All namespaces attributes have a namespace property of {\tt http://www.w3.org/2000/xmlns}.

\item[in-scope namespaces] Let $inScopeNamespaces$ be the non-empty finite set of namespace information items
that are in effect for this element.
This set always contains the namespace information item with the prefix {\tt xml} bound to the 
namespace {\tt http://www.w3.org/XML/1998/namespace}.
This set never contains an item with the prefix {\tt xmlns}.
This set always contains items that correspond to the items in 
$namespaceAttributes$ except those that undeclare namespaces.

\item[base URI] Let $baseURI$ be the base URI of the element.

\item[parent] Let $parent$ be the information item that has this element information item as a child. 
The parent of an element information item is either an element information item or 
a document information item.

\end{description}
\begin{schema}{ElementItem}
	Item \\
	namespaceName : OptionalURI \\
	localName : NCName \\
	prefix : OptionalString \\
	children : \iseq (EII \cup PIII \cup UEII \cup ChII \cup CII)\\
	attributes : \finset AII \\
	namespaceAttributes : \finset AII \\
	inScopeNamespaces : \finset_1 NsII \\
	baseURI : URI \\
	parent : DII \cup EII
\where
	id \in EII \\
	attributes \cap namespaceAttributes = \emptyset
\end{schema}
\begin{itemize}

\item The identifier is an element information item identifier.

\item The attributes and namespace attributes are disjoint sets.

\end{itemize}

\subsection{Attribute Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.attribute}{2.3 Attribute Information Items}
\end{description}

There is an attribute information item for each attribute (specified or defaulted) of each element.

\subsubsection{AttributeItem1}

Let $AttributeItem1$ be the set of unconstrained attribute information item properties:
\begin{description}

\item[namespace name] Let $namespaceName$ be the URI namespace, if any, of the attribute name.
If this attribute has no namespace, this property has no value.

\item[local name] Let $localName$ be the NCName local part of the attribute name.

\item[prefix] Let $prefix$ be the string prefix part, if any, of the attribute name.
If the attribute name has no prefix part, this property has no value.

\item[normalized value] Let $normalizedValue$ be the normalized attribute value.

\item[specified] Let $specified$ be a Boolean flag that indicates when True that the attribute was specified in the start-tag
of its element and when False that the attribute was defaulted from the DTD.

\item[attribute type] Let $attributeType$ be an indication of the type of the attribute.

If there is no declaration for this attribute, this property has no value.

If a declaration has not been read and the $allDeclarationsProcessed$ property of the document is false, this property 
has a value of unknown.

\item[references] Let $references$ be the sequence of element, unparsed entity, or notation information items that
are referenced in the attribute value, in the order they appear there.

If the attribute type has no value or is ID, NMTOKEN, NMTOKENS, CDATA, or ENUMERATION, this property has no value.

If the attribute type is unknown, this property has an unknown value.
Otherwise, the attribute type is IDREF, IDREFS, ENTITY, ENTITIES, or NOTATION, and this property of the corresponding sequence of
information items.

If the attribute value is syntactically invalid, this property has no value.

If the attribute type is IDREF or IDREFS and any of the values do not appear as the value of an ID attribute, this property has no value.

If the attribute type is ENTITY, ENTITIES, or NOTATION and no declaration has been read for any of the enities or the notation, this
property either has no value or is unknown, depending on whether the 
$allDeclarationsProcessed$ property is true or false.

If the attribute type is IDREF or IDREFS and any of the IDs appear as the value of more than one ID attribue, 
this property has no value.

\item[owner element] Let $ownerElement$ be the element information item that 
contains this item in its
$attributes$ or $namespaceAttributes$ properties.

\end{description}
\begin{schema}{AttributeItem1}
	Item \\
	namespaceName : OptionalURI \\
	localName : NCName \\
	prefix : OptionalString \\
	normalizedValue : NormalizedValue \\
	specified : Boolean \\
	attributeType : ExtendedAttributeType \\
	references : ExtendedIIs \\
	ownerElement : EII
\where
	id \in AII
\end{schema}
The identifier is an attribute information item identifier.

The constraints on the properties of attribute information items are described in the following sections.

\subsubsection{AttributeItemReferences}

Let $AttributeItemReferences$ be that set of attribute information item properties that satisfy the
constraints on the $references$ property that can be expressed without reference to other information items:
\begin{schema}{AttributeItemReferences}
	AttributeItem1
\where
	attributeType = unknownAttributeType \implies \\
	\t1	references = unknownIIs
\also
	attributeType = noValueAttributeType \implies \\
	\t1	references = noValueIIs
\also
	attributeType \in valueAttributeType \limg NonReferenceType \rimg \implies \\
	\t1	references = noValueIIs
\also
	\exists t : ReferenceType | attributeType = valueAttributeType~t @ \\
	\t1	t \mapsto normalizedValue \notin typeValue \implies \\
	\t1	references = noValueIIs
\end{schema}
\begin{itemize}

\item If the attribute type is unknown then references are unknown.

\item If the attribute type has no value then references has no value.

\item If the attribute type is a non-reference type then reference has no value.

\item If the attribute type is a reference type but the attribute value is not syntactically valid then references has no value.

\end{itemize}

\subsubsection{AttributeItem}

Let $AttributeItem$ be the set of constrained attribute information items:
\begin{zed}
	AttributeItem \defs AttributeItemReferences
\end{zed}

\subsection{Processing Instruction Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.pi}{2.4 Processing Instruction Information Items}
\end{description}

There is a processing instruction information item for each processing instruction in the document.

\subsubsection{InstructionItem}

Let $InstructionItem$ be the set of processing information item properties:
\begin{description}

\item[target] Let $target$ be the string, an XML name, representing the target part of the processing instruction.

\item[content] Let $content$ be the possibly empty string representing the content of the processing instruction.

\item[base URI] Let $baseURI$ be the base URI of the processing instruction.

\item[notation] Let $notation$ be the notation information item named by the target.

If there is no declaration for a notation with that name, this property has no value.

If no declaration has been read, but the $allDeclarationsProcessed$ property is false, this property is unknown.

\item[parent] Let $parent$ be the document, element, or document type definition information item that contains this item in
its $children$ property.

\end{description}
\begin{schema}{InstructionItem}
	Item \\
	target : String \\
	content : String \\
	baseURI : URI \\
	notation : ExtendedII \\
	parent : DII \cup EII \cup DTDII
\where
	id \in PIII \\
	notation \in \{noValueII, unknownII\} \cup valueII\limg NII \rimg
\end{schema}
\begin{itemize}

\item The identifier is a processing instruction information item identifier.

\item If the notation has a value, it is a notation information item.

\end{itemize}

\subsection{Unexpanded Entity Reference Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.rse}{2.5 Unexpanded Entity Reference Information Items}
\end{description}

An unexpanded entity reference information item is a placeholder for an external parsed entity
that has not been expanded.

\subsubsection{ReferenceItem}

Let $ReferenceItem$ be the set of unexpanded entity reference information items:
\begin{description}

\item[name] Let $name$ be the string name of the referenced entity.

\item[system identifier] Let $systemIdentifier$ be the string system identifier of the entity
as it appears in the declaration of the entity.

If there is no declaration, this property has no value.

If no declaration has been read and the $allDeclarationsProcessed$ property is false, this property is unknown.

\item[public identifier] Let $publicIdentifier$ be the normalized string public identifier of the entity.

If there is no declaration, this property is unknown.

If no declaration has been read and the $allDeclarationsProcessed$ property is false, this property is unknown.

\item[declaration base URI] Let $declarationBaseURI$ be the base URI relative to which the system identifier is resolved.

This property has no value or is unknown under the same circumstances as the system identifier.

\item[parent] Let $parent$ be the element information item that contains this item in its $children$ property.

\end{description}
\begin{schema}{ReferenceItem}
	Item \\
	name : String \\
	systemIdentifier : ExtendedURI \\
	publicIdentifier : ExtendedString \\
	declarationBaseURI : ExtendedURI \\
	parent : EII
\where
	id \in UERII
\also
	systemIdentifier = noValueURI \iff \\
	\t1	declarationBaseURI = noValueURI
\also
	systemIdentifier = unknownURI \iff \\
	\t1	declarationBaseURI = unknownURI
\end{schema}
\begin{itemize}

\item The identifier is an unexpanded entity reference information item identifier.

\item The system identifier has no value exactly when the declaration base URI has no value.

\item The system identifier is unknown exactly when the declaration base URI is unknown.

\end{itemize}

\subsection{Character Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.character}{2.6 Character Information Items}
\end{description}

There is a character information item for each data character that appears in the document
whether literally, as a character reference, or within a CDATA section.

\subsubsection{CharacterItem}

Let $CharacterItem$ be the set of character information item properties:
\begin{description}

\item[character code] Let $characterCode$ be the ISO 10646 character code of the character.

\item[element content whitespace] Let $elementContentWhitespace$ be a Boolean indicate if this
character is white space appearing within element content.

If there is no declaration for the containing element, this property has no value.

If no declaration has been read and the $allDeclarationsProcessed$ property is false, this property is unknown

\item[parent] Let $parent$ be the element information item that contains this item in its children.

\end{description}
\begin{schema}{CharacterItem}
	Item \\
	characterCode : ISO10646 \\
	elementContentWhitespace : ExtendedBoolean \\
	parent : EII
\where
	id \in ChII
\end{schema}
The identifier is a character information item identifer.

\subsection{Comment Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.comment}{2.7 Comment Information Items}
\end{description}

There is a comment information item for every comment that appears in the document,
except for those that appear in the DTD.

\subsubsection{CommentItem}

Let $CommentItem$ be the set of comment information item properties:
\begin{description}

\item[content] Let $content$ be the string content of the comment.

\item[parent] Let $parent$ be the document or element information item that contains this item in its
$children$ property.

\end{description}
\begin{schema}{CommentItem}
	Item \\
	content : String \\
	parent : DII \cup EII
\where
	id \in CII
\end{schema}
The identifier is a comment information item identifier.

\subsection{The Document Type Declaration Information Item}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.doctype}{2.8 The Document Type Declaration Information Item}
\end{description}

If the document has a DTD, there is a single DTD information item in the information set.

\subsubsection{DeclarationItem}

Let $DeclarationItem$ be the set of DTD information item properties:
\begin{description}
\item[system identifier] Let $systemIdentifier$ be the URI of the external subset if one exists.

If there is no external subset, this property has on value.

\item[public identifier] Let $publicIdentifier$ be the string public identifier of the external subset if one exists.

If there is no external subset, this property had no value.

\item[children] Let $children$ be the sequence of procession instruction informatio items, in document order,
with the internal items appearing before the external items.

\item[parent] Let $parent$ be the document information item.

\end{description}
\begin{schema}{DeclarationItem}
	Item \\
	systemIdentifier : OptionalURI \\
	publicIdentifier : OptionalString \\
	children : \iseq PIII \\
	parent : DII
\where
	id \in DTDII
\end{schema}
The identifier is a document type definition information item identifier.

\subsection{Unparsed Entity Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.entity.unparsed}{2.9 Unparsed Entity Information Items}
\end{description}

There is an unparsed entity information item for each unparsed general entity declared in the DTD.

\subsubsection{EntityItem}

Let $EntityItem$ be the set of unparsed entity information item properties:
\begin{description}

\item[name] Let $name$ be the string name of the entity.

\item[system identifier] Let $systemIdentifier$ be the URI system identifier of the entity.

\item[public identifier] Let $publicIdentifier$ be the string public identifier of the entity if it
has one. Otherwise this property has no value.

\item[declaration base URI] Let $declarationBaseURI$ be the base URI relative to which the
system URI is resolved.

\item[notation name] Let $notationName$ be the string notation name associated with the entity.

\item[notation] Let $notation$ be the notation information item named by the notation name.
If no there is no declaration for an entity with the notation name, then this property has no value.
If no declaration has been read and the value of the $allDeclarationsProcessed$ property is false then
this property has an unknown value.

\end{description}
\begin{schema}{EntityItem}
	Item \\
	name : String \\
	systemIdentifier : URI \\
	publicIdentifier : OptionalString \\
	declarationBaseURI : URI \\
	notationName : String \\
	notation : ExtendedII
\where
	id \in UEII
\end{schema}
The identifier is an unparsed entity information item identifier.

\subsection{Notation Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.notation}{2.10 Notation Information Items}
\end{description}

There is a notation information item for each notation declared in the DTD.

\subsubsection{NotationItem}

Let $NotationItem$ be the set of notation information item properties:
\begin{description}

\item[name] Let $name$ be the string name of the notation.

\item[system identifier] Let $systemIdentifier$ be the optional URI system identifier of the notation.

\item[public identifier] Let $publicIdentifier$ be the optional string public identifier of the notation.

\item[declaration base URI] Let $declarationBaseURI$ be the base URI relative to which the system identifier is
resolved.

\end{description}
\begin{schema}{NotationItem}
	Item \\
	name : String \\
	systemIdentifier : OptionalURI \\
	publicIdentifier : OptionalString \\
	declarationBaseURI : URI
\where
	id \in NII
\end{schema}
The identifier is a notation information item identifier.

\subsection{Namespace Information Items}

\begin{description}
\item[XML Information Set:] \href{http://www.w3.org/TR/2004/REC-xml-infoset-20040204#infoitem.namespace}{2.11 Namespace Information Items}
\end{description}

Each element has a namespace information item for each namespace that is in scope in the element.

\subsubsection{NamespaceItem}

Let $NamespaceItem$ be the set of namespace information item properties:
\begin{description}

\item[prefix] Let $prefix$ be the string prefix for the namespace binding.
This property has no value for the default namespace.

\item[namespace name] Let $namespaceName$ be the URI namespace name.

\end{description}
\begin{schema}{NamespaceItem}
	Item \\
	prefix : OptionalString \\
	namespace : URI
\where
	id \in NsII
\end{schema}
The identifier is a namespace information item identifier.

\section{Information Sets}

An infoset consists of a set of information items and their properties.

\subsection{Infoset Information Items}

An infoset has a set of information items, and each information item is
one of the eleven kinds. 

\subsection{InfosetItems}

Let $InfosetItems$ be the set of unconstrained sets of each of the eleven kinds
of information items:
\begin{schema}{InfosetItems}
	attributeItems : \finset AttributeItem \\
	characterItems : \finset CharacterItem \\
	commentItems : \finset CommentItem \\
	declarationItems : \finset DeclarationItem \\
	documentItems : \finset DocumentItem \\
	elementItems : \finset ElementItem \\
	entityItems : \finset EntityItem \\
	instructionItems : \finset InstructionItem \\
	namespaceItems : \finset NamespaceItem \\
	notationItems : \finset NotationItem \\
	referenceItems : \finset ReferenceItem
\end{schema}

\subsection{InfosetItems1}

Let $InfosetItems1$ be the set of infosets that satisfy the following additional constraints
on the number of items.
\begin{itemize}

\item Let $documentItem$ be the document information item.

\item Let $documentElementItem$ be the document element information item.

\end{itemize}
\begin{schema}{InfosetItems1}
	InfosetItems \\
	documentItem : DocumentItem \\
	documentElementItem : ElementItem
\where
	documentItems = \{documentItem\}
\also
	documentElementItem \in elementItems \\
	documentElementItem.id = documentItem.documentElement
\also
	\# declarationItems \leq 1
\end{schema}
\begin{itemize}

\item There is exactly one document information item.

\item There is at least one element information item.

\item The document element property of the document item refers to an element item in the infoset.

\item There is at most one DTD information item.

\end{itemize}

\subsection{InfosetIds}

It is useful to define the sets of identifiers that are present for
each kind of information item.

Let $InfosetIds$ be the set of infosets with the sets of identifiers defined:
\begin{schema}{InfosetIds}
	InfosetItems1 \\
	attributeIds : \finset AII \\
	characterIds : \finset ChII \\
	commentIds : \finset CII \\
	declarationIds : \finset DTDII \\
	documentIds : \finset DII \\
	elementIds : \finset EII \\
	entityIds : \finset UEII \\
	instructionIds : \finset PIII \\
	namespaceIds : \finset NsII \\
	notationIds : \finset NII \\
	referenceIds : \finset UERII
\where
	attributeIds = \{~item : attributeItems @ item.id~\} \\
	characterIds = \{~item : characterItems @ item.id~\} \\
	commentIds = \{~item : commentItems @ item.id~\} \\
	declarationIds = \{~item : declarationItems @ item.id~\} \\
	documentIds = \{~item : documentItems @ item.id~\} \\
	elementIds = \{~item : elementItems @ item.id~\} \\
	entityIds = \{~item : entityItems @ item.id~\} \\
	instructionIds = \{~item : instructionItems @ item.id~\} \\
	namespaceIds = \{~item : namespaceItems @ item.id~\} \\
	notationIds = \{~item : notationItems @ item.id~\} \\
	referenceIds = \{~item : referenceItems @ item.id~\}
\end{schema}
Each set of identifiers is equal to the set of values that appear
in the id property of the corresponding set of information items.

\subsection{InfosetUniqueIds}

Each information information is uniquely identified by its identifier.

Let $InfosetUniqueIds$ be the set of infosets that have unique indentifiers:
\begin{schema}{InfosetUniqueIds}
	InfosetIds
\where
	\# attributeIds = \# attributeItems \\
	\# characterIds = \# characterItems \\
	\# commentIds = \# commentItems \\
	\# declarationIds = \# declarationItems \\
	\# documentIds = \# documentItems \\
	\# elementIds = \# elementItems \\
	\# entityIds = \# entityItems \\
	\# instructionIds = \# instructionItems \\
	\# namespaceIds = \# namespaceItems \\
	\# notationIds = \# notationItems \\
	\# referenceIds = \# referenceItems
\end{schema}
The identifiers are unique if and only if the number of identifiers
is equal to the number of information items.

\subsection{InfosetAllIds}

It is useful to define the set of all identifiers that appear in an infoset.
Let $InfosetAllIds$ be the set of infosets the set of all identifiers defined.
Let $ids$ be the set of all information item identifiers in the infoset.
\begin{schema}{InfosetAllIds}
	InfosetUniqueIds \\
	ids : \finset_1 II
\where
	\langle attributeIds, characterIds, commentIds, declarationIds, \\
	\t1	documentIds, elementIds, entityIds, namespaceIds, \\
	\t1	notationIds, referenceIds \rangle \partition ids
\end{schema}
The set of all identifiers is composed of the identifiers from each kind of information item.

\subsection{InfosetMaps}

Since each information item is uniquely identified by its id, it is possible
to look up the information item given its id.

Let $InfosetMaps$ be the set of infosets with the lookup maps defined:
\begin{schema}{InfosetMaps}
	InfosetAllIds \\
	attributeMap : AII \pfun AttributeItem \\
	characterMap : ChII \pfun CharacterItem \\
	commentMap : CII \pfun CommentItem \\
	declarationMap : DTDII \pfun DeclarationItem \\
	documentMap : DII \pfun DocumentItem \\
	elementMap : EII \pfun ElementItem \\
	entityMap : UEII \pfun EntityItem \\
	instructionMap : PIII \pfun InstructionItem \\
	namespaceMap : NsII \pfun NamespaceItem \\
	notationMap : NII \pfun NotationItem \\
	referenceMap : UERII \pfun ReferenceItem
\where
	attributeMap = \{~item : attributeItems @ item.id \mapsto item~\} \\
	characterMap = \{~item : characterItems @ item.id \mapsto item~\} \\
	commentMap = \{~item : commentItems @ item.id \mapsto item~\} \\
	declarationMap = \{~item : declarationItems @ item.id \mapsto item~\} \\
	documentMap = \{~item : documentItems @ item.id \mapsto item~\} \\
	elementMap = \{~item : elementItems @ item.id \mapsto item~\} \\
	entityMap = \{~item : entityItems @ item.id \mapsto item~\} \\
	instructionMap = \{~item : instructionItems @ item.id \mapsto item~\} \\
	namespaceMap = \{~item : namespaceItems @ item.id \mapsto item~\} \\
	notationMap = \{~item : notationItems @ item.id \mapsto item~\} \\
	referenceMap = \{~item : referenceItems @ item.id \mapsto item~\}
\end{schema}
Each map maps the identifier of an item to that item.

\subsection{Relations Between Information Items}

Some of the properties of information items, for example $parent$ and
$attributes$, refer to other information items. 
Clearly, the items refered to by
these properties must also belong to the infoset.
Therefore, these properties define binary relations on the set of information
items.
Also, some of the properties have inverse properties, for example $parent$ and
$children$ are inverse properties.
Table~\ref{relations} summarizes all the properties that define relations, and
indicates the inverse relation where one exists.
\begin{table}
\begin{tabular}{|l|l|l|l|}
\hline
Domain & Property & Range & Inverse \\
\hline
$DII$ & $children$ & $EII$   & $parent$ \\
      &            & $PIII$  &          \\
      &            & $CII$   &          \\
      &            & $DTDII$ &          \\
\cline{2-4}
      & $documentElement$ & $EII$ & $parent$ \\
\cline{2-4}
      & $notations$ & $NII$ & n/a \\
\cline{2-4}
      & $unparsedEntities$ & $UEII$ & n/a \\
\hline
$EII$ & $children$ & $EII$   & $parent$ \\
      &            & $PIII$  &          \\
      &            & $UERII$ &          \\
      &            & $ChII$  &          \\
      &            & $CII$   &          \\
\cline{2-4}
      & $attributes$ & $AII$ & $ownerElement$ \\
\cline{2-4}
      & $namespaceAttributes$ & $AII$ & $ownerElement$ \\
\cline{2-4}
      & $inScopeNamespaces$ & $NsII$ & n/a \\
\cline{2-4}
      & $parent$ & $DII$ & $children$ \\
      &          & $EII$ &            \\
\hline
$AII$ & $references$ & $EII$  & n/a \\
      &              & $UEII$ &     \\
      &              & $NII$  &     \\
\cline{2-4}
      & $ownerElement$ & $EII$ & $attributes$ \\ 
      &                  &       & $namespaceAttributes$ \\
\hline
$PIII$ & $notation$ & $NII$ & n/a \\
\cline{2-4}
       & $parent$ & $DII$   & $children$ \\
       &          & $EII$   &            \\
       &          & $DTDII$ &            \\
\hline
$UERII$ & $parent$ & $EII$ & $children$ \\
\hline
$ChII$ & $parent$ & $EII$ & $children$ \\
\hline
$CII$ & $parent$ & $DII$ & $children$ \\
      &          & $EII$ &            \\
\hline
$DTDII$ & $children$ & $PIII$ & $parent$ \\
\cline{2-4}
        & $parent$ & $DII$ & $children$ \\
\hline
$UEII$ & $notation$ & $NII$ & n/a \\
\hline
\end{tabular}
\caption{Relations Between Information Items} \label{relations}
\end{table}

Each relation has an associated range constraint and, if an inverse relation
exists, an inverse relation constraint.
These constraints are defined in the following sections.

\subsubsection{InfosetDocumentChildren}

Let $InfosetDocumentChildren$ be the set of infosets that satisfy the constraints
on the document information item $children$ property:
\begin{schema}{InfosetDocumentChildren}
	InfosetMaps
\where
	\forall child : \ran documentItem.children @ \\
	\t1	child \in elementIds \cup instructionIds \cup \\
	\t2		commentIds \cup declarationIds \land \\
	\t1	child \in elementIds \implies \\
	\t2		(elementMap~child).parent = documentItem.id \land \\
	\t1	child \in instructionIds \implies \\
	\t2		(instructionMap~child).parent = documentItem.id \land \\
	\t1	child \in commentIds \implies \\
	\t2		(commentMap~child).parent = documentItem.id \land \\
	\t1	child \in declarationIds \implies \\
	\t2		(declarationMap~child).parent = documentItem.id 
\end{schema}
\begin{itemize}

\item Each child of the document information item is either an element, processing
instruction, comment, or DTD information item in the infoset.

\item The parent of each child of the document information item is the
document information item.

\end{itemize}

\subsubsection{InfosetDocumentDocumentElement}

Let $InfosetDocumentDocumentElement$ be the set of infosets that satisfy the
constraints on the document information item $documentElement$ property:
\begin{schema}{InfosetDocumentDocumentElement}
	InfosetMaps
\where
	documentElementItem.parent = documentItem.id
\end{schema}
The parent of the document element is the document information item.

\subsubsection{InfosetDocumentNotations}

Let $InfosetDocumentNotations$ be the set of infosets that satisfy the constraints
on the document information item $notations$ property:
\begin{schema}{InfosetDocumentNotations}
	InfosetMaps
\where
	documentItem.notations = notationIds
\end{schema}
The value of the notations property 
of the document information item is the set of all
notation information item identifiers in the infoset.

\subsubsection{InfosetDocumentUnparsedEntities}

Let $InfosetDocumentUnparsedEntities$ be the set of infosets that satisfy the
constraints on the document information item $unparsed\_entity$ property:
\begin{schema}{InfosetDocumentUnparsedEntities}
	InfosetMaps
\where
	documentItem.unparsedEntities = entityIds
\end{schema}
The value of the unparsed entities property
of the document information item is the set of all
unparsed entity information item identifiers in the infoset.

\subsubsection{InfosetDocument}

Let $InfosetDocument$ be the set of infosets that satisfy all the constraints on the
document entity properties:
\begin{zed}
	InfosetDocument \defs \\
	\t1	InfosetDocumentChildren \land \\
	\t1	InfosetDocumentDocumentElement \land \\
	\t1	InfosetDocumentNotations \land \\
	\t1	InfosetDocumentUnparsedEntities
\end{zed}

\subsubsection{InfosetElementChildren}

Let $InfosetElementChildren$ be the set of all infosets that satisfy the
constraints on the element information item $children$ property:
\begin{schema}{InfosetElementChildren}
	InfosetMaps
\where
	\forall item : elementItems; child : II | \\
	\t1	child \in \ran item.children @ \\
	\t1	child \in elementIds \cup instructionIds \cup referenceIds \cup \\
	\t2		commentIds \cup characterIds \land \\
	\t1	child \in elementIds \implies \\
	\t2		(elementMap~child).parent = item.id \land \\
	\t1	child \in instructionIds \implies \\
	\t2		(instructionMap~child).parent = item.id \land \\
	\t1	child \in referenceIds \implies \\
	\t2		(referenceMap~child).parent = item.id \land \\
	\t1	child \in commentIds \implies \\
	\t2		(commentMap~child).parent = item.id \land \\
	\t1	child \in characterIds \implies \\
	\t2		(characterMap~child).parent = item.id
\end{schema}
\begin{itemize}

\item Each child of each element information item in the infoset is either an
element, processing instruction, unexpanded entity reference, comment, or character
information item in the infoset.

\item The parent of each child of each element information item in the infoset
is that element information item.

\end{itemize}

\subsubsection{InfosetElementAttributes}

Let $InfosetElementAttributes$ be the set of infosets that satisfy the constraints
on the element information item $attributes$ property:
\begin{schema}{InfosetElementAttributes}
	InfosetMaps
\where
	\forall item : elementItems; id: AII | \\
	\t1	id \in item.attributes @ \\
	\t1	id \in attributeIds \land \\
	\t1	(attributeMap~id).ownerElement = item.id
\end{schema}
\begin{itemize}

\item Each attribute of each element information item in the infoset is an
attribute information item in the infoset.

\item The owner element of each attribute of each element information item in the
infoset is that element information item.

\end{itemize}

\subsubsection{InfosetElementNamespaceAttributes}

Let $InfosetElementNamespaceAttributes$ be the set of infosets that satisfy the constraints
on the element information item $namespaceAttributes$ property:
\begin{schema}{InfosetElementNamespaceAttributes}
	InfosetMaps
\where
	\forall item : elementItems; id: AII | \\
	\t1	id \in item.namespaceAttributes @ \\
	\t1	id \in attributeIds \land \\
	\t1	(attributeMap~id).ownerElement = item.id
\end{schema}
\begin{itemize}

\item Each namespace attribute of each element information item in the infoset is an
attribute information item in the infoset.

\item The owner element of each namespace attribute of each element information item in the
infoset is that element information item.

\end{itemize}

\subsubsection{InfosetElementInScopeNamespaces}

Let $InfosetElementInScopeNamespaces$ be the set of infosets that satisfy the constraints
on the element information item $inScopeNamespaces$ property:
\begin{schema}{InfosetElementInScopeNamespaces}
	InfosetMaps
\where
	\forall item : elementItems @ \\
	\t1	item.inScopeNamespaces \subseteq namespaceIds
\also
	\forall id : namespaceIds @ \\
	\t1	\exists item : elementItems @ \\
	\t2		id \in item.inScopeNamespaces
\end{schema}
\begin{itemize}

\item The in scope namespaces of each element information item in the infoset are in the infoset.

\item Each namespace information item in the infoset is in the scope of some element
information item in the infoset.

\end{itemize}

\subsubsection{InfosetElementParent}

Let $InfosetElementParent$ be the set of all infosets that satisfy the
constraints on the element information item $parent$ property:
\begin{schema}{InfosetElementParent}
	InfosetMaps
\where
	\forall item : elementItems @ \\
	\t1	item.parent \in documentIds \cup elementIds \land \\
	\t1	item.parent \in documentIds \implies \\
	\t2		item.id \in \ran (documentMap~item.parent).children \land \\
	\t1	item.parent \in elementIds \implies \\
	\t2		item.id \in \ran (elementMap~item.parent).children
\end{schema}
\begin{itemize}

\item The parent of each element information item in the infoset is either a
document or element information item in the infoset.

\item Each element in the infoset is one of the children of its parent.

\end{itemize}

\subsubsection{InfosetElement}

Let $InfosetElement$ be the set of infosets that satisfy all the constraints on the
element properties:
\begin{zed}
	InfosetElement \defs \\
	\t1	InfosetElementChildren \land \\
	\t1	InfosetElementAttributes \land \\
	\t1	InfosetElementNamespaceAttributes \land \\
	\t1	InfosetElementInScopeNamespaces \land \\
	\t1	InfosetElementParent
\end{zed}

\subsubsection{InfosetAttributeReferences}

Let $InfosetAttributeReferences$ be the set of all infosets that satisfy the
contraints on the attribute information item $references$ propoerty:
\begin{schema}{InfosetAttributeReferences}
	InfosetMaps
\where
	\forall item : attributeItems; refs: \seq II; id : II | \\
	\t1	item.references = valueIIs~refs @ \\
	\t1	\ran refs \subseteq elementIds \cup entityIds \cup notationIds
\end{schema}
Each reference in each attribute information item in the infoset 
refers to either an element, unparsed entity, or notation in the infoset.

\subsubsection{InfosetAttributeOwnerElement}

Let $InfosetAttributeOwnerElement$ be the set of all infosets that satisfy the
constraints on the attribute information item $ownerElement$ property:
\begin{schema}{InfosetAttributeOwnerElement}
	InfosetMaps
\where
	\forall item : attributeItems @ \\
	\t1	item.ownerElement \in elementIds \land \\
	\t1	(\LET owner == elementMap~item.ownerElement @ \\
	\t2		item.id \in owner.attributes \lor \\
	\t2		item.id \in owner.namespaceAttributes)
\end{schema}
\begin{itemize}

\item The owner element of each attribute information item in the infoset is
an element information item in the infoset.

\item Each attribute information item in the infoset is in either the attributes
or namespace attributes of its owner element.

\end{itemize}

\subsubsection{InfosetAttribute}

Let $InfosetAttribute$ be the set of infosets that satisfy all the constraints on the
attribute properties:
\begin{zed}
	InfosetAttribute \defs \\
	\t1	InfosetAttributeReferences \land \\
	\t1	InfosetAttributeOwnerElement
\end{zed}

\subsubsection{InfosetInstructionNotation}

Let $InfosetInstructionNotation$ be the set of all infosets that satisfy the
contraints on the processing instruction information item $notation$ propoerty:
\begin{schema}{InfosetInstructionNotation}
	InfosetMaps
\where
	\forall item : instructionItems; notation : NII | \\
	\t1	item.notation = valueII~notation@ \\
	\t1	notation \in notationIds
\end{schema}
The notation in each attribute information item in the infoset 
refers to notation in the infoset.

\subsubsection{InfosetInstructionParent}

Let $InfosetInstructionParent$ be the set of all infosets that satisfy the
constraints on the processing instruction information item $parent$ property:
\begin{schema}{InfosetInstructionParent}
	InfosetMaps
\where
	\forall item : instructionItems @ \\
	\t1	item.parent \in documentIds \cup elementIds \cup declarationIds \land \\
	\t1	item.parent \in documentIds \implies \\
	\t2		item.id \in \ran (documentMap~item.parent).children \land \\
	\t1	item.parent \in elementIds \implies \\
	\t2		item.id \in \ran (elementMap~item.parent).children \land \\
	\t1	item.parent \in declarationIds \implies \\
	\t2		item.id \in \ran (declarationMap~item.parent).children
\end{schema}
\begin{itemize}

\item The parent of each processing instruction information item in the infoset is either a
document, element, or DTD information item in the infoset.

\item Each processing instruction in the infoset is one of the children of its parent.

\end{itemize}

\subsubsection{InfosetInstruction}

Let $InfosetInstruction$ be the set of infosets that satisfy all the constraints on the
processing instruction properties:
\begin{zed}
	InfosetInstruction \defs \\
	\t1	InfosetInstructionNotation \land \\
	\t1	InfosetInstructionParent
\end{zed}

\subsubsection{InfosetReference}

Let $InfosetReference$ be the set of all infosets that satisfy the
constraints on the unexpanded entity reference information item $parent$ property:
\begin{schema}{InfosetReference}
	InfosetMaps
\where
	\forall item : referenceItems @ \\
	\t1	item.parent \in elementIds \land \\
	\t1	item.id \in \ran (elementMap~item.parent).children
\end{schema}
\begin{itemize}

\item The parent of each unexpanded entity reference information item in the infoset is an
element in the infoset.

\item Each unexpanded entity reference in the infoset is one of the children of its parent.

\end{itemize}

\subsubsection{InfosetCharacter}

Let $InfosetCharacter$ be the set of all infosets that satisfy the
constraints on the character information item $parent$ property:
\begin{schema}{InfosetCharacter}
	InfosetMaps
\where
	\forall item : characterItems @ \\
	\t1	item.parent \in elementIds \land \\
	\t1	item.id \in \ran (elementMap~item.parent).children
\end{schema}
\begin{itemize}

\item The parent of each character information item in the infoset is an
element in the infoset.

\item Each character in the infoset is one of the children of its parent.

\end{itemize}

\subsubsection{InfosetComment}

Let $InfosetComment$ be the set of all infosets that satisfy the
constraints on the comment information item $parent$ property:
\begin{schema}{InfosetComment}
	InfosetMaps
\where
	\forall item : commentItems @ \\
	\t1	item.parent \in documentIds \cup elementIds \land \\
	\t1	item.parent \in documentIds \implies \\
	\t2		item.id \in \ran (documentMap~item.parent).children \land \\
	\t1	item.parent \in elementIds \implies \\
	\t2		item.id \in \ran (elementMap~item.parent).children
\end{schema}
\begin{itemize}

\item The parent of each comment information item in the infoset is either a
document or element information item in the infoset.

\item Each comment information item in the infoset is one of the children of its parent.

\end{itemize}

\subsubsection{InfosetDeclarationChildren}

Let $InfosetDeclarationChildren$ be the set of infosets that satisfy the constraints
on the DTD information item $children$ property:
\begin{schema}{InfosetDeclarationChildren}
	InfosetMaps
\where
	\forall item : declarationItems; child : II | \\
	\t1	child \in \ran item.children @ \\
	\t1	child \in instructionIds \land \\
	\t1	(instructionMap~child).parent = item.id
\end{schema}
\begin{itemize}

\item Each child of each DTD information item is a processing
instruction information item in the infoset.

\item The parent of each child of each DTD information item is the
DTD information item.

\end{itemize}

\subsubsection{InfosetDeclarationParent}

Let $InfosetDeclarationParent$ be the set of all infosets that satisfy the
constraints on the DTD information item $parent$ property:
\begin{schema}{InfosetDeclarationParent}
	InfosetMaps
\where
	\forall item : declarationItems @ \\
	\t1	item.parent = documentItem.id \land \\
	\t1	item.id \in \ran documentItem.children
\end{schema}
\begin{itemize}

\item The parent of each DTD information item in the infoset is the
document item of the infoset.

\item Each DTD in the infoset is one of the children of its parent.

\end{itemize}

\subsubsection{InfosetDeclaration}

Let $InfosetDeclaration$ be the set of infosets that satisfy all the constraints on the
DTD properties:
\begin{zed}
	InfosetDeclaration \defs \\
	\t1	InfosetDeclarationChildren \land \\
	\t1	InfosetDeclarationParent
\end{zed}

\subsubsection{InfosetEntity}

Let $InfosetEntity$ be the set of all infosets that satisfy the
contraints on the unparsed entity information item $notation$ propoerty:
\begin{schema}{InfosetEntity}
	InfosetMaps
\where
	\forall item : entityItems; notation : NII | \\
	\t1	item.notation = valueII~notation@ \\
	\t1	notation \in notationIds
\end{schema}
The notation in each unparsed entity information item in the infoset 
refers to a notation in the infoset.

\subsection{InfosetRelations}

Let $InfosetRelations$ be the set of all infosets that satisfy all the
relation constraints:
\begin{zed}
	InfosetRelations \defs \\
	\t1	InfosetDocument \land \\
	\t1	InfosetElement \land \\
	\t1	InfosetAttribute \land \\
	\t1	InfosetInstruction \land \\
	\t1	InfosetReference \land \\
	\t1	InfosetCharacter \land \\
	\t1	InfosetComment \land \\
	\t1	InfosetDeclaration \land \\
	\t1	InfosetEntity
\end{zed}

\subsection{Infoset}

Finally, the parent property in a valid infoset defines a tree structure on 
a subset of the items.
Let $Infoset$ be the set of infosets for which the parent property
defines a valid tree structure:
\begin{itemize}

\item Let $parent$ be the mapping that sends a descendent node to its parent node.

\item Let $nodes$ be subset of information items that form the nodes of the tree.
The set is never empty since it always contains the document and document element items.

\item Let $root$ be the root of the tree.
This is the document item.

\item Let $descendents$ be the set of nodes that are reachable from the root.
This set is never empty since it always contains the document element item.

\end{itemize}
\begin{schema}{Infoset}
	InfosetRelations \\
	parent : II \pfun II \\
	descendents : \finset_1 II \\
	root : II \\
	nodes : \finset_1 II
\where
	parent = \\
	\t1	(\lambda id : elementIds @ (elementMap~id).parent) \cup \\
	\t1 	(\lambda id : instructionIds @ (instructionMap~id).parent) \cup \\
	\t1 	(\lambda id : referenceIds @ (referenceMap~id).parent) \cup \\
	\t1 	(\lambda id : characterIds @ (characterMap~id).parent) \cup \\
	\t1 	(\lambda id : commentIds @ (commentMap~id).parent) \cup \\
	\t1 	(\lambda id : declarationIds@ (declarationMap~id).parent)
\also
	descendents = \dom parent \\
	\{root\} = \ran parent \setminus descendents \\
	\langle \{root\}, descendents \rangle \partition nodes \\
	\dom (parent \plus \rres \{root\}) = descendents
\end{schema}
\begin{itemize}

\item The parent mapping is the union of all the parent properties.

\item Each descendent information item has a unique parent information item.

\item The root information item is the only information item that is not a descendent of any other information item.

\item Each node is either the root or a descendent.

\item Each descendent is directly or indirectly connected to the root via the parent mapping.

\end{itemize}

The preceeding constraints imply that each item in the infoset is reachable, either directly or indirectly, from the document element.
Each element, processing instruction, comment, DTD, character, and unexpanded entity reference information
item is reachable, either directly or indirectly from the document element via the children property.
Each notation information item in the infoset is reachable from the document element via the notations property.
Each unparsed entity information item in the infoset is reachable from the document element via the unparsed entities property.
Each attribute information item in the infoset is reachable from some element information item via either the 
attributes or the namespace attributes property.
Each namespace information item in the infoset is reachable from some element information item via the 
in scope namespaces property.

\end{document}
