OAI/Computability/DirectedFeedback/Machines/ContextClear.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextClear.Tape line 12
2. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.fieldAt line 16
3. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.fields line 19
4. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.fieldAt_injective line 21
5. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.fields_length line 28
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.fields_nodup line 31
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.field_mem line 34
8. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.mem_fields_iff line 39
9. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.outputTapes line 47
10. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.output_field line 51
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.output_frame line 54
12. abbrev OAI.DFVSGames.Foundations.Hastad.SourceContextClear.Label line 58
13. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.entryLabel_inline_SourceContextClear line 61
14. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.main line 65
15. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.program line 69
16. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.entryLabel_eq_inline_SourceContextClear line 74
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.entry_eq_inline_SourceContextClear line 81
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.finalTapes_eq line 85
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.lengthSum_update_inline_SourceContextClear line 91
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.steps_eq_of_nodup_inline_SourceContextClear line 101
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.trace_trans_inline_SourceContextClear line 113
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.clearTrace line 117
23. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.clearInTime line 129
24. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.lengthSum_le_selected_inline_SourceContextClear line 137
25. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.clauseField_length_le line 149
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.variables_add_two_le_input line 157
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.loaded_field_length_le line 164
28. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.loaded_cost_le line 173
29. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.clearLoadedInTime line 186
30. theorem OAI.DFVSGames.Foundations.Hastad.SourceContextClear.output_loaded_eq_base line 198
31. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.clearLoadedToBaseInTime line 209
32. def OAI.DFVSGames.Foundations.Hastad.SourceContextClear.machine line 219
33. def OAI.DFVSGames.Foundations.Hastad.SourceQueryOrder.occurrenceBits line 238
34. def OAI.DFVSGames.Foundations.Hastad.SourceQueryOrder.slotBits line 241
35. def OAI.DFVSGames.Foundations.Hastad.SourceQueryOrder.tupleBits line 245
36. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryOrder.equationBits_eq line 248
37. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryOrder.prefixBits_eq_slotBits line 255
38. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryOrder.sourceLoopInTime line 268
39. structure OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.Snapshot line 313
40. def OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes line 323
41. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_rank line 331
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_rightBase line 333
43. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_leftBase line 335
44. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_zero line 337
45. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_accumulator line 339
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_coefficient line 341
47. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_dummy line 343
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_leftBlock line 345
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_queryTemporary line 347
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_queryScratch line 349
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_field line 351
52. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_current line 353
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_formula line 355
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_index line 357
55. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_work line 359
56. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_variableHeader line 361
57. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_clauseHeader line 363
58. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.update_rank line 368
59. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.update_rightBase line 377
60. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.update_leftBase line 386
61. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.update_zero line 395
62. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.update_emitted line 404
63. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.query_result line 414
64. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.horner_clause_result line 423
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.horner_variable_result line 430
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.horner_right_result line 438
67. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.horner_left_result line 445
68. structure OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.WorkClean line 452
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.clean_clause line 459
70. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.clean_variable line 467
71. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.clean_base line 475
72. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_coordinateOutput line 483
73. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.tapes_stageTapes line 496
74. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.final_tapes line 508
75. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.empty_tapes line 521
76. theorem OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.clear_loaded line 528
77. def OAI.DFVSGames.Foundations.Hastad.SourceTupleTape.clearLoadedSnapshotInTime line 535