OAI/Computability/WeisfeilerLeman/Turing.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WLTime.OneTape line 9
  2. abbrev OAI.WLTime.OneTape.Cell line 20
  3. def OAI.WLTime.OneTape.action line 22
  4. structure OAI.WLTime.OneTape.Config line 25
  5. def OAI.WLTime.OneTape.moveAt line 30
  6. def OAI.WLTime.OneTape.step line 36
  7. def OAI.WLTime.OneTape.snapshot line 43
  8. def OAI.WLTime.OneTape.written line 46
  9. def OAI.WLTime.OneTape.arrival line 50
  10. def OAI.WLTime.OneTape.localRule line 54
  11. theorem OAI.WLTime.OneTape.written_snapshot line 59
  12. theorem OAI.WLTime.OneTape.arrival_snapshot line 65
  13. theorem OAI.WLTime.OneTape.moveAt_eq_iff line 72
  14. theorem OAI.WLTime.OneTape.snapshot_step line 80
  15. def OAI.WLTime.OneTape.run line 99
  16. theorem OAI.WLTime.OneTape.run_snapshot line 102
  17. def OAI.WLTime.OneTape.toTM line 115
  18. def OAI.WLTime.OneTape.embed line 125
  19. def OAI.WLTime.OneTape.lineShift line 130
  20. theorem OAI.WLTime.OneTape.moveAt_line line 132
  21. theorem OAI.WLTime.OneTape.embed_step line 135
  22. def OAI.WLTime.OneTape.initial line 150
  23. theorem OAI.WLTime.OneTape.embed_initial line 156
  24. theorem OAI.WLTime.OneTape.embed_run line 164
  25. theorem OAI.WLTime.OneTape.step_halted line 174
  26. theorem OAI.WLTime.OneTape.run_halted line 179
  27. theorem OAI.WLTime.OneTape.line_head_step line 184
  28. theorem OAI.WLTime.OneTape.line_head_run line 192
  29. def OAI.WLTime.OneTape.Agrees line 207
  30. theorem OAI.WLTime.OneTape.agrees_step line 210
  31. theorem OAI.WLTime.OneTape.agrees_run line 238
  32. theorem OAI.WLTime.OneTape.run_frozen_after line 254
  33. theorem OAI.WLTime.OneTape.accepts_iff_state line 262
  34. def OAI.WLTime.OneTape.protectedInterval line 281
  35. theorem OAI.WLTime.OneTape.protectedInterval_injective line 283
  36. def OAI.WLTime.OneTape.ringShift line 297
  37. def OAI.WLTime.OneTape.ringInitial line 299
  38. theorem OAI.WLTime.OneTape.ring_initial_agrees line 305
  39. theorem OAI.WLTime.OneTape.ring_run_agrees line 338
  40. def OAI.WLTime.OneTape.letterAccepting line 352
  41. theorem OAI.WLTime.OneTape.accepting_snapshot line 354
  42. theorem OAI.WLTime.OneTape.ring_accepts_iff line 366
  43. theorem OAI.WLTime.TM.run_add line 384
  44. theorem OAI.WLTime.TM.run_succ line 388
  45. theorem OAI.WLTime.TM.step_frozen line 391
  46. theorem OAI.WLTime.TM.run_frozen line 394
  47. theorem OAI.WLTime.TM.time_halted line 400
  48. theorem OAI.WLTime.TM.time_le_of_halted line 404
  49. theorem OAI.WLTime.TM.accepts_iff_at_halt line 409