OAI/Computability/WeisfeilerLeman/TapePair.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.WLTime.OneTape.Symbolic.FullWriter.Reg line 12
  2. instance OAI.WLTime.OneTape.Symbolic.FullWriter.(instance at line 15) line 15
  3. def OAI.WLTime.OneTape.Symbolic.FullWriter.args line 17
  4. def OAI.WLTime.OneTape.Symbolic.FullWriter.N line 18
  5. def OAI.WLTime.OneTape.Symbolic.FullWriter.R line 19
  6. def OAI.WLTime.OneTape.Symbolic.FullWriter.E line 20
  7. def OAI.WLTime.OneTape.Symbolic.FullWriter.L line 21
  8. def OAI.WLTime.OneTape.Symbolic.FullWriter.B line 22
  9. def OAI.WLTime.OneTape.Symbolic.FullWriter.P line 23
  10. def OAI.WLTime.OneTape.Symbolic.FullWriter.body line 24
  11. def OAI.WLTime.OneTape.Symbolic.FullWriter.rho line 25
  12. def OAI.WLTime.OneTape.Symbolic.FullWriter.program line 26
  13. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.eval_N line 32
  14. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.eval_L line 33
  15. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.eval_B line 38
  16. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.eval_P line 41
  17. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.safe line 45
  18. def OAI.WLTime.OneTape.Symbolic.FullWriter.budget line 67
  19. theorem OAI.WLTime.OneTape.Symbolic.FullWriter.correct line 71
  20. def OAI.WLTime.TypedStack.Code.mapLetters line 113
  21. def OAI.WLTime.TypedStack.Code.listMap line 121
  22. theorem OAI.WLTime.TypedStack.Code.listMap_update line 122
  23. theorem OAI.WLTime.TypedStack.Code.unmap_tops line 128
  24. theorem OAI.WLTime.TypedStack.Code.mapLetters_exec line 134
  25. theorem OAI.WLTime.TypedStack.Code.mapLetters_size line 150
  26. def OAI.WLTime.TypedStack.Command.transport line 156
  27. theorem OAI.WLTime.TypedStack.Execution.transport line 165
  28. theorem OAI.WLTime.TypedStack.Execution.transport_inr line 181
  29. theorem OAI.WLTime.TypedStack.Code.relabel_inl_exec line 199
  30. structure OAI.WLTime.TapePair.Tape line 211
  31. def OAI.WLTime.TapePair.contents line 216
  32. def OAI.WLTime.TapePair.moveWrite line 219
  33. theorem OAI.WLTime.TapePair.getD_tail line 224
  34. theorem OAI.WLTime.TapePair.getD_nonneg line 227
  35. theorem OAI.WLTime.TapePair.contents_moveWrite line 235
  36. theorem OAI.WLTime.TapePair.contents_zero line 285
  37. def OAI.WLTime.TMStack.store line 295
  38. def OAI.WLTime.TMStack.single line 298
  39. def OAI.WLTime.TMStack.tapeCost line 304
  40. theorem OAI.WLTime.TMStack.single_exec line 308
  41. def OAI.WLTime.TMStack.body line 348
  42. def OAI.WLTime.TMStack.bodyCost line 352
  43. theorem OAI.WLTime.TMStack.bodyCost_le line 355
  44. theorem OAI.WLTime.TMStack.body_exec line 364
  45. def OAI.WLTime.TMStack.blank line 388
  46. instance OAI.WLTime.TMStack.moveFintype line 389
  47. abbrev OAI.WLTime.TMStack.Payload line 391
  48. def OAI.WLTime.TMStack.stepCode line 392
  49. abbrev OAI.WLTime.TMStack.State line 394
  50. instance OAI.WLTime.TMStack.(instance at line 395) line 395
  51. def OAI.WLTime.TMStack.transition line 398
  52. def OAI.WLTime.TMStack.machine line 406
  53. def OAI.WLTime.TMStack.Relative line 412
  54. def OAI.WLTime.TMStack.nextTapes line 415
  55. theorem OAI.WLTime.TMStack.stepCode_exec line 418
  56. theorem OAI.WLTime.TMStack.observed line 425
  57. theorem OAI.WLTime.TMStack.next_relative line 434