OAI/Computability/MinUncut/PCP/Occurrences.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding line 14
2. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.fin line 20
3. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.bool line 21
4. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.unit line 22
5. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.prod line 24
6. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.sum line 27
7. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.function line 30
8. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 38
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 40
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 43
11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 47
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 50
13. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.GlobalKey line 56
14. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.globalEncoding line 58
15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 64
16. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.extendRestricted line 69
17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 73
18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 77
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 84
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 90
21. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 96
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 101
23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 107
24. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.localAddress line 119
25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.localAddress_injective line 126
26. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 151
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 160
28. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.findValid line 189
29. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 193
30. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.firstValid line 202
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 205
32. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.occurrenceList line 210
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 213
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum line 217
35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.countP_enumerate line 223
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 230
37. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 245
38. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.slotEncoding line 247
39. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.iEncoding line 255
40. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.jEncoding line 256
41. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.variableEncoding line 257
42. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.clauseEncoding line 259
43. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 261
44. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.proofEncoding line 264
45. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.nBits line 268
46. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.nBits_eq line 270
47. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.dummyIndex line 274
48. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.leftAnchor line 277
49. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.rightAnchor line 279
50. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 282
51. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 286
52. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.extendHalfTables line 298
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 305
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 316
55. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.emptyAddress line 333
56. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.contextEquation line 338
57. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.leftResponse line 347
58. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.rightResponse line 351
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 358
60. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 375
61. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.SourceIndex line 379
62. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 382
63. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceEquation line 385
64. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.rawSourceList line 389
65. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 392
66. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 399
67. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 422
68. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceList line 425
69. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceList_empty line 428
70. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 431
71. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 437
72. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 446
73. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.sourceInput line 457
74. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 461