OAI/Computability/PerfectCompleteness/Machines/PostfixAlignment.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens line 14
2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens line 21
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_length line 24
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_rename line 28
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_nil line 32
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_cons line 35
7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_length line 38
8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.compileTokens_append line 45
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.compile_exprTokens line 72
10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.compile_forestTokens line 108
11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_lowered_ordered line 122
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_lowered_ordered line 126
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_preserves_root_suffix line 130
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.expr_inputBits line 142
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forest_inputBits line 147
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forest_gateRecords_alignment line 152
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.tokenWords_length_le line 160
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_member line 176
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.expr_tokenWords_bounded line 205
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forest_tokenWords_bounded line 218
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forest_tokenBits_length_le line 226
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixAlignment.forest_inputBits_length_le line 236