OAI/Computability/DirectedFeedback/Games/AddressTupleLoaded.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Integration.AddressTupleLoaded.Arena line 55
  2. def OAI.DFVSGames.Integration.AddressTupleLoaded.fieldAssignment line 59
  3. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.stageTapes_eq line 66
  4. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.fieldAssignment_frame line 92
  5. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_frame line 98
  6. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_field line 106
  7. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_source line 113
  8. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_extra line 119
  9. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_header line 126
  10. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_radix line 134
  11. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_capacity line 142
  12. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_current line 150
  13. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_remaining line 157
  14. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_finalOutput line 164
  15. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_loaderWork line 171
  16. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_privateAddress line 186
  17. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_clean line 194
  18. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_rhs line 213
  19. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_name line 223
  20. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_occurrence line 232
  21. def OAI.DFVSGames.Integration.AddressTupleLoaded.canonicalValues line 238
  22. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_canonicalField line 243
  23. theorem OAI.DFVSGames.Integration.AddressTupleLoaded.loaded_savedFields line 263
  24. def OAI.DFVSGames.Integration.AddressTupleCleanup.loadedFields line 288
  25. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.loadedFields_length line 293
  26. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.mem_loadedFields line 296
  27. abbrev OAI.DFVSGames.Integration.AddressTupleCleanup.Label line 310
  28. abbrev OAI.DFVSGames.Integration.AddressTupleCleanup.cleared line 312
  29. abbrev OAI.DFVSGames.Integration.AddressTupleCleanup.steps line 315
  30. abbrev OAI.DFVSGames.Integration.AddressTupleCleanup.budget line 318
  31. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_field line 321
  32. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_outside line 327
  33. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_source line 336
  34. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_savedIndex line 342
  35. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_extra line 349
  36. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_index line 356
  37. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_work line 362
  38. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_scratch line 368
  39. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_copyScratch line 374
  40. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_headerTape line 380
  41. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_current line 388
  42. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_remaining line 395
  43. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.cleared_finalOutput line 402
  44. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.steps_le line 409
  45. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.steps_le_uniform line 414
  46. abbrev OAI.DFVSGames.Integration.AddressTupleCleanup.entry line 422
  47. def OAI.DFVSGames.Integration.AddressTupleCleanup.instruction line 425
  48. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.trace line 430
  49. theorem OAI.DFVSGames.Integration.AddressTupleCleanup.trace_clean line 443
  50. def OAI.DFVSGames.Integration.AddressTupleCleanup.execution line 455
  51. abbrev OAI.DFVSGames.Integration.AddressTupleFrame.Arena line 481
  52. theorem OAI.DFVSGames.Integration.AddressTupleFrame.cleared_outputTapes line 483
  53. theorem OAI.DFVSGames.Integration.AddressTupleFrame.cleared_appended line 503
  54. theorem OAI.DFVSGames.Integration.AddressTupleFrame.cleared_fieldAssignment line 514
  55. theorem OAI.DFVSGames.Integration.AddressTupleFrame.cleared_loaded line 522
  56. theorem OAI.DFVSGames.Integration.AddressTupleFrame.cleared_appended_loaded line 531
  57. abbrev OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes line 542
  58. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_other line 558
  59. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_source line 565
  60. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_current line 570
  61. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_remaining line 577
  62. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_header line 584
  63. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_radix line 593
  64. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_capacity line 601
  65. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_output line 609
  66. theorem OAI.DFVSGames.Integration.AddressTupleFrame.finalTapes_clean line 617
  67. abbrev OAI.DFVSGames.Reduction.MachineRhsLoad.State line 637
  68. abbrev OAI.DFVSGames.Reduction.MachineRhsLoad.Alphabet line 638
  69. def OAI.DFVSGames.Reduction.MachineRhsLoad.rhs line 640
  70. def OAI.DFVSGames.Reduction.MachineRhsLoad.setRhs line 642
  71. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.rhs_setRhs line 645
  72. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.setRhs_setRhs line 648
  73. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.setRhs_same line 651
  74. def OAI.DFVSGames.Reduction.MachineRhsLoad.fill line 653
  75. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.fill_apply line 656
  76. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.fill_all line 669
  77. def OAI.DFVSGames.Reduction.MachineRhsLoad.finish line 679
  78. def OAI.DFVSGames.Reduction.MachineRhsLoad.peekChain line 684
  79. def OAI.DFVSGames.Reduction.MachineRhsLoad.statement line 692
  80. def OAI.DFVSGames.Reduction.MachineRhsLoad.readRhs line 695
  81. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.stepAux_peekChain line 698
  82. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.stepAux_statement line 709
  83. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.readRhs_of_unary line 716
  84. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.loadStep line 724
  85. def OAI.DFVSGames.Reduction.MachineRhsLoad.loadInTime line 735
  86. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.peekChain_pushBound line 751
  87. theorem OAI.DFVSGames.Reduction.MachineRhsLoad.statement_pushBound line 758