Sequence reversion
Function
context
$ X $ … set
definiendum
$ \mathrm{rev}: \mathrm{FiniteSequence}(X)\to\mathrm{FiniteSequence}(X) $
postulate
$ \pi_n(\mathrm{length}(S))=\pi_{\mathrm{length}(S)+1-n}(S)$
Discussion
Parents
Subset of
Idempotent function
Context
Sequence length