OAI/Computability/MinUncut/Machines/MachineBinaryNameMachine.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.BinaryNameMachine.frame line 14
  2. def OAI.MinUncutGames.BinaryNameMachine.finalDigit line 18
  3. def OAI.MinUncutGames.BinaryNameMachine.canonical line 22
  4. structure OAI.MinUncutGames.BinaryNameMachine.Result line 24
  5. def OAI.MinUncutGames.BinaryNameMachine.scanSpec line 30
  6. def OAI.MinUncutGames.BinaryNameMachine.steps line 36
  7. theorem OAI.MinUncutGames.BinaryNameMachine.steps_le line 40
  8. theorem OAI.MinUncutGames.BinaryNameMachine.frame_length line 49
  9. theorem OAI.MinUncutGames.BinaryNameMachine.scanSpec_frame line 55
  10. theorem OAI.MinUncutGames.BinaryNameMachine.steps_frame line 64
  11. abbrev OAI.MinUncutGames.BinaryNameMachine.Alphabet line 74
  12. abbrev OAI.MinUncutGames.BinaryNameMachine.State line 75
  13. def OAI.MinUncutGames.BinaryNameMachine.clean line 77
  14. def OAI.MinUncutGames.BinaryNameMachine.exitAt line 79
  15. def OAI.MinUncutGames.BinaryNameMachine.finish line 84
  16. def OAI.MinUncutGames.BinaryNameMachine.scan line 87
  17. theorem OAI.MinUncutGames.BinaryNameMachine.stepAux_finish line 102
  18. theorem OAI.MinUncutGames.BinaryNameMachine.update_source line 107
  19. theorem OAI.MinUncutGames.BinaryNameMachine.update_destination line 118
  20. theorem OAI.MinUncutGames.BinaryNameMachine.step_empty line 132
  21. theorem OAI.MinUncutGames.BinaryNameMachine.step_end line 140
  22. theorem OAI.MinUncutGames.BinaryNameMachine.step_truncated line 151
  23. theorem OAI.MinUncutGames.BinaryNameMachine.step_digit line 159
  24. theorem OAI.MinUncutGames.BinaryNameMachine.scanTrace line 169
  25. def OAI.MinUncutGames.BinaryNameMachine.scanInTime line 203
  26. theorem OAI.MinUncutGames.BinaryNameMachine.framedTrace line 215
  27. def OAI.MinUncutGames.BinaryNameMachine.machine line 228
  28. theorem OAI.MinUncutGames.BinaryNameMachine.machine_finiteAlphabet line 239
  29. def OAI.MinUncutGames.BinaryNameMachine.machineInTime line 243
  30. abbrev OAI.MinUncutGames.BinaryNameCompare.Alphabet line 265
  31. abbrev OAI.MinUncutGames.BinaryNameCompare.State line 266
  32. def OAI.MinUncutGames.BinaryNameCompare.clean line 268
  33. def OAI.MinUncutGames.BinaryNameCompare.scanStateEquiv line 270
  34. def OAI.MinUncutGames.BinaryNameCompare.compareStateEquiv line 276
  35. inductive OAI.MinUncutGames.BinaryNameCompare.Label line 282
  36. abbrev OAI.MinUncutGames.BinaryNameCompare.Label.enumList line 286
  37. theorem OAI.MinUncutGames.BinaryNameCompare.Label.enumList_getElem?_ctorIdx_eq line 288
  38. theorem OAI.MinUncutGames.BinaryNameCompare.Label.enumList_nodup line 292
  39. instance OAI.MinUncutGames.BinaryNameCompare.(instance at line 294) line 294
  40. def OAI.MinUncutGames.BinaryNameCompare.instruction line 298
  41. def OAI.MinUncutGames.BinaryNameCompare.steps line 311
  42. theorem OAI.MinUncutGames.BinaryNameCompare.steps_le line 314
  43. theorem OAI.MinUncutGames.BinaryNameCompare.joinTrace line 319
  44. theorem OAI.MinUncutGames.BinaryNameCompare.compareTrace line 323
  45. def OAI.MinUncutGames.BinaryNameCompare.compareInTime line 427
  46. def OAI.MinUncutGames.BinaryNameCompare.machine line 449
  47. theorem OAI.MinUncutGames.BinaryNameCompare.machine_finiteAlphabet line 462
  48. abbrev OAI.MinUncutGames.BinaryNameSearch.Token line 477
  49. def OAI.MinUncutGames.BinaryNameSearch.tokenBits line 479
  50. def OAI.MinUncutGames.BinaryNameSearch.stream line 482
  51. def OAI.MinUncutGames.BinaryNameSearch.payloads line 486
  52. def OAI.MinUncutGames.BinaryNameSearch.afterMatch line 488
  53. def OAI.MinUncutGames.BinaryNameSearch.steps line 492
  54. def OAI.MinUncutGames.BinaryNameSearch.payloadSize line 498
  55. theorem OAI.MinUncutGames.BinaryNameSearch.stream_nil line 500
  56. theorem OAI.MinUncutGames.BinaryNameSearch.stream_cons line 502
  57. theorem OAI.MinUncutGames.BinaryNameSearch.payloads_nil line 505
  58. theorem OAI.MinUncutGames.BinaryNameSearch.payloads_cons line 507
  59. theorem OAI.MinUncutGames.BinaryNameSearch.payloadSize_nil line 510
  60. theorem OAI.MinUncutGames.BinaryNameSearch.payloadSize_cons line 512
  61. theorem OAI.MinUncutGames.BinaryNameSearch.stream_length line 515
  62. theorem OAI.MinUncutGames.BinaryNameSearch.steps_le line 524
  63. theorem OAI.MinUncutGames.BinaryNameSearch.steps_le_stream line 533
  64. abbrev OAI.MinUncutGames.BinaryNameSearch.Alphabet line 543
  65. abbrev OAI.MinUncutGames.BinaryNameSearch.State line 544
  66. abbrev OAI.MinUncutGames.BinaryNameSearch.clean line 546
  67. inductive OAI.MinUncutGames.BinaryNameSearch.Label line 548
  68. def OAI.MinUncutGames.BinaryNameSearch.compareTapes line 554
  69. theorem OAI.MinUncutGames.BinaryNameSearch.compareTapes_injective line 557
  70. def OAI.MinUncutGames.BinaryNameSearch.exitAt line 563
  71. def OAI.MinUncutGames.BinaryNameSearch.finish line 568
  72. def OAI.MinUncutGames.BinaryNameSearch.instruction line 571
  73. theorem OAI.MinUncutGames.BinaryNameSearch.stepAux_finish line 582
  74. theorem OAI.MinUncutGames.BinaryNameSearch.update_source line 586
  75. theorem OAI.MinUncutGames.BinaryNameSearch.update_counter line 597
  76. theorem OAI.MinUncutGames.BinaryNameSearch.joinTrace line 603
  77. theorem OAI.MinUncutGames.BinaryNameSearch.signStep line 616
  78. theorem OAI.MinUncutGames.BinaryNameSearch.emptyStep line 627
  79. theorem OAI.MinUncutGames.BinaryNameSearch.incrementStep line 638
  80. theorem OAI.MinUncutGames.BinaryNameSearch.tokenTrace line 648
  81. theorem OAI.MinUncutGames.BinaryNameSearch.searchTrace line 694
  82. def OAI.MinUncutGames.BinaryNameSearch.searchInTime line 745
  83. def OAI.MinUncutGames.BinaryNameSearch.machine line 766
  84. theorem OAI.MinUncutGames.BinaryNameSearch.machine_finiteAlphabet line 779