OAI/Computability/DirectedFeedback/Encoding/Occurrences.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding line 12
2. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.fin line 18
3. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.bool line 19
4. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.unit line 20
5. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.prod line 22
6. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.sum line 25
7. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.function line 28
8. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 36
9. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 38
10. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 41
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 45
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 48
13. abbrev OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.GlobalKey line 54
14. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.globalEncoding line 56
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 62
16. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.extendRestricted line 67
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 71
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 75
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 82
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 88
21. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 94
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 99
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 105
24. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.localAddress line 117
25. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.localAddress_injective line 124
26. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence line 149
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.conditionedOccurrence_satisfied line 158
28. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.findValid line 187
29. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.findValid_none_iff line 191
30. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.firstValid line 200
31. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.firstValid_none_iff line 203
32. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.occurrenceList line 208
33. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.occurrenceList_length line 211
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.countP_cast_eq_sum_inline_SourceOccurrences line 215
35. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.countP_enumerate line 221
36. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.occurrenceList_acceptance line 228
37. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 242
38. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.slotEncoding line 244
39. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.iEncoding line 252
40. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.jEncoding line 253
41. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.variableEncoding line 254
42. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.clauseEncoding line 256
43. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 258
44. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.proofEncoding line 261
45. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.nBits line 265
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.nBits_eq line 267
47. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.dummyIndex line 271
48. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.leftAnchor line 274
49. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.rightAnchor line 276
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 279
51. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 283
52. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.extendHalfTables line 295
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 302
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 313
55. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.emptyAddress line 330
56. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.contextEquation line 335
57. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.leftResponse line 344
58. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.rightResponse line 348
59. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 355
60. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 372
61. abbrev OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.SourceIndex line 376
62. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 379
63. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceEquation line 382
64. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.rawSourceList line 386
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 389
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 396
67. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 419
68. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceList line 422
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceList_empty line 425
70. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 428
71. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 434
72. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 443
73. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.sourceInput line 454
74. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 458
75. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_pair line 473
76. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.prod_decode_mk line 481
77. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_prod line 497
78. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.map_enumerate_prod line 512
79. theorem OAI.DFVSGames.Foundations.Hastad.SourceEnumeration.testTapeEncoding_enumerate line 524
80. theorem OAI.DFVSGames.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_enumerate line 532
81. theorem OAI.DFVSGames.Foundations.Hastad.SourceEnumeration.sourceIndexEncoding_map line 543
82. theorem OAI.DFVSGames.Foundations.Hastad.SourceEnumeration.rawSourceList_eq_nestedLoops line 555
83. theorem OAI.DFVSGames.Foundations.Hastad.SourceEnumeration.sourceList_eq_nestedLoops line 565
84. theorem OAI.DFVSGames.Foundations.Hastad.SourceEnumeration.rawSourceList_flatMap line 576
85. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.variable_rank line 598
86. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.clause_rank line 602
87. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.left_address line 606
88. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.right_address line 611
89. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.dummy_address line 617
90. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.left_address_radix line 624
91. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.right_address_radix line 631
92. theorem OAI.DFVSGames.Foundations.Hastad.SourceAddressArithmetic.nBits_eq_dummy_succ line 639
93. abbrev OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.Position line 651
94. abbrev OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.NameProfile line 652
95. structure OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.Signature line 654
96. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureEquiv line 660
97. instance OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureFintype line 667
98. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.card_position line 671
99. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.card_signature line 674
100. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.positiveAt line 680
101. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.occurrenceName line 685
102. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.contextNameProfile line 689
103. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.ofContext line 692
104. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.ofContext_signs line 698
105. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.ofContext_sameName line 702
106. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.ofContext_selected line 707
107. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureSatisfies line 710
108. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureValid line 715
109. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureSatisfies_ofContext line 720
110. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signature_validJ line 725
111. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot line 748
112. def OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureProjection line 752
113. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signatureCanonicalSlot_ofContext line 755
114. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signature_pi line 770
115. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.signature_projection_selected line 776
116. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.validJ_eq_of_signature_eq line 785
117. theorem OAI.DFVSGames.Foundations.Hastad.SourceLocalSignature.pi_eq_of_signature_eq line 791