OAI/Computability/MatchingCount/FiniteStack.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.StackCode.Store line 9
  2. inductive OAI.BinaryMatching.StackCode.Instr line 11
  3. def OAI.BinaryMatching.StackCode.Instr.map line 20
  4. def OAI.BinaryMatching.StackCode.Instr.eval line 26
  5. theorem OAI.BinaryMatching.StackCode.Instr.eval_map line 32
  6. abbrev OAI.BinaryMatching.StackCode.Instr.Stmt line 40
  7. def OAI.BinaryMatching.StackCode.Instr.target line 42
  8. def OAI.BinaryMatching.StackCode.Instr.translate line 45
  9. theorem OAI.BinaryMatching.StackCode.Instr.target_step line 52
  10. theorem OAI.BinaryMatching.StackCode.Instr.translate_step line 55
  11. structure OAI.BinaryMatching.StackCode.Block line 68
  12. inductive OAI.BinaryMatching.StackCode.Steps line 76
  13. theorem OAI.BinaryMatching.StackCode.Steps.trans line 86
  14. theorem OAI.BinaryMatching.StackCode.Steps.map line 93
  15. abbrev OAI.BinaryMatching.StackCode.Steps.cfg line 103
  16. theorem OAI.BinaryMatching.StackCode.Steps.simulation line 106
  17. def OAI.BinaryMatching.StackCode.Block.primitive line 119
  18. def OAI.BinaryMatching.StackCode.Block.seq line 125
  19. def OAI.BinaryMatching.StackCode.Block.cases line 133
  20. def OAI.BinaryMatching.StackCode.Block.loop line 144
  21. abbrev OAI.BinaryMatching.StackCode.Block.Runs line 152
  22. theorem OAI.BinaryMatching.StackCode.Block.primitive_runs line 155
  23. theorem OAI.BinaryMatching.StackCode.Block.seq_runs line 161
  24. def OAI.BinaryMatching.StackCode.Block.machine line 172
  25. theorem OAI.BinaryMatching.StackCode.Block.machine_finite line 183
  26. def OAI.BinaryMatching.StackCode.Block.machine_runs line 188