sequences as mappings of an index.

Definition Let s, i, x be an instance of Sequence and xs be in s x, then we call xs finite if and only if the evaluation of lengthN xs terminates and will not end up in an exception.

Property Let s, i, x be an instance of Sequence, then holds:

1. For all xs in s x holds:

   1. graph is constant in its first parameter.
   2. If xs is finite, then lengthN xs == lengthN (graph p xs) for any p.

2. For all xs in s x holds:

   1. list is constant in its first parameter.
   2. For all ..(x,i):(x,j).. in xs holds: i < j.
   3. If xs is finite, then lengthN xs == lengthN (list p xs) for any p.
3. Let xs be in s x and i in i, then holds: there exists an x in x with xs ? i matches Just x if and only if there exists an (i',x) in graph (Just i) xs such that i == i'.

Note The first parameter of graph - respectively list - serves only as a proxy and as such it is only relevant on the type level.

the indexed list of the sequence.

the i-th element of the sequence.

Property Let xs be in s x and i in i for a instance of Sequence s i x, then holds: If i is in the support of xs then xs ? i is the i-th item of xs, else its evaluation will end up by throwing a IndexOutOfSupport-exception.

checks for being empty.

the span of a sequence.

the support of a sequence, i.e. all the indices which are not mapped to Nothing.

the image of a sequence, i.e. all the entities are hit by the mapping.

constructable sequences.

mapping the indices according to the given set.

sequence exceptions which are sub exceptions from SomeOAlgException.