OAI/Computability/DirectedFeedback/Games/FieldArray.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.finish line 14
2. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.finishStep line 18
3. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequenceTapes line 28
4. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequenceTrace line 36
5. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequenceInTime line 95
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequence_time_eq_length line 117
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_other line 122
8. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_source line 137
9. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sequenceTapes_selected line 152
10. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.boundedIndex line 200
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.boundedIndex_val line 202
12. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.destination line 205
13. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.startLabel line 206
14. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.loopLabel line 207
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.destination_ne_source line 209
16. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.destination_injective_below line 217
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.destination_eq_succ line 224
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.output_source line 228
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.output_field line 236
20. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.program line 249
21. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.machine line 258
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.atStart line 269
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.atLoop line 273
24. theorem OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.atDone line 278
25. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.machineInTime line 281
26. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.machineInTime_inputBound line 312
27. def OAI.DFVSGames.Foundations.Hastad.SourceFieldArray.sixFieldsInTime line 326
28. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.discardFieldsTrace line 351
29. inductive OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.Tape line 394
30. inductive OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.Label line 398
31. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.fieldDestination line 404
32. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.readStart line 405
33. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.readLoop line 406
34. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.skipLabel line 407
35. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.headerLabel line 408
36. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.program line 411
37. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.machine line 428
38. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.atSkip line 439
39. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.atReadStart line 443
40. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.atReadLoop line 447
41. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.atReadDone line 452
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.discardHeadersTrace line 455
43. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.discardSixTrace line 467
44. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.readSixTrace line 477
45. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.scanTapes line 493
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.scanTapes_work line 497
47. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.scanTapes_index line 501
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.scanTapes_other line 506
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.update_scanTapes_work line 511
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.skipClausesTrace line 518
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_eq line 566
52. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.fieldDestination_injective_below line 572
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.readSix_output_field line 578
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.readSix_output_work line 590
55. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.readSix_output_frame line 598
56. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.outputTapes line 606
57. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.scanSteps line 612
58. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.scanReadTrace line 618
59. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.lookupSteps line 646
60. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitTrace line 650
61. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.output_formula line 680
62. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.output_index line 686
63. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.output_work line 692
64. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.output_field line 698
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.output_frame line 705
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.clauseWords_six line 712
67. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.fieldWords line 718
68. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.output_fieldWords line 722
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.lookupSteps_le_input line 728
70. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.timePolynomial line 747
71. theorem OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.timePolynomial_eval line 749
72. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.lookupWithSplitInTime line 752
73. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.lookupInTime line 772
74. def OAI.DFVSGames.Foundations.Hastad.SourceClauseLookup.machineInTime line 791