Skip to content

feat(MultiTapeTM): the identity is computable in linear time and zero space - #885

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

feat(MultiTapeTM): the identity is computable in linear time and zero space#885
crei wants to merge 1 commit into
leanprover:mainfrom
crei:identity_complexity

Conversation

@crei

@crei crei commented Sep 8, 2026

Copy link
Copy Markdown
Collaborator

As a combinator, this might not look like a useful lemma, but it will together with some more results: It for example allows us to copy from one tape to another.

@crei
crei force-pushed the identity_complexity branch from a5c82fc to a584a76 Compare September 8, 2026 18:09
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.

1 participant