OAI/Computability/DirectedFeedback/Machines/MachineBinaryTotalInputMachine.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DFVSGames.BinaryTotalInputMachine.Label line 60
  2. instance OAI.DFVSGames.BinaryTotalInputMachine.(instance at line 67) line 67
  3. abbrev OAI.DFVSGames.BinaryTotalInputMachine.Alphabet line 69
  4. abbrev OAI.DFVSGames.BinaryTotalInputMachine.State line 70
  5. def OAI.DFVSGames.BinaryTotalInputMachine.rejectedWord line 72
  6. def OAI.DFVSGames.BinaryTotalInputMachine.instruction line 74
  7. abbrev OAI.DFVSGames.BinaryTotalInputMachine.machine line 88
  8. def OAI.DFVSGames.BinaryTotalInputMachine.tapes line 99
  9. def OAI.DFVSGames.BinaryTotalInputMachine.cfg line 104
  10. theorem OAI.DFVSGames.BinaryTotalInputMachine.tapes_input line 108
  11. theorem OAI.DFVSGames.BinaryTotalInputMachine.tapes_output line 111
  12. theorem OAI.DFVSGames.BinaryTotalInputMachine.tapes_saved line 114
  13. theorem OAI.DFVSGames.BinaryTotalInputMachine.update_input_inline_MachineBinaryTotalInputMachine line 117
  14. theorem OAI.DFVSGames.BinaryTotalInputMachine.update_output_inline_MachineBinaryTotalInputMachine line 123
  15. theorem OAI.DFVSGames.BinaryTotalInputMachine.update_saved_inline_MachineBinaryTotalInputMachine line 129
  16. def OAI.DFVSGames.BinaryTotalInputMachine.afterScan line 135
  17. theorem OAI.DFVSGames.BinaryTotalInputMachine.step_scan_empty line 137
  18. theorem OAI.DFVSGames.BinaryTotalInputMachine.step_scan_cons line 145
  19. theorem OAI.DFVSGames.BinaryTotalInputMachine.scanTrace line 153
  20. theorem OAI.DFVSGames.BinaryTotalInputMachine.restoreTrace line 169
  21. theorem OAI.DFVSGames.BinaryTotalInputMachine.drainTrace line 181
  22. theorem OAI.DFVSGames.BinaryTotalInputMachine.step_rejectOutput line 192
  23. theorem OAI.DFVSGames.BinaryTotalInputMachine.joinTrace_inline_MachineBinaryTotalInputMachine line 202
  24. theorem OAI.DFVSGames.BinaryTotalInputMachine.acceptedTrace line 206
  25. theorem OAI.DFVSGames.BinaryTotalInputMachine.rejectedTrace line 217
  26. theorem OAI.DFVSGames.BinaryTotalInputMachine.initList_eq line 232
  27. theorem OAI.DFVSGames.BinaryTotalInputMachine.haltList_eq line 239
  28. def OAI.DFVSGames.BinaryTotalInputMachine.steps line 246
  29. theorem OAI.DFVSGames.BinaryTotalInputMachine.steps_le line 249
  30. theorem OAI.DFVSGames.BinaryTotalInputMachine.totalTrace line 253
  31. def OAI.DFVSGames.BinaryTotalInputMachine.outputsInTime line 275
  32. def OAI.DFVSGames.BinaryTotalInputMachine.computableInPolyTime line 283
  33. theorem OAI.DFVSGames.BinaryTotalInputMachine.machine_finiteAlphabet line 297
  34. theorem OAI.DFVSGames.BinaryTotalInputMachine.computation_finiteAlphabet line 301
  35. abbrev OAI.DFVSGames.BinaryNameCompare.Alphabet line 318
  36. abbrev OAI.DFVSGames.BinaryNameCompare.State line 319
  37. def OAI.DFVSGames.BinaryNameCompare.clean line 321
  38. def OAI.DFVSGames.BinaryNameCompare.scanStateEquiv line 323
  39. def OAI.DFVSGames.BinaryNameCompare.compareStateEquiv line 329
  40. inductive OAI.DFVSGames.BinaryNameCompare.Label line 335
  41. instance OAI.DFVSGames.BinaryNameCompare.(instance at line 339) line 339
  42. def OAI.DFVSGames.BinaryNameCompare.instruction line 341
  43. def OAI.DFVSGames.BinaryNameCompare.steps line 354
  44. theorem OAI.DFVSGames.BinaryNameCompare.steps_le line 357
  45. theorem OAI.DFVSGames.BinaryNameCompare.joinTrace_inline_MachineBinaryNameCompare line 362
  46. theorem OAI.DFVSGames.BinaryNameCompare.compareTrace line 366
  47. def OAI.DFVSGames.BinaryNameCompare.compareInTime line 470
  48. def OAI.DFVSGames.BinaryNameCompare.machine line 492
  49. theorem OAI.DFVSGames.BinaryNameCompare.machine_finiteAlphabet line 505
  50. abbrev OAI.DFVSGames.BinaryNameSearch.Token line 522
  51. def OAI.DFVSGames.BinaryNameSearch.tokenBits line 524
  52. def OAI.DFVSGames.BinaryNameSearch.stream line 527
  53. def OAI.DFVSGames.BinaryNameSearch.payloads line 531
  54. def OAI.DFVSGames.BinaryNameSearch.afterMatch line 533
  55. def OAI.DFVSGames.BinaryNameSearch.steps line 537
  56. def OAI.DFVSGames.BinaryNameSearch.payloadSize line 543
  57. theorem OAI.DFVSGames.BinaryNameSearch.stream_nil line 545
  58. theorem OAI.DFVSGames.BinaryNameSearch.stream_cons line 547
  59. theorem OAI.DFVSGames.BinaryNameSearch.payloads_nil line 550
  60. theorem OAI.DFVSGames.BinaryNameSearch.payloads_cons line 552
  61. theorem OAI.DFVSGames.BinaryNameSearch.payloadSize_nil line 555
  62. theorem OAI.DFVSGames.BinaryNameSearch.payloadSize_cons line 557
  63. theorem OAI.DFVSGames.BinaryNameSearch.stream_length line 560
  64. theorem OAI.DFVSGames.BinaryNameSearch.steps_le line 569
  65. theorem OAI.DFVSGames.BinaryNameSearch.steps_le_stream line 578
  66. abbrev OAI.DFVSGames.BinaryNameSearch.Alphabet line 588
  67. abbrev OAI.DFVSGames.BinaryNameSearch.State line 589
  68. abbrev OAI.DFVSGames.BinaryNameSearch.clean line 591
  69. inductive OAI.DFVSGames.BinaryNameSearch.Label line 593
  70. def OAI.DFVSGames.BinaryNameSearch.compareTapes line 599
  71. theorem OAI.DFVSGames.BinaryNameSearch.compareTapes_injective line 602
  72. def OAI.DFVSGames.BinaryNameSearch.exitAt line 608
  73. def OAI.DFVSGames.BinaryNameSearch.finish line 613
  74. def OAI.DFVSGames.BinaryNameSearch.instruction line 616
  75. theorem OAI.DFVSGames.BinaryNameSearch.stepAux_finish line 627
  76. theorem OAI.DFVSGames.BinaryNameSearch.update_source_inline_MachineBinaryNameSearch line 631
  77. theorem OAI.DFVSGames.BinaryNameSearch.update_counter_inline_MachineBinaryNameSearch line 642
  78. theorem OAI.DFVSGames.BinaryNameSearch.joinTrace_inline_MachineBinaryNameSearch line 648
  79. theorem OAI.DFVSGames.BinaryNameSearch.signStep line 661
  80. theorem OAI.DFVSGames.BinaryNameSearch.emptyStep line 672
  81. theorem OAI.DFVSGames.BinaryNameSearch.incrementStep line 683
  82. theorem OAI.DFVSGames.BinaryNameSearch.tokenTrace line 693
  83. theorem OAI.DFVSGames.BinaryNameSearch.searchTrace line 739
  84. def OAI.DFVSGames.BinaryNameSearch.searchInTime line 790
  85. def OAI.DFVSGames.BinaryNameSearch.machine line 811
  86. theorem OAI.DFVSGames.BinaryNameSearch.machine_finiteAlphabet line 824