Skip to content

feat(MultitapeTM): Prove an exponential upper bound in the number of configurations reachable in bounded space - #772

Open
crei wants to merge 1 commit into
leanprover:mainfrom
crei:configs_reachable_in_bounded_space
Open

feat(MultitapeTM): Prove an exponential upper bound in the number of configurations reachable in bounded space#772
crei wants to merge 1 commit into
leanprover:mainfrom
crei:configs_reachable_in_bounded_space

Conversation

@crei

@crei crei commented Aug 3, 2026

Copy link
Copy Markdown
Collaborator

Proves an upper bound on the number of configurations reachable in bounded space on a multi-tape TM.

The proof introduces a structure that uses a different index set for the tapes and proves equivalence, then shows that a finite index set that depends on the space bound is sufficient.

@crei

crei commented Aug 19, 2026

Copy link
Copy Markdown
Collaborator Author

#819 should be merged first, I'll update this one in a minute.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants