OAI/Computability/WeisfeilerLeman/SparseStore.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.SparseLookup.answer line 9
  2. def OAI.WLTime.SparseLookup.supplyZero line 11
  3. def OAI.WLTime.SparseLookup.program line 13
  4. theorem OAI.WLTime.SparseLookup.supplyZero_exec line 15
  5. theorem OAI.WLTime.SparseLookup.program_exec line 31
  6. theorem OAI.WLTime.SparseLookup.program_size line 51
  7. abbrev OAI.WLTime.WordMemory.Log line 60
  8. def OAI.WLTime.WordMemory.read line 61
  9. def OAI.WLTime.WordMemory.entries line 64
  10. theorem OAI.WLTime.WordMemory.entries_wellFormed line 66
  11. theorem OAI.WLTime.WordMemory.entries_length line 70
  12. theorem OAI.WLTime.WordMemory.word_zero line 71
  13. theorem OAI.WLTime.WordMemory.answer_read line 73
  14. theorem OAI.WLTime.WordMemory.lookup_exec line 87
  15. theorem OAI.WLTime.WordMemory.read_prepend line 96
  16. abbrev OAI.WLTime.SparseStore.Reg line 103
  17. def OAI.WLTime.SparseStore.state line 104
  18. def OAI.WLTime.SparseStore.program line 105
  19. theorem OAI.WLTime.SparseStore.program_exec line 106
  20. theorem OAI.WLTime.BitWords.value_sum line 128
  21. def OAI.WLTime.WordMemory.chunk line 149
  22. theorem OAI.WLTime.WordMemory.chunk_length line 151
  23. theorem OAI.WLTime.WordMemory.chunk_value line 152
  24. theorem OAI.WLTime.WordMemory.packed_bits line 160
  25. theorem OAI.WLTime.WordMemory.chunk_zero line 172
  26. def OAI.WLTime.WordMemory.address line 177
  27. theorem OAI.WLTime.WordMemory.address_val line 178
  28. theorem OAI.WLTime.WordMemory.address_eq line 179
  29. def OAI.WLTime.WordMemory.initialLog line 181
  30. theorem OAI.WLTime.WordMemory.initialLog_length line 184
  31. theorem OAI.WLTime.WordMemory.read_initialLog line 188
  32. theorem OAI.WLTime.WordMemory.initialLog_correct line 202
  33. theorem OAI.WLTime.WordMemory.number_of_chunks line 210
  34. theorem OAI.WLTime.BitWords.eq_word line 219
  35. theorem OAI.WLTime.BitWords.inc_address line 225
  36. abbrev OAI.WLTime.RAMInput.Reg line 235
  37. def OAI.WLTime.RAMInput.state line 236
  38. def OAI.WLTime.RAMInput.storeMap line 238
  39. theorem OAI.WLTime.RAMInput.storeMap_inj line 239
  40. def OAI.WLTime.RAMInput.body line 240
  41. def OAI.WLTime.RAMInput.running line 243
  42. def OAI.WLTime.RAMInput.loopCode line 244
  43. def OAI.WLTime.RAMInput.program line 245
  44. theorem OAI.WLTime.RAMInput.body_exec line 247
  45. def OAI.WLTime.RAMInput.packedState line 291
  46. theorem OAI.WLTime.RAMInput.body_packed line 294
  47. theorem OAI.WLTime.RAMInput.loop_packed line 308
  48. theorem OAI.WLTime.RAMInput.program_exec line 325
  49. theorem OAI.WLTime.RAMInput.body_size line 349
  50. theorem OAI.WLTime.RAMInput.program_size line 352
  51. theorem OAI.WLTime.TypedStack.Code.readN_all line 360
  52. theorem OAI.WLTime.TypedStack.Code.readN_map line 366
  53. abbrev OAI.WLTime.TMPort.Letter line 377
  54. abbrev OAI.WLTime.TMPort.Reg line 378
  55. def OAI.WLTime.TMPort.port line 379
  56. def OAI.WLTime.TMPort.temp line 380
  57. def OAI.WLTime.TMPort.result line 381
  58. def OAI.WLTime.TMPort.tapeIn line 382
  59. def OAI.WLTime.TMPort.inputSymbol line 383
  60. def OAI.WLTime.TMPort.outputSymbol line 386
  61. def OAI.WLTime.TMPort.unletter line 389
  62. def OAI.WLTime.TMPort.inputState line 392
  63. def OAI.WLTime.TMPort.innerState line 394
  64. def OAI.WLTime.TMPort.load line 396
  65. def OAI.WLTime.TMPort.runCode line 400
  66. def OAI.WLTime.TMPort.rewindCode line 402
  67. def OAI.WLTime.TMPort.extract line 404
  68. theorem OAI.WLTime.TMPort.load_exec line 407
  69. theorem OAI.WLTime.TMPort.run_exec line 445
  70. theorem OAI.WLTime.TMPort.rewind_exec line 456