OAI/Computability/VertexCover/Machines/Primitive.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VertexCover.Machine.Stream.K line 46
  2. abbrev OAI.VertexCover.Machine.Stream.Γ line 47
  3. abbrev OAI.VertexCover.Machine.Stream.State line 48
  4. abbrev OAI.VertexCover.Machine.Stream.Stmt line 49
  5. abbrev OAI.VertexCover.Machine.Stream.Cfg line 50
  6. theorem OAI.VertexCover.Machine.Stream.cfg_ext line 53
  7. def OAI.VertexCover.Machine.Stream.emit line 56
  8. theorem OAI.VertexCover.Machine.Stream.emit_step line 62
  9. def OAI.VertexCover.Machine.Stream.program line 81
  10. abbrev OAI.VertexCover.Machine.Stream.machine line 92
  11. def OAI.VertexCover.Machine.Stream.output line 103
  12. def OAI.VertexCover.Machine.Stream.finalState line 107
  13. def OAI.VertexCover.Machine.Stream.tapes line 111
  14. theorem OAI.VertexCover.Machine.Stream.tapes_zero line 112
  15. theorem OAI.VertexCover.Machine.Stream.tapes_one line 113
  16. theorem OAI.VertexCover.Machine.Stream.tapes_two line 114
  17. theorem OAI.VertexCover.Machine.Stream.update_zero line 116
  18. theorem OAI.VertexCover.Machine.Stream.update_one line 118
  19. theorem OAI.VertexCover.Machine.Stream.update_two line 120
  20. abbrev OAI.VertexCover.Machine.Stream.cfg line 123
  21. theorem OAI.VertexCover.Machine.Stream.scan_cons line 129
  22. theorem OAI.VertexCover.Machine.Stream.scan_nil line 139
  23. theorem OAI.VertexCover.Machine.Stream.reverse_cons line 148
  24. theorem OAI.VertexCover.Machine.Stream.reverse_nil line 155
  25. def OAI.VertexCover.Machine.Stream.scan_run line 165
  26. def OAI.VertexCover.Machine.Stream.reverse_run line 179
  27. theorem OAI.VertexCover.Machine.Stream.initial_eq line 191
  28. def OAI.VertexCover.Machine.Stream.execution line 196
  29. theorem OAI.VertexCover.Machine.Stream.output_length line 210
  30. def OAI.VertexCover.Machine.Stream.poly line 222