OAI/Combinatorics/IndependentSets/Machines/Remaining2.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.remaining line 11
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.remaining_zero line 13
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.remaining_done line 14
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.remaining_cons line 16
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.inputBlocks line 22
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.outputBlocks line 25
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.vertexBlock_codec line 28
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.encodeWords_flatMap line 34
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.inputBlocks_codec line 40
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.outputBlocks_codec line 47
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.input_table_codec line 53
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.output_table_codec line 64
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.loopSteps line 76
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.loopTrace line 84
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.totalSteps line 125
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.tableTrace line 129
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.dummyRows_length_le line 144
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.bodySteps_le line 155
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.output_length_le line 276
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.loopSteps_le line 293
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.timePolynomial line 325
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.timePolynomial_eval line 328
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.totalSteps_le line 332
24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.machine line 363
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.machine_alphabet_finite line 374
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.initial_configuration line 380
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.finalTapes_input line 387
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.finalTapes_output line 388
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.finalTapes_work_empty line 390
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.machineInTime line 394