@ -274,3 +274,84 @@ and will become \\(v - \\{c\\}\\).

If all of these conditions are met, our program, starting at \\((c, a, v)\\), will terminate in the state \\((c'', a'', v'')\\). This third rule completes our semantics; a program being executed will keep running instructions using the third rule, until it finally

hits an invalid program counter (terminating with the first rule) or gets to the end of the program (terminating with the second rule).

#### Aside: Vectors and Finite \\(\mathbb{N}\\)

We'll be getting to the Coq implementation of our semantics soon, but before we do:

what type should \\(c\\) be? It's entirely possible for an instruction like \\(\\texttt{jmp} \\; -10000\\)

to throw our program counter way before the first instruction of our program, so at first, it seems

as though we should use an integer. But the prompt doesn't even specify what should happen in this

case - it only says an instruction shouldn't be run twice. The "valid set", although it may help resolve

this debate, is our invention, and isn't part of the original specification.

There is, however, something we can infer from this problem. Since the problem of jumping "too far behind" or

"too far ahead" is never mentioned, we can assume that _all jumps will lead either to a valid instruction,

or right to the end of a program_. This means that \\(c\\) is a natural number, with

{{<latex>}}

0 \leq c \leq \text{length}(p)

{{</latex>}}

In a language like Coq, it's possible to represent such a number. Since we've gotten familliar with

inference rules, let's present two rules that define such a number:

{{<latex>}}

\frac

{n \in \mathbb{N}^+}

{Z : \text{Fin} \; n}

\quad

\frac

{f : \text{Fin} \; n}

{S f : \text{Fin} \; (n+1)}

{{</latex>}}

This is a variation of the [Peano encoding](https://wiki.haskell.org/Peano_numbers) of natural numbers.

It reads as follows: zero (\\(Z\\)) is a finite natural number less than any positive natural number \\(n\\). Then, if a finite natural number

\\(f\\) is less than \\(n\\), then adding one to that number (using the successor function \\(S\\))

will create a natural number less than \\(n+1\\). We encode this in Coq as follows

([originally from here](https://coq.inria.fr/library/Coq.Vectors.Fin.html#t)):

```Coq

Inductive t : nat -> Set :=

| F1 : forall {n}, t (S n)

| FS : forall {n}, t n -> t (S n).

```

The `F1` constructor here is equivalent to our \\(Z\\), and `FS` is equivalent to our \\(S\\).

To represent positive natural numbers \\(\\mathbb{N}^+\\), we simply take a regular natural

number from \\(\mathbb{N}\\) and find its successor using `S` (simply adding 1). Again, we have

to explicitly use `forall` in our type signatures.

We can use a similar technique to represent a list with a known number of elements, known

in the Idris and Coq world as a vector. Again, we only need two inference rules to define such