I would like to know what is a correct formal notation for representing a state where the state is defined by
$ K \to (V x N)$
where K is the key, V is the value and N is the infinite ordered set of version numbers. An injective function f takes an element of N and returns the next version number.