# Sequence Length Function

A Sequence Length Function is a length function that is restricted to sequences (a count function that maps a sequence to a non-negative number of the count of the symbols in the sequence)

**Context:****Example(s):****See:**Set Cardinality Function, Infinite Sequence.

## References

- http://www.isi.edu/~hobbs/bgt-sequences.text
- We define "length" as follows:
`(12)`

- We define "length" as follows:

(forall (n s)
(if (sequence s)
(iff (length n s)
(exists (s1 s2)
(and (function0 s s1 s2)(ints s1 1 n))))))

```
```