OAI/Computability/WeisfeilerLeman/RAMMemory.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLTime.TMPort.output_symbol line 10
  2. theorem OAI.WLTime.TMPort.extract_exec line 12
  3. theorem OAI.WLTime.TMPort.extract_inner line 41
  4. def OAI.WLTime.TMPort.privateRegs line 58
  5. def OAI.WLTime.TMPort.program line 59
  6. def OAI.WLTime.TMPort.factor line 61
  7. theorem OAI.WLTime.TMPort.input_mass line 62
  8. theorem OAI.WLTime.TMPort.private_nodup line 68
  9. theorem OAI.WLTime.TMPort.private_mem line 70
  10. theorem OAI.WLTime.TMPort.cleanup line 72
  11. theorem OAI.WLTime.TMPort.program_exec line 88
  12. theorem OAI.WLTime.TMPort.size_load line 113
  13. theorem OAI.WLTime.TMPort.size_extract line 115
  14. def OAI.WLTime.TMPort.sizeFactor line 117
  15. theorem OAI.WLTime.TMPort.program_size line 118
  16. theorem OAI.WLTime.TypedStack.Code.readN_prefix line 125
  17. abbrev OAI.WLTime.RAMSlices.Reg line 135
  18. def OAI.WLTime.RAMSlices.state line 136
  19. def OAI.WLTime.RAMSlices.read line 137
  20. def OAI.WLTime.RAMSlices.write line 140
  21. theorem OAI.WLTime.RAMSlices.read_exec line 143
  22. theorem OAI.WLTime.RAMSlices.write_exec line 184
  23. theorem OAI.WLTime.RAMSlices.read_size line 218
  24. theorem OAI.WLTime.RAMSlices.write_size line 221
  25. theorem OAI.WLTime.RegisterFile.flatten_length line 227
  26. theorem OAI.WLTime.RegisterFile.length line 236
  27. theorem OAI.WLTime.RegisterFile.zero line 240
  28. theorem OAI.WLTime.RegisterFile.update_list line 242
  29. theorem OAI.WLTime.RegisterFile.split line 254
  30. abbrev OAI.WLTime.RAMMemory.Reg line 284
  31. def OAI.WLTime.RAMMemory.state line 285
  32. def OAI.WLTime.RAMMemory.keyMap line 287
  33. def OAI.WLTime.RAMMemory.valueMap line 288
  34. def OAI.WLTime.RAMMemory.lookupMap line 289
  35. def OAI.WLTime.RAMMemory.storeMap line 290
  36. theorem OAI.WLTime.RAMMemory.keyMap_inj line 291
  37. theorem OAI.WLTime.RAMMemory.valueMap_inj line 292
  38. theorem OAI.WLTime.RAMMemory.lookupMap_inj line 293
  39. theorem OAI.WLTime.RAMMemory.storeMap_inj line 294
  40. def OAI.WLTime.RAMMemory.readKey line 295
  41. def OAI.WLTime.RAMMemory.readValue line 296
  42. def OAI.WLTime.RAMMemory.writeValue line 297
  43. def OAI.WLTime.RAMMemory.lookup line 298
  44. def OAI.WLTime.RAMMemory.store line 299
  45. def OAI.WLTime.RAMMemory.load line 300
  46. def OAI.WLTime.RAMMemory.save line 302
  47. theorem OAI.WLTime.RAMMemory.readKey_exec line 304
  48. theorem OAI.WLTime.RAMMemory.readValue_exec line 316
  49. theorem OAI.WLTime.RAMMemory.writeValue_exec line 328
  50. theorem OAI.WLTime.RAMMemory.lookup_exec line 340
  51. theorem OAI.WLTime.RAMMemory.store_exec line 349
  52. theorem OAI.WLTime.RAMMemory.clear_key line 359
  53. theorem OAI.WLTime.RAMMemory.clear_value line 364
  54. def OAI.WLTime.RAMMemory.cost line 369
  55. theorem OAI.WLTime.RAMMemory.cost_arith line 370
  56. theorem OAI.WLTime.RAMMemory.load_exec line 379
  57. theorem OAI.WLTime.RAMMemory.save_exec line 390
  58. theorem OAI.WLTime.RAMMemory.load_size line 402
  59. theorem OAI.WLTime.RAMMemory.save_size line 411