OAI/Computability/MinUncut/PCP/LoopOrder.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple line 13
2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_function line 17
3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_fin_function line 23
4. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.tupleTapeOrder line 35
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_eq_tupleTapeOrder line 43
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_flatMap_tupleTapeOrder line 50
7. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.rankedQuery line 56
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.rankedQuery_at line 62
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_ofFn line 67
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_enumerate line 82
11. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_tupleTapeOrder line 96
12. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder line 105
13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.sourceIndexEncoding_eq_tupleSourceOrder line 111
14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.rawSourceList_eq_tupleOrder line 129
15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.sourceList_eq_tupleOrder line 134
16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.rawSourceList_flatMap_tupleOrder line 138
17. def OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.reverseAppend line 145
18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend line 149
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_header line 159
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_prefix line 165
21. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.foldl_resultTapes line 172
22. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.inputBits_eq_header_records line 190
23. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.input_reverse_accumulator line 202
24. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.sourceInput_tuple_reverse_accumulator line 209
25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceLoopOrder.finalReverse_steps line 223
26. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryOrder.occurrenceBits line 244
27. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryOrder.slotBits line 247
28. def OAI.MinUncutGames.Foundations.Hastad.SourceQueryOrder.tupleBits line 251
29. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryOrder.equationBits_eq line 254
30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryOrder.prefixBits_eq_slotBits line 261
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceQueryOrder.sourceLoopInTime line 274
32. structure OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.Snapshot line 320
33. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes line 330
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_rank line 338
35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_rightBase line 340
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_leftBase line 342
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_zero line 344
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_accumulator line 346
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_coefficient line 348
40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_dummy line 350
41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_leftBlock line 352
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_queryTemporary line 354
43. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_queryScratch line 356
44. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_field line 358
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_current line 360
46. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_formula line 362
47. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_index line 364
48. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_work line 366
49. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_variableHeader line 368
50. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_clauseHeader line 370
51. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.update_rank line 375
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.update_rightBase line 384
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.update_leftBase line 393
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.update_zero line 402
55. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.update_emitted line 411
56. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.query_result line 421
57. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.horner_clause_result line 430
58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.horner_variable_result line 437
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.horner_right_result line 445
60. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.horner_left_result line 452
61. structure OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.WorkClean line 459
62. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.clean_clause line 466
63. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.clean_variable line 474
64. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.clean_base line 482
65. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_coordinateOutput line 490
66. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.tapes_stageTapes line 503
67. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.final_tapes line 515
68. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.empty_tapes line 528
69. theorem OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.clear_loaded line 535
70. def OAI.MinUncutGames.Foundations.Hastad.SourceTupleTape.clearLoadedSnapshotInTime line 542