OAI/Computability/VertexCover/Machines/Loop.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VertexCover.Machine.Loop.K line 47
  2. abbrev OAI.VertexCover.Machine.Loop.Γ line 48
  3. abbrev OAI.VertexCover.Machine.Loop.Λ line 49
  4. abbrev OAI.VertexCover.Machine.Loop.State line 50
  5. abbrev OAI.VertexCover.Machine.Loop.Cfg line 51
  6. abbrev OAI.VertexCover.Machine.Loop.Stmt line 52
  7. abbrev OAI.VertexCover.Machine.Loop.temporary line 53
  8. abbrev OAI.VertexCover.Machine.Loop.output line 54
  9. abbrev OAI.VertexCover.Machine.Loop.phase line 55
  10. abbrev OAI.VertexCover.Machine.Loop.haltTarget line 56
  11. abbrev OAI.VertexCover.Machine.Loop.tapes line 57
  12. def OAI.VertexCover.Machine.Loop.extra line 61
  13. abbrev OAI.VertexCover.Machine.Loop.program line 83
  14. abbrev OAI.VertexCover.Machine.Loop.machine line 85
  15. def OAI.VertexCover.Machine.Loop.extraTapes line 99
  16. theorem OAI.VertexCover.Machine.Loop.extraTapes_false line 103
  17. theorem OAI.VertexCover.Machine.Loop.extraTapes_true line 104
  18. theorem OAI.VertexCover.Machine.Loop.tapes_update_extra line 106
  19. theorem OAI.VertexCover.Machine.Loop.update_extra_false line 116
  20. theorem OAI.VertexCover.Machine.Loop.update_extra_true line 120
  21. abbrev OAI.VertexCover.Machine.Loop.embedded line 124
  22. def OAI.VertexCover.Machine.Loop.cfg1 line 127
  23. def OAI.VertexCover.Machine.Loop.cfg2true line 133
  24. def OAI.VertexCover.Machine.Loop.cfg2false line 138
  25. theorem OAI.VertexCover.Machine.Loop.cfg_ext line 143
  26. theorem OAI.VertexCover.Machine.Loop.halt_label line 150
  27. theorem OAI.VertexCover.Machine.Loop.halt_var line 152
  28. theorem OAI.VertexCover.Machine.Loop.cfg0_step line 154
  29. theorem OAI.VertexCover.Machine.Loop.cfg1_cons line 165
  30. theorem OAI.VertexCover.Machine.Loop.cfg1_nil_true line 178
  31. theorem OAI.VertexCover.Machine.Loop.cfg1_nil_false line 188
  32. theorem OAI.VertexCover.Machine.Loop.cfg2true_cons line 198
  33. theorem OAI.VertexCover.Machine.Loop.cfg2false_cons line 209
  34. theorem OAI.VertexCover.Machine.Loop.initial_eq line 221
  35. theorem OAI.VertexCover.Machine.Loop.cfg2true_nil line 236
  36. theorem OAI.VertexCover.Machine.Loop.cfg2false_nil line 248
  37. def OAI.VertexCover.Machine.Loop.cfg1_run_true line 265
  38. def OAI.VertexCover.Machine.Loop.cfg1_run_false line 278
  39. def OAI.VertexCover.Machine.Loop.cfg2true_run line 291
  40. def OAI.VertexCover.Machine.Loop.cfg2false_run line 305
  41. def OAI.VertexCover.Machine.Loop.bodyRun line 319
  42. def OAI.VertexCover.Machine.Loop.restart line 334
  43. def OAI.VertexCover.Machine.Loop.finish line 356
  44. theorem OAI.VertexCover.Machine.Loop.finiteAlphabet line 376
  45. inductive OAI.VertexCover.Machine.BoundedRun line 384
  46. def OAI.VertexCover.Machine.loopCost line 392
  47. theorem OAI.VertexCover.Machine.loopCost_bound line 397
  48. theorem OAI.VertexCover.Machine.boundedRun_execution line 410
  49. def OAI.VertexCover.Machine.Poly.loop line 436