refactor(MultiTapeTM): Make the deterministic machine a nondeterministic one

[barni120400]

Builds on #820. GitHub shows that PR's commit too, since its branch is not on this repository and cannot be used as a base. Only the commits after 3e67a9b belong here, and they are exactly:

barni120400/cslib@multitape/ntm...multitape/ntm-deterministic

MultiTapeTM now extends MultiTapeNTM, permitting exactly the transition its transition function prescribes, with ofTr building one from a transition function. Everything defined for the nondeterministic machine therefore applies to it directly: initCfg and ComputesInTimeAndSpace are no longer defined for it, Step, ComputationPath and the Computes notions are available on it unchanged, and the separate embedding file is gone.

What is left is what follows from there being no choice to make. step_iff identifies the inherited Step with the graph of step; a computation path can then only follow runFrom, and runPath supplies one of every length, giving computesInExactTimeAndSpace_iff_runFrom. The previous embedding proved one direction of that; it is now an equivalence, so runFrom, spaceUsed and the TapeLemmas results keep their meaning.

Then several things move out of the deterministic file, because none of them were deterministic:

• Stepping. step and Step each carried the same case analysis, differing only in choosing an action by a function or by a relation. Cfg.stepWith, Cfg.StepWith and Cfg.stepWith_iff state that once in Configuration.lean, which mentions no machine. Both machines then define a step in a line, and step_iff is that lemma applied.
• What a step does to a tape. workTapePos_step_le and step_workTapes_eq_of_ne hold because of what applying an action does, not because of determinism. They are now stated of Action.apply and of Step, and the deterministic machine gets them by its own step being one of those steps.
• The space bounds, whose proofs are cardinality arguments about a list of configurations. spaceUsedOfCfgs_le and spaceUsedOfCfgs_mono give ComputationPath.space_le, a bound for nondeterministic machines that the library did not have, and leave spaceUsed_linear and spaceUsed_mono as corollaries.

spaceUsed was describing what ComputationPath.space already described, so it is now that: the space of the machine's own run, (tm.runPath cfg t).space. The three views agree by rfl — a path's space, a sum over the tapes, and spaceUsedOfCfgs of the configurations passed through.

Two changes to Nondeterministic.lean that a reader of #820 should see called out:

1. ComputationPath gains nothing and loses its endpoints. It designated one end and not the other, so the two ends of one list were described in two different ways. It is now a non-empty list whose consecutive elements are joined by a step, with start and last read off it. Fixing the endpoints was the only thing IsChainFromTo added over IsChain and non-emptiness, so it is no longer used here; ComputesSuchThat asks that a path start at the initial configuration, which the type used to carry.
2. A path may start anywhere, which is what lets spaceUsed and the results about it be read off one.

Also removes declarations nothing referred to (runFrom_add, runFrom_output_eq_of_halt, spaceUsedByTape_le_spaceUsed, spaceUsed_zero_tapes_eq_zero, outputSymbol_of_halt, step_output, outputSymbol, haltsAtStep, halting_step_unique, not_halts_of_repeat_nonhalt) and TransitionRelation, which was the graph of step and so is the inherited Step; relatesInSteps_iff_runFrom_eq is stated over Step.

NB: claude was used heavily throughout.