OAI/Combinatorics/VariableWL/MultiStack.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VariableWL.StackSimulation.next_length line 13
  2. theorem OAI.VariableWL.StackSimulation.evolve_length line 21
  3. theorem OAI.VariableWL.StackSimulation.one_bound line 30
  4. theorem OAI.VariableWL.StackSimulation.run_bound line 50
  5. theorem OAI.VariableWL.BoundedSimulation.Steps.rebase line 75
  6. def OAI.VariableWL.UnitSimulation.instructions line 86
  7. theorem OAI.VariableWL.UnitSimulation.statement_bound line 95
  8. theorem OAI.VariableWL.UnitSimulation.one_bound line 137
  9. theorem OAI.VariableWL.UnitSimulation.steps_support line 149
  10. theorem OAI.VariableWL.UnitSimulation.steps_bound line 156
  11. abbrev OAI.VariableWL.MultiStack.K line 174
  12. abbrev OAI.VariableWL.MultiStack.Γ line 175
  13. abbrev OAI.VariableWL.MultiStack.Q line 176
  14. abbrev OAI.VariableWL.MultiStack.Slot line 177
  15. abbrev OAI.VariableWL.MultiStack.Stacks line 178
  16. abbrev OAI.VariableWL.MultiStack.Data line 179
  17. inductive OAI.VariableWL.MultiStack.Label line 181
  18. instance OAI.VariableWL.MultiStack.(instance at line 186) line 186
  19. instance OAI.VariableWL.MultiStack.(instance at line 190) line 190
  20. structure OAI.VariableWL.MultiStack.Vars line 192
  21. abbrev OAI.VariableWL.MultiStack.Statement line 197
  22. abbrev OAI.VariableWL.MultiStack.Config line 198
  23. instance OAI.VariableWL.MultiStack.(instance at line 200) line 200
  24. def OAI.VariableWL.MultiStack.getData line 202
  25. def OAI.VariableWL.MultiStack.tape line 203
  26. def OAI.VariableWL.MultiStack.readVars line 205
  27. def OAI.VariableWL.MultiStack.readAll line 208
  28. theorem OAI.VariableWL.MultiStack.readAll_sem line 213
  29. def OAI.VariableWL.MultiStack.allTapes line 230
  30. theorem OAI.VariableWL.MultiStack.readVars_all line 232
  31. def OAI.VariableWL.MultiStack.writeVars line 239
  32. def OAI.VariableWL.MultiStack.writeStacks line 244
  33. def OAI.VariableWL.MultiStack.writeTape line 251
  34. theorem OAI.VariableWL.MultiStack.writeTape_sem line 261
  35. theorem OAI.VariableWL.MultiStack.writeVars_data line 274
  36. theorem OAI.VariableWL.MultiStack.writeStacks_other line 277
  37. def OAI.VariableWL.MultiStack.applyMotion line 283
  38. theorem OAI.VariableWL.MultiStack.tape_writeStacks line 288
  39. def OAI.VariableWL.MultiStack.writeAll line 295
  40. def OAI.VariableWL.MultiStack.applyStacks line 299
  41. theorem OAI.VariableWL.MultiStack.writeAll_sem line 303
  42. theorem OAI.VariableWL.MultiStack.tape_applyStacks line 315
  43. def OAI.VariableWL.MultiStack.program line 330
  44. def OAI.VariableWL.MultiStack.Related line 350
  45. theorem OAI.VariableWL.MultiStack.applyMotion_nth line 354
  46. theorem OAI.VariableWL.MultiStack.allTapes_mem line 358
  47. theorem OAI.VariableWL.MultiStack.allTapes_nodup line 360
  48. theorem OAI.VariableWL.MultiStack.simulate_step line 364
  49. theorem OAI.VariableWL.MultiStack.simulate_steps line 403
  50. theorem OAI.VariableWL.MultiStack.simulate_halt line 413
  51. def OAI.VariableWL.MultiStack.inputSymbol line 435
  52. def OAI.VariableWL.MultiStack.initialStacks line 437
  53. def OAI.VariableWL.MultiStack.initialConfig line 440
  54. theorem OAI.VariableWL.MultiStack.initialConfig_eq line 442
  55. theorem OAI.VariableWL.MultiStack.tape_nth_nat line 444
  56. theorem OAI.VariableWL.MultiStack.tape_nth_neg line 446
  57. theorem OAI.VariableWL.MultiStack.initial_related line 449
  58. theorem OAI.VariableWL.MultiStack.initial_lengths line 482
  59. theorem OAI.VariableWL.BoundedSimulation.evolve_steps line 492
  60. theorem OAI.VariableWL.run_eq_evolve line 504