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

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\).