# Predicates on Sequences

Boolean valued operators and functions on enumerated sequences exist to test whether entries are defined (see previous section), to test for membership and containment, and to compare sequences with respect to an ordering on its entries. On formal sequences, only element membership can be tested.

## `IsComplete(S): SeqEnum -> BoolElt`

Boolean valued function, returning `true` if and only if each of the terms $S[i]$ for $1\leq i\leq \#S$ is defined, for an enumerated sequence $S$.

## `IsDefined(S, i): SeqEnum, RngIntElt -> BoolElt`

Given an enumerated sequence $S$ and an index $i$, this returns `true` if and only if $S[i]$ is defined. (Hence the result is `false` if $i>\#S$, but an error results if $i<1$.) Note that the index $i$ is allowed to be a multi-index; if $i=[i_1, \ldots, i_r]$ is a multi-index and $i_j>\#S[i_1, \ldots, i_{j-1}]$ the function returns false, but if $S$ is $s$ levels deep and $r>s$ while $i_j\leq \#S[i_1, \ldots, i_{j-1}]$ for $1\leq j\leq s$, then an error occurs.

## `IsEmpty(S): SeqEnum -> BoolElt`

Boolean valued function, returning `true` if and only if the enumerated sequence $S$ is empty.

## `IsNull(S): SeqEnum -> BoolElt`

Boolean valued function, returning `true` if and only if the enumerated sequence $S$ is empty and its universe is undefined, `false` otherwise.

## Membership Testing

Here, $S$ and $T$ denote sequences. The element $x$ is always assumed to be compatible with $S$.

### `x in S: Elt, SeqEnum -> BoolElt`

Returns `true` if the object $x$ occurs as a term of the enumerated or formal sequence $S$, `false` otherwise. If $x$ is not in the universe of $S$, coercion is attempted. If that fails, an error results.

### `x notin S: Elt, SeqEnum -> BoolElt`

Returns `true` if the object $x$ does not occur as a term of the enumerated or formal sequence $S$, `false` otherwise. If $x$ is not in the universe of $S$, coercion is attempted. If that fails, an error results.

### `IsSubsequence(S, T): SeqEnum, SeqEnum -> BoolElt`

### `IsSubsequence(S, T: Kind := option): SeqEnum, SeqEnum, MonStgElt -> BoolElt`

```magma
Kind: MonStgElt                    Default: "Consecutive"
```

Returns `true` if the enumerated sequence $S$ appears as a subsequence of consecutive elements of the enumerated sequence $T$, `false` otherwise. By changing the default value `"Consecutive"` of the parameter `Kind` to `"Sequential"` or to `"Setwise"`, this returns `true` if and only if the elements of $S$ appear in order (but not necessarily consecutively) in $T$, or if and only if all elements of $S$ appear as elements of $T$; so in the latter case the test is merely whether the set of elements of $S$ is contained in the set of elements of $T$. If the universes of $S$ and $T$ are not the same, coercion is attempted.

### `S eq T: SeqEnum, SeqEnum -> BoolElt`

Returns `true` if the enumerated sequences $S$ and $T$ are equal, `false` otherwise. If the universes of $S$ and $T$ are not the same, coercion is attempted.

### `S ne T: SeqEnum, SeqEnum -> BoolElt`

Returns `true` if the enumerated sequences $S$ and $T$ are not equal, `false` otherwise. If the universes of $S$ and $T$ are not the same, coercion is attempted.

## Testing Order Relations

Here, $S$ and $T$ denote complete enumerated sequences with universe $U$ and $V$ respectively, such that a common overstructure $W$ for $U$ and $V$ can be found (as outlined in the Introduction), and such that on $W$ an ordering on the elements is defined allowing the Magma operators `eq` (=), `le` ($\leq$), `lt` ($<$), `gt` ($>$), and `ge` ($\geq$) to be invoked on its elements.

With these comparison operators the *lexicographical* ordering is used to order complete enumerated sequences. Sequences $S$ and $T$ are equal (`S eq T`) if and only if they have the same length and all terms are the same. A sequence $S$ precedes $T$ (`S lt T`) in the ordering imposed by that of the terms if at the first index $i$ where $S$ and $T$ differ then $S[i] < T[i]$. If the length of $T$ exceeds that of $S$ and $S$ and $T$ agree in all places up to the length of $S$, then `S lt T` is true also. In all other cases where $S\ne T$ one has `S gt T`.

### `S lt T: SeqEnum, SeqEnum -> BoolElt`

Returns `true` if the sequence $S$ precedes the sequence $T$ under the ordering induced from $S$, `false` otherwise. Thus, `true` is returned if and only if either $S[k] < T[k]$ and $S[i] = T[i]$ (for $1\leq i< k$) for some $k$, or $S[i] = T[i]$ for $1\leq i\leq \#S$ and $\#S < \#T$.

### `S le T: SeqEnum, SeqEnum -> BoolElt`

Returns `true` if the sequence $S$ either precedes the sequence $T$, under the ordering induced from $S$, or is equal to $T$, `false` otherwise. Thus, `true` is returned if and only if either $S[k] < T[k]$ and $S[i] = T[i]$ (for $1\leq i< k$) for some $k$, or $S[i] = T[i]$ for $1\leq i\leq \#S$ and $\#S\leq\#T$.

### `S ge T: SeqEnum, SeqEnum -> BoolElt`

Returns `true` if the sequence $S$ either comes after the sequence $T$, under the ordering induced from $S$, or is equal to $T$, `false` otherwise. Thus, `true` is returned if and only if either $S[k] > T[k]$ and $S[i] = T[i]$ (for $1\leq i< k$) for some $k$, or $S[i] = T[i]$ for $1\leq i\leq \#T$ and $\#S\geq\#T$.

### `S gt T: SeqEnum, SeqEnum -> BoolElt`

Returns `true` if the sequence $S$ comes after the sequence $T$ under the ordering induced from $S$, `false` otherwise. Thus, `true` is returned if and only if either $S[k] > T[k]$ and $S[i] = T[i]$ (for $1\leq i< k$) for some $k$, or $S[i] = T[i]$ for $1\leq i\leq \#T$ and $\#S > \#T$.