OAI/Computability/SpaceSimulation/OneTape/Layout.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Fifths.Entry.code line 9

    Also declared: ComparatorChallenges/OneTapeSpace.lean:209 (same declaration text).

  2. theorem OAI.Fifths.Entry.code_lt line 12
  3. theorem OAI.Fifths.Entry.code_inj line 15
  4. def OAI.Fifths.Entry.parse line 19
  5. theorem OAI.Fifths.Entry.code_parse line 23
  6. theorem OAI.Fifths.Entry.parse_code line 25
  7. abbrev OAI.Fifths.Square line 33

    Source documentation

    Shifted by T into natural-address range; then the block partition can be computed with unsigned arithmetic.

    abbrev Square (T : ℕ) := Fin (2*T+1)
…
  8. def OAI.Fifths.Square.cut line 36
  9. theorem OAI.Fifths.Square.cut_ok line 37
  10. def OAI.Fifths.Square.atDisp line 38
  11. def OAI.Fifths.Square.disp line 39
  12. theorem OAI.Fifths.Square.bounded line 41
  13. theorem OAI.Fifths.Square.disp_at line 44
  14. theorem OAI.Fifths.Square.disp_inj line 51
  15. theorem OAI.Fifths.Square.at_disp line 53
  16. def OAI.Fifths.Square.adjacent line 56
  17. theorem OAI.Fifths.Square.adj line 61
  18. structure OAI.Fifths.Site line 77
  19. def OAI.Fifths.Site.b line 87
  20. theorem OAI.Fifths.Site.b_pos line 88
  21. def OAI.Fifths.Site.N line 89
  22. def OAI.Fifths.Site.home line 90
  23. def OAI.Fifths.Site.slot line 91
  24. theorem OAI.Fifths.Site.home_lt line 93
  25. theorem OAI.Fifths.Site.slot_lt line 99
  26. def OAI.Fifths.Site.reach line 101
  27. def OAI.Fifths.Site.pin line 103
  28. theorem OAI.Fifths.Site.packed_index line 105
  29. theorem OAI.Fifths.Site.pin_ok line 108
  30. theorem OAI.Fifths.Site.backwards line 118
  31. def OAI.Fifths.Single.w line 134

    Source documentation

    Field of a controller is w(T) bits. Pad cell entries even further, to match a controller as a whole, for one consistent block radix.

    def w (T : ℕ) := (2*T + Fintype.card M.Q + Fintype.card M.A + 1).size
  32. def OAI.Fifths.Single.q line 135
  33. def OAI.Fifths.Single.fields line 136
  34. def OAI.Fifths.Single.c line 137
  35. def OAI.Fifths.Single.radix line 138
  36. theorem OAI.Fifths.Single.qpos line 140
  37. theorem OAI.Fifths.Single.short line 141
  38. theorem OAI.Fifths.Single.powers line 146
  39. theorem OAI.Fifths.Single.rpos line 149
  40. theorem OAI.Fifths.Single.moduli line 150
  41. structure OAI.Fifths.Single.Control line 155
  42. def OAI.Fifths.Single.key line 161
  43. def OAI.Fifths.Single.packCtrl line 165
  44. def OAI.Fifths.Single.parseCtrl line 167
  45. theorem OAI.Fifths.Single.key_lt line 170
  46. theorem OAI.Fifths.Single.packed_short line 180
  47. theorem OAI.Fifths.Single.roundtrip line 183