OAI/Computability/DirectedFeedback/Machines/MachineCloudSelect.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.BaseTape line 12
  2. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.BaseAlphabet line 13
  3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.BaseState line 14
  4. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.BaseLabel line 16
  5. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.skipLabel line 22
  6. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.baseProgram line 27
  7. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.baseProgram_skip line 47
  8. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Phase line 52
  9. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList line 57

    Source documentation

    A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.)

    protected abbrev Phase.enumList : List Phase := [.checking, .advancing, .finishing]

    Mentions: OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Phase

  10. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_getElem?_ctorIdx_eq line 59
  11. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_nodup line 63
  12. instance OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.(instance at line 65) line 65
  13. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Control line 69
  14. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Control.enumList line 74

    Source documentation

    A list enumerating every element of the type, which are all zero-argument constructors. (Generated by the Fintype deriving handler.)

    protected abbrev Control.enumList : List Control := [.initialize, .dispatch]

    Mentions: OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Control

  15. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_getElem?_ctorIdx_eq line 76
  16. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_nodup line 80
  17. instance OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.(instance at line 82) line 82
  18. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Tape line 86
  19. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Alphabet line 87
  20. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.Label line 88
  21. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.State line 89
  22. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.go line 91
  23. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.dispatcher line 94
  24. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.extra line 107
  25. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.program line 111
  26. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.memory line 114
  27. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.memory_inl line 119
  28. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.memory_position line 121
  29. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.update_memory_hit line 124
  30. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.update_memory_rank line 130
  31. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.update_memory_position line 136
  32. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.cfg line 143
  33. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.liftTrace line 148
  34. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.compareTrace line 161
  35. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.dispatch_miss line 184
  36. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_succ line 191
  37. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_zero line 200
  38. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.advanceStep line 208
  39. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.finishStep line 217
  40. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.initializeStep line 223
  41. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.skipTrace line 230
  42. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.rowSkipTrace line 254
  43. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.prefixTime line 298
  44. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.prefixTrace line 302
  45. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.cleanupTrace line 330
  46. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.selectedTrace line 364
  47. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.queryWord line 381
  48. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.prepareSteps line 383
  49. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.prepareTrace line 387
  50. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.prefixSelectedTrace line 446
  51. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.totalSteps line 468
  52. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.fullTrace line 473
  53. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.prefixTime_le line 497
  54. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.totalSteps_le line 509
  55. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.remainder line 527
  56. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.tableRows_getElem line 531
  57. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.tableWord_split line 541
  58. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps line 554
  59. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.cloudSelectTrace line 560
  60. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps_le line 584
  61. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.timePolynomial line 594
  62. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.cloudSelectInTime line 597
  63. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.machine line 613
  64. def OAI.DFVSGames.Foundations.Complexity.MachineCloudSelect.machineInTime line 624
  65. def OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.localStep line 651
  66. def OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.destination line 655
  67. def OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.rowIndex line 659
  68. def OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row line 664
  69. def OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation line 668
  70. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation_apply line 671
  71. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.cloud_rotation line 675
  72. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.source_rotation line 684
  73. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.rotation_internal line 696
  74. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.reverseIndex_internal line 703
  75. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.relation_ext_inline_PreprocessingInternalRows line 713
  76. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.relations_internal line 722
  77. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row_tail line 729
  78. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row_reverse line 734
  79. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row_relation line 741
  80. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.localStep_original line 746
  81. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.localStep_dummy line 751
  82. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row_tail_original line 755
  83. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row_tail_dummy line 761
  84. def OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex line 767
  85. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_eq line 772
  86. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_old line 796
  87. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_dummy line 801
  88. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.row_reverse_selectedIndex line 807
  89. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingInternalRows.rowWords_eq line 815