OAI/Computability/WeisfeilerLeman/RAMSimulation.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLTime.RAMAlphabet.instruction line 12
  2. theorem OAI.WLTime.RAMAlphabet.bound_mono line 27
  3. theorem OAI.WLTime.RAMAlphabet.instruction_exec line 29
  4. theorem OAI.WLTime.RAMAlphabet.encode_length_bound line 118
  5. def OAI.WLTime.RAMAlphabet.exponent line 122
  6. def OAI.WLTime.RAMAlphabet.opConstant line 123
  7. def OAI.WLTime.RAMAlphabet.constant line 125
  8. theorem OAI.WLTime.RAMAlphabet.opCost_bound line 126
  9. theorem OAI.WLTime.RAMAlphabet.unitCost_bound line 142
  10. def OAI.WLTime.RAMAlphabet.opSizeConstant line 157
  11. theorem OAI.WLTime.RAMAlphabet.compute_linear line 158
  12. theorem OAI.WLTime.RAMAlphabet.instruction_linear line 166
  13. theorem OAI.WLTime.TypedStack.Code.casesList_size line 224
  14. theorem OAI.WLTime.TypedStack.Code.casesAll_size line 230
  15. theorem OAI.WLTime.SparseRAM.iterate_fixed line 237
  16. def OAI.WLTime.RAMAlphabet.depth line 248
  17. theorem OAI.WLTime.RAMAlphabet.depth_le line 249
  18. theorem OAI.WLTime.RAMAlphabet.depth_pos line 250
  19. def OAI.WLTime.RAMAlphabet.selectPC line 251
  20. def OAI.WLTime.RAMAlphabet.dispatch line 255
  21. def OAI.WLTime.RAMAlphabet.stepBound line 257
  22. theorem OAI.WLTime.RAMAlphabet.stepBound_mono line 258
  23. theorem OAI.WLTime.RAMAlphabet.select_state line 261
  24. theorem OAI.WLTime.RAMAlphabet.dispatch_exec line 263
  25. def OAI.WLTime.RAMAlphabet.running line 276
  26. def OAI.WLTime.RAMAlphabet.loopCode line 277
  27. theorem OAI.WLTime.RAMAlphabet.running_state line 278
  28. theorem OAI.WLTime.RAMAlphabet.loop_exec line 281
  29. theorem OAI.WLTime.RAMAlphabet.dispatch_linear line 315
  30. def OAI.WLTime.RAMAlphabet.inputMap line 332
  31. theorem OAI.WLTime.RAMAlphabet.inputMap_inj line 333
  32. def OAI.WLTime.RAMAlphabet.loader line 336
  33. theorem OAI.WLTime.RAMAlphabet.loader_exec line 337
  34. def OAI.WLTime.RAMAlphabet.inputState line 347
  35. def OAI.WLTime.RAMAlphabet.initial line 348
  36. def OAI.WLTime.RAMAlphabet.initCode line 353
  37. def OAI.WLTime.RAMAlphabet.initBound line 356
  38. theorem OAI.WLTime.RAMAlphabet.init_exec line 357
  39. theorem OAI.WLTime.RAMAlphabet.initial_forget line 385
  40. def OAI.WLTime.RAMAlphabet.program line 390
  41. def OAI.WLTime.RAMAlphabet.budget line 391
  42. theorem OAI.WLTime.RAMAlphabet.program_exec line 392
  43. theorem OAI.WLTime.RAMAlphabet.init_linear line 420
  44. theorem OAI.WLTime.RAMAlphabet.program_linear line 424