OAI/Combinatorics/IndependentSets/Machines/MachineLookupSpec.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.skipWord line 8
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.skipWord_encodeWord line 13
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.skipWord_iterate_encodeWords line 20
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.headWord line 31
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWord line 36
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWords line 44
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.lookupBits line 50
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.lookupBits_encodeWords line 53
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded line 58
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.decodeWords_encodeWord line 63
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_encode line 67
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_some line 72
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_none line 77
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.encoded_selected_split line 82
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.scannedBits line 94
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.encoded_prefix_length_le line 97
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.scannedBits_le line 106
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.scannedBits_of_some line 110
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.selected_scan_length_le line 117
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.output_length_le line 124
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.index_length_le line 131
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps line 142
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length_strong line 147
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length line 161
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_lt line 166
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_some line 181
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps_add_length_of_invalid line 187
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookupSpec.steps_le_input_encoding_size line 201