OAI/Computability/VertexCover/Fourier/SourceOccurrences.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding line 46
2. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.fin line 52
3. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.bool line 53
4. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.unit line 54
5. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.prod line 56
6. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.sum line 59
7. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.function line 62
8. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 70
9. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 72
10. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 75
11. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 79
12. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 82
13. abbrev OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.GlobalKey line 88
14. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.globalEncoding line 90
15. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 96
16. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.extendRestricted line 101
17. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 105
18. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 109
19. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 116
20. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 122
21. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 128
22. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 133
23. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 139
24. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.localAddress line 151
25. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.localAddress_injective line 158
26. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 183
27. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 192
28. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.findValid line 221
29. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 225
30. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.firstValid line 234
31. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 237
32. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.occurrenceList line 242
33. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 245
34. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum line 249
35. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.countP_enumerate line 255
36. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 262
37. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 277
38. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.slotEncoding line 279
39. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.iEncoding line 287
40. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.jEncoding line 288
41. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.variableEncoding line 289
42. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.clauseEncoding line 291
43. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 293
44. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.proofEncoding line 296
45. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.nBits line 300
46. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.nBits_eq line 302
47. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.dummyIndex line 306
48. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.leftAnchor line 309
49. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.rightAnchor line 311
50. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 314
51. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 318
52. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.extendHalfTables line 330
53. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 337
54. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 348
55. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.emptyAddress line 365
56. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.contextEquation line 370
57. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.leftResponse line 379
58. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.rightResponse line 383
59. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 390
60. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 407
61. abbrev OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.SourceIndex line 411
62. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 414
63. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceEquation line 417
64. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.rawSourceList line 421
65. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 424
66. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 431
67. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 454
68. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceList line 457
69. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceList_empty line 460
70. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 463
71. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 469
72. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 478
73. def OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.sourceInput line 489
74. theorem OAI.UniqueGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 493