Lessons learnt #7
Description
Avoid assumptions when describing the behaviour of a TM, instead use a plain tm.eval tapes = ... and use conditionals or default values on the rhs.
Requiring [a, b, c].get.Injective is much easier to deal with than a ≠ b ∧ b ≠ c ∧ a ≠ c.
Allocating auxiliary tapes is tricky.
Use dyadic numbers instead of binary since encoding is a bijection.
Loops are what is tricky.