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

Draft

barni120400 wants to merge 6 commits into

leanprover:mainfrom

barni120400:multitape/ntm-deterministic

Commits on Aug 20, 2026

refactor(MultiTapeTM): Put the output tape into the configuration

avivbarnatan-air
and
claude
committed
2b62c21
refactor(MultiTapeTM): Rename `configs` to `runFrom`

avivbarnatan-air
and
claude
committed
794c978
docs(MultiTapeTM): address review comments

avivbarnatan-air
and
claude
committed
3f015fb
feat(MultiTapeTM): Nondeterministic multi-tape Turing machines

avivbarnatan-air
and
claude
committed
e9426ed
refactor(MultiTapeTM): Make the deterministic machine a nondeterministic one

avivbarnatan-air
and
claude
committed
94bfea4
refactor(MultiTapeTM): Split Run out of Computation and generalise the space measures

avivbarnatan-air
and
claude
committed
a03c9d4