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.
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.Injectiveis much easier to deal with thana ≠ 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.