Start Bit Machine evaluation with TCOon

[roconnor-blockstream]

There is no good reason not to start with TCOon at https://github.com/ElementsProject/simplicity/blob/6adfd252ececd613203d051d4fc75dd427578e2c/C/eval.c#L357. This could potentially reduce the maximum number of frames needed by 1. It could also reduce the number of cells needed in cases where the Bit Machine is started with a non-trivial input.

Update the Simplicity Tech Report's correctness theorems (e.g. Theorem 3.8 an any copies of it and the theorems about the correctness of static analysis) to focus on the TCOon special case instead of the TCOoff special case

[roconnor-blockstream]

I suppose there is an issue that the current definition of the Bit Machine requires that there is always some active read frame, and starting with TCOon would end in a state where there is no active read frame.