OAI/Combinatorics/UniformKServer/StackCompiler.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Finite-control, finite-alphabet stack processors, compiled to the exact binary multitape model. There is no unit-cost arithmetic oracle.

  1. instance OAI.UniformKServer.StackCompiler.(instance at line 14) line 14
  2. inductive OAI.UniformKServer.StackCompiler.Op line 16
  3. structure OAI.UniformKServer.StackCompiler.Action line 20
  4. structure OAI.UniformKServer.StackCompiler.Processor line 28
  5. structure OAI.UniformKServer.StackCompiler.State line 32
  6. def OAI.UniformKServer.StackCompiler.applyOp line 39
  7. def OAI.UniformKServer.StackCompiler.step line 45
  8. def OAI.UniformKServer.StackCompiler.initial line 51
  9. def OAI.UniformKServer.StackCompiler.install line 54
  10. def OAI.UniformKServer.StackCompiler.code line 57
  11. def OAI.UniformKServer.StackCompiler.decode line 59
  12. theorem OAI.UniformKServer.StackCompiler.decode_none line 62
  13. theorem OAI.UniformKServer.StackCompiler.decode_code line 68
  14. abbrev OAI.UniformKServer.StackCompiler.controls line 76
  15. def OAI.UniformKServer.StackCompiler.ctl line 77
  16. def OAI.UniformKServer.StackCompiler.wire line 78
  17. def OAI.UniformKServer.StackCompiler.machine line 80
  18. structure OAI.UniformKServer.StackCompiler.Matches line 107
  19. theorem OAI.UniformKServer.StackCompiler.matches_initial line 115
  20. theorem OAI.UniformKServer.StackCompiler.matches_install line 119
  21. theorem OAI.UniformKServer.StackCompiler.matches_heads line 124