OAI/Computability/PerfectCompleteness/Machines/TupleIndexMachine.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TupleIndexMachine.Tape line 15
  2. abbrev OAI.PerfectCompleteness.TupleIndexMachine.Register line 16
  3. def OAI.PerfectCompleteness.TupleIndexMachine.source line 18
  4. def OAI.PerfectCompleteness.TupleIndexMachine.cleanupTapes line 20
  5. abbrev OAI.PerfectCompleteness.TupleIndexMachine.Label line 24
  6. def OAI.PerfectCompleteness.TupleIndexMachine.initLabel line 29
  7. def OAI.PerfectCompleteness.TupleIndexMachine.enumerationLabel line 31
  8. def OAI.PerfectCompleteness.TupleIndexMachine.cleanupLabel line 34
  9. def OAI.PerfectCompleteness.TupleIndexMachine.cleanupEntry line 37
  10. def OAI.PerfectCompleteness.TupleIndexMachine.program line 40
  11. def OAI.PerfectCompleteness.TupleIndexMachine.machine line 47
  12. def OAI.PerfectCompleteness.TupleIndexMachine.cfg line 58
  13. def OAI.PerfectCompleteness.TupleIndexMachine.inputTapes line 61
  14. def OAI.PerfectCompleteness.TupleIndexMachine.output line 64
  15. def OAI.PerfectCompleteness.TupleIndexMachine.readyTapes line 67
  16. def OAI.PerfectCompleteness.TupleIndexMachine.emittedTapes line 70
  17. theorem OAI.PerfectCompleteness.TupleIndexMachine.output_eq line 73
  18. theorem OAI.PerfectCompleteness.TupleIndexMachine.initialized_eq line 79
  19. def OAI.PerfectCompleteness.TupleIndexMachine.initializeInTime line 105
  20. def OAI.PerfectCompleteness.TupleIndexMachine.enumerationBudget line 116
  21. def OAI.PerfectCompleteness.TupleIndexMachine.enumerationInTime line 119
  22. def OAI.PerfectCompleteness.TupleIndexMachine.returnInTime line 131
  23. theorem OAI.PerfectCompleteness.TupleIndexMachine.mem_cleanupTapes line 139
  24. theorem OAI.PerfectCompleteness.TupleIndexMachine.cleanupTapes_length line 159
  25. theorem OAI.PerfectCompleteness.TupleIndexMachine.finalTapes_cleanup line 166
  26. theorem OAI.PerfectCompleteness.TupleIndexMachine.cleanup_lengthSum line 178
  27. theorem OAI.PerfectCompleteness.TupleIndexMachine.cleanup_budget line 187
  28. theorem OAI.PerfectCompleteness.TupleIndexMachine.cleanup_steps_le line 193
  29. def OAI.PerfectCompleteness.TupleIndexMachine.cleanupInTime line 199
  30. def OAI.PerfectCompleteness.TupleIndexMachine.totalBudget line 209
  31. def OAI.PerfectCompleteness.TupleIndexMachine.totalInTime line 212
  32. theorem OAI.PerfectCompleteness.TupleIndexMachine.initList_eq line 225
  33. theorem OAI.PerfectCompleteness.TupleIndexMachine.haltList_eq line 231
  34. def OAI.PerfectCompleteness.TupleIndexMachine.outputsInTime line 237
  35. def OAI.PerfectCompleteness.TupleIndexMachine.time line 246
  36. theorem OAI.PerfectCompleteness.TupleIndexMachine.time_eval line 251
  37. theorem OAI.PerfectCompleteness.TupleIndexMachine.totalBudget_mono line 255
  38. abbrev OAI.PerfectCompleteness.TupleIndexMachine.PositiveNat line 269
  39. def OAI.PerfectCompleteness.TupleIndexMachine.input line 271
  40. def OAI.PerfectCompleteness.TupleIndexMachine.tuples line 273
  41. def OAI.PerfectCompleteness.TupleIndexMachine.computation line 275
  42. theorem OAI.PerfectCompleteness.TupleIndexMachine.workAlphabet_finite line 296