OAI/Computability/WeisfeilerLeman/RAMInstruction.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.ZeroTest.Reg line 7
  2. def OAI.WLTime.ZeroTest.state line 8
  3. def OAI.WLTime.ZeroTest.marks line 9
  4. theorem OAI.WLTime.ZeroTest.marks_length line 12
  5. theorem OAI.WLTime.ZeroTest.marks_head line 17
  6. def OAI.WLTime.ZeroTest.body line 25
  7. def OAI.WLTime.ZeroTest.loopCode line 26
  8. def OAI.WLTime.ZeroTest.finish line 27
  9. def OAI.WLTime.ZeroTest.program line 29
  10. theorem OAI.WLTime.ZeroTest.loop_exec line 30
  11. theorem OAI.WLTime.ZeroTest.finish_exec line 47
  12. theorem OAI.WLTime.ZeroTest.program_exec line 64
  13. theorem OAI.WLTime.ZeroTest.program_size line 78
  14. theorem OAI.WLTime.ZeroTest.any_false_iff line 79
  15. theorem OAI.WLTime.ZeroTest.word_zero_iff line 83
  16. def OAI.WLTime.RAMInstruction.operations line 98
  17. def OAI.WLTime.RAMInstruction.depth line 103
  18. theorem OAI.WLTime.RAMInstruction.depth_pos line 107
  19. structure OAI.WLTime.SparseRAM.Config line 111
  20. def OAI.WLTime.SparseRAM.execute line 117
  21. theorem OAI.WLTime.SparseRAM.execute_log_length line 124
  22. def OAI.WLTime.SparseRAM.forget line 142
  23. theorem OAI.WLTime.SparseRAM.execute_forget line 147
  24. def OAI.WLTime.SparseRAM.step line 162
  25. theorem OAI.WLTime.SparseRAM.step_forget line 166
  26. theorem OAI.WLTime.SparseRAM.iterate_forget line 171
  27. theorem OAI.WLTime.SparseRAM.step_fixed line 176
  28. theorem OAI.WLTime.RAM.time_halted line 180
  29. theorem OAI.WLTime.RAM.answer_stable line 185
  30. theorem OAI.WLTime.RAM.run_add_halted line 186
  31. theorem OAI.WLTime.RAM.accepts_iff_answer line 196
  32. def OAI.WLTime.RAMAlphabet.operations line 217
  33. abbrev OAI.WLTime.RAMAlphabet.Index line 219
  34. def OAI.WLTime.RAMAlphabet.operation line 220
  35. abbrev OAI.WLTime.RAMAlphabet.Reg line 221
  36. abbrev OAI.WLTime.RAMAlphabet.Letter line 222
  37. def OAI.WLTime.RAMAlphabet.decode line 223
  38. def OAI.WLTime.RAMAlphabet.memMap line 226
  39. theorem OAI.WLTime.RAMAlphabet.memMap_inj line 227
  40. def OAI.WLTime.RAMAlphabet.liftMem line 230
  41. def OAI.WLTime.RAMAlphabet.state line 234
  42. theorem OAI.WLTime.RAMAlphabet.liftMem_mem line 236
  43. theorem OAI.WLTime.RAMAlphabet.mem_exec line 238
  44. def OAI.WLTime.RAMAlphabet.opReg line 252
  45. theorem OAI.WLTime.RAMAlphabet.opReg_inj line 254
  46. def OAI.WLTime.RAMAlphabet.opLetter line 263
  47. theorem OAI.WLTime.RAMAlphabet.opLetter_inj line 266
  48. def OAI.WLTime.RAMAlphabet.opDecode line 269
  49. theorem OAI.WLTime.RAMAlphabet.opDecode_left line 271
  50. def OAI.WLTime.RAMAlphabet.opCode line 273
  51. def OAI.WLTime.RAMAlphabet.fileState line 275
  52. theorem OAI.WLTime.RAMAlphabet.fileState_opReg line 277
  53. theorem OAI.WLTime.RAMAlphabet.op_exec line 285
  54. theorem OAI.WLTime.RAMAlphabet.opCode_size line 303
  55. theorem OAI.WLTime.RAMAlphabet.mem_program line 306
  56. def OAI.WLTime.RAMAlphabet.locate line 310
  57. theorem OAI.WLTime.RAMAlphabet.locate_eq line 312
  58. abbrev OAI.WLTime.RAMTests.Reg line 320
  59. def OAI.WLTime.RAMTests.flags line 321
  60. def OAI.WLTime.RAMTests.testMap line 323
  61. theorem OAI.WLTime.RAMTests.testMap_inj line 324
  62. def OAI.WLTime.RAMTests.testCode line 325
  63. theorem OAI.WLTime.RAMTests.exec line 327
  64. theorem OAI.WLTime.RAMTests.pop_exec line 342
  65. theorem OAI.WLTime.RAMTests.code_size line 347
  66. def OAI.WLTime.RAMAlphabet.memCode line 358
  67. theorem OAI.WLTime.RAMAlphabet.memCode_size line 360
  68. theorem OAI.WLTime.RAMAlphabet.prefix_exec line 361
  69. def OAI.WLTime.RAMAlphabet.compute line 371
  70. theorem OAI.WLTime.RAMAlphabet.compute_exec line 374
  71. theorem OAI.WLTime.RAMAlphabet.compute_size line 390
  72. def OAI.WLTime.RAMAlphabet.opCost line 405
  73. def OAI.WLTime.RAMAlphabet.unitCost line 408
  74. theorem OAI.WLTime.RAMAlphabet.basic_le_unit line 409
  75. theorem OAI.WLTime.RAMAlphabet.unit_pos line 410
  76. theorem OAI.WLTime.RAMAlphabet.six_le_unit line 411
  77. theorem OAI.WLTime.RAMAlphabet.op_le_unit line 412
  78. theorem OAI.WLTime.RAMAlphabet.memory_le_unit line 416
  79. theorem OAI.WLTime.RAMAlphabet.test_le_unit line 420
  80. def OAI.WLTime.RAMAlphabet.haltCode line 422
  81. def OAI.WLTime.RAMAlphabet.jumpCode line 423
  82. theorem OAI.WLTime.RAMAlphabet.halt_exec line 424
  83. theorem OAI.WLTime.RAMAlphabet.jump_exec line 438
  84. theorem OAI.WLTime.RAMAlphabet.test_tops line 450
  85. theorem OAI.WLTime.RAMAlphabet.combine_cost line 453