OAI/ModelTheory/Choiceless/Stack.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CPTSeparation.StackLang.Store line 13
  2. inductive OAI.CPTSeparation.StackLang.Action line 17
  3. def OAI.CPTSeparation.StackLang.Action.run line 29
  4. def OAI.CPTSeparation.StackLang.Action.stmt line 37
  5. lemma OAI.CPTSeparation.StackLang.Action.stmt_run line 45
  6. inductive OAI.CPTSeparation.StackLang.Program line 59
  7. inductive OAI.CPTSeparation.StackLang.Exec line 65
  8. def OAI.CPTSeparation.StackLang.Program.Labels line 76
  9. instance OAI.CPTSeparation.StackLang.Program.finiteLabels line 82
  10. def OAI.CPTSeparation.StackLang.Program.start line 89
  11. def OAI.CPTSeparation.StackLang.Program.jump line 95
  12. lemma OAI.CPTSeparation.StackLang.Program.stepAux_jump line 99
  13. def OAI.CPTSeparation.StackLang.Program.code line 102
  14. def OAI.CPTSeparation.StackLang.configuration line 124
  15. def OAI.CPTSeparation.StackLang.one_step line 127
  16. def OAI.CPTSeparation.StackLang.Exec.simulates line 130
  17. def OAI.CPTSeparation.StackLang.Program.machine line 175
  18. instance OAI.CPTSeparation.StackLang.Program.machine_alphabet_finite line 186
  19. def OAI.CPTSeparation.StackLang.Program.compiles line 190
  20. abbrev OAI.CPTSeparation.StackLang.SStore line 202
  21. abbrev OAI.CPTSeparation.StackLang.SProgram line 204
  22. def OAI.CPTSeparation.StackLang.Runs line 206
  23. lemma OAI.CPTSeparation.StackLang.Runs.atom line 211
  24. lemma OAI.CPTSeparation.StackLang.Runs.atom_of line 214
  25. lemma OAI.CPTSeparation.StackLang.Runs.mono line 217
  26. lemma OAI.CPTSeparation.StackLang.Runs.seq line 222
  27. lemma OAI.CPTSeparation.StackLang.Runs.loop_false line 228
  28. lemma OAI.CPTSeparation.StackLang.Runs.loop_true line 231
  29. lemma OAI.CPTSeparation.StackLang.Runs.cond_true line 238
  30. lemma OAI.CPTSeparation.StackLang.Runs.cond_false line 243
  31. lemma OAI.CPTSeparation.StackLang.Runs.loop_steps line 248
  32. lemma OAI.CPTSeparation.StackLang.Store.ext' line 266
  33. def OAI.CPTSeparation.StackLang.Macros.state line 279
  34. def OAI.CPTSeparation.StackLang.Macros.peek line 281
  35. def OAI.CPTSeparation.StackLang.Macros.moveBody line 283
  36. def OAI.CPTSeparation.StackLang.Macros.moveLoop line 287
  37. def OAI.CPTSeparation.StackLang.Macros.moveRev line 290
  38. lemma OAI.CPTSeparation.StackLang.Macros.update_comm line 294
  39. lemma OAI.CPTSeparation.StackLang.Macros.moveLoop_runs line 302
  40. lemma OAI.CPTSeparation.StackLang.Macros.moveRev_runs line 333
  41. def OAI.CPTSeparation.StackLang.Macros.clearBody line 347
  42. def OAI.CPTSeparation.StackLang.Macros.clearLoop line 350
  43. def OAI.CPTSeparation.StackLang.Macros.clear line 352
  44. lemma OAI.CPTSeparation.StackLang.Macros.clearLoop_runs line 355
  45. lemma OAI.CPTSeparation.StackLang.Macros.clear_runs line 374
  46. def OAI.CPTSeparation.StackLang.Macros.dupeBody line 388
  47. def OAI.CPTSeparation.StackLang.Macros.dupeLoop line 392
  48. def OAI.CPTSeparation.StackLang.Macros.dupeRev line 395
  49. lemma OAI.CPTSeparation.StackLang.Macros.dupeLoop_runs line 397
  50. lemma OAI.CPTSeparation.StackLang.Macros.dupeRev_runs line 428
  51. def OAI.CPTSeparation.StackLang.Macros.copy line 441
  52. lemma OAI.CPTSeparation.StackLang.Macros.copy_runs line 444
  53. def OAI.CPTSeparation.StackLang.Macros.rowLoop line 472
  54. def OAI.CPTSeparation.StackLang.Macros.moveRow line 475
  55. lemma OAI.CPTSeparation.StackLang.Macros.rowLoop_runs line 479
  56. lemma OAI.CPTSeparation.StackLang.Macros.moveRow_runs line 519
  57. def OAI.CPTSeparation.StackLang.Macros.skipRowLoop line 551
  58. def OAI.CPTSeparation.StackLang.Macros.skipRow line 554
  59. lemma OAI.CPTSeparation.StackLang.Macros.skipRowLoop_runs line 558
  60. lemma OAI.CPTSeparation.StackLang.Macros.skipRow_runs line 582
  61. def OAI.CPTSeparation.StackLang.Macros.zipRowBody line 606
  62. def OAI.CPTSeparation.StackLang.Macros.zipRowLoop line 614
  63. def OAI.CPTSeparation.StackLang.Macros.zipRow line 618
  64. lemma OAI.CPTSeparation.StackLang.Macros.zipRowLoop_runs line 623
  65. lemma OAI.CPTSeparation.StackLang.Macros.zipRow_runs line 672