OAI/Computability/FiniteCompiler/UniformControl.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Uniform validation, simulation, and finite control.

  1. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.primrec_rightStep line 18
  2. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.primrec_step line 62
  3. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.sectorList line 71

    Source documentation

    Only control heads in the supplied literal support are enumerated. The ambient coded head type need not be finite.

    noncomputable def sectorList [Fintype B] [Fintype T] (heads : List H) (n : ℕ) : List (Sector H B T) :=
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Sector

  4. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.mem_sectorList line 77
  5. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.primrec_sectorList line 83
  6. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.universeList line 99
  7. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.mem_universeList line 104
  8. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.primrec_universeList line 114
  9. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.componentList line 122
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.primrec_componentList line 126
  11. inductive OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.Static line 141
  12. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.ofStatic line 148
  13. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.dynamic line 155
  14. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.simCode line 157
  15. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.controlCode line 173
  16. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.surfaceCode line 191
  17. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.pathCode line 200
  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_simCode line 227
  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_simDecode line 228
  20. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_ofStatic line 229
  21. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_dynamic line 231
  22. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlCode line 234
  23. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlDecode line 235
  24. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_machine line 236
  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_surfaceCode line 239
  26. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_surfaceDecode line 240
  27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_internal line 241
  28. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_pathCode line 244
  29. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_pathDecode line 246
  30. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.stateMap line 256
  31. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.controlMap line 260
  32. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.commandMap line 264
  33. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.commandCode line 266
  34. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_commandCode line 276
  35. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_commandState line 279
  36. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_commandWrite line 282
  37. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_commandMove line 285
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_commandMk line 288
  39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_stateMap line 294
  40. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlMap line 302
  41. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_instruction line 310
  42. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.stateMap_injective line 316
  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.controlMap_injective line 323
  44. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table_direction_map line 338
  45. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table_boundary_map line 342
  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Simulator.table_cell_map line 348
  47. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.dummy line 382
  48. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.static_cell line 385
  49. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_staticCell line 399
  50. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.leftCross line 415
  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_leftCell line 419
  52. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_runWorkspace line 433
  53. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_runCell line 461
  54. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_simCell line 472
  55. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.staticBoundary line 491
  56. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_simBoundary line 496
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_simDirection line 508
  58. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.staticControl line 518
  59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.validatorHead_map line 521
  60. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.staticControl_cell line 526
  61. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.staticControl_boundary line 540
  62. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlStaticCell line 552
  63. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlCell line 569
  64. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlBoundary line 589
  65. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlDirection line 609
  66. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.table_direction_map line 629
  67. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.table_boundary_map line 635
  68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.table_cell_map line 648
  69. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.entry_map line 663
  70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.success_map line 669
  71. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.simSupport line 681
  72. def OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.controlSupport line 683
  73. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.mem_simSupport line 686
  74. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.mem_controlSupport line 697
  75. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_simSupport line 712
  76. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.HeadCodec.primrec_controlSupport line 721
  77. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.rawSweep_takeDrop line 737
  78. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_rawSweep line 753
  79. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_rawNormal line 765
  80. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_trimQuota line 775
  81. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_quotaNormal line 778
  82. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_unmerge line 794
  83. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_pendingPreprocess line 829
  84. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_cleanupNormal line 832
  85. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_cleanupPreprocess line 849