OAI/Computability/PerfectCompleteness/Machines/NormalizedTargetMachine.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.NormalizedTargetMachine.Tape line 20
  2. def OAI.PerfectCompleteness.NormalizedTargetMachine.tapeEnumeration line 26
  3. def OAI.PerfectCompleteness.NormalizedTargetMachine.finalizerTape line 30
  4. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.finalizerTape_injective line 36
  5. abbrev OAI.PerfectCompleteness.NormalizedTargetMachine.Control line 54
  6. abbrev OAI.PerfectCompleteness.NormalizedTargetMachine.Ambient line 57
  7. abbrev OAI.PerfectCompleteness.NormalizedTargetMachine.Label line 60
  8. def OAI.PerfectCompleteness.NormalizedTargetMachine.initialControl line 62
  9. def OAI.PerfectCompleteness.NormalizedTargetMachine.initialAmbient line 65
  10. def OAI.PerfectCompleteness.NormalizedTargetMachine.initLabel line 74
  11. def OAI.PerfectCompleteness.NormalizedTargetMachine.driverLabel line 76
  12. def OAI.PerfectCompleteness.NormalizedTargetMachine.finalizerLabel line 78
  13. def OAI.PerfectCompleteness.NormalizedTargetMachine.program line 93
  14. def OAI.PerfectCompleteness.NormalizedTargetMachine.machine line 104
  15. def OAI.PerfectCompleteness.NormalizedTargetMachine.configuration line 118
  16. def OAI.PerfectCompleteness.NormalizedTargetMachine.returnInTime line 124
  17. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.header_body_eq_outputBits line 139
  18. def OAI.PerfectCompleteness.NormalizedTargetMachine.initializeInTime line 149
  19. def OAI.PerfectCompleteness.NormalizedTargetMachine.enumerateInTime line 158
  20. def OAI.PerfectCompleteness.NormalizedTargetMachine.finalizeBudget line 178
  21. def OAI.PerfectCompleteness.NormalizedTargetMachine.finalizeInTime line 182
  22. def OAI.PerfectCompleteness.NormalizedTargetMachine.totalBudget line 206
  23. def OAI.PerfectCompleteness.NormalizedTargetMachine.totalInTime line 210
  24. def OAI.PerfectCompleteness.NormalizedTargetMachine.time line 224
  25. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.time_eval line 232
  26. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.initList_eq line 237
  27. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.haltList_eq line 255
  28. def OAI.PerfectCompleteness.NormalizedTargetMachine.outputsInTime line 260
  29. def OAI.PerfectCompleteness.NormalizedTargetMachine.computation line 270
  30. def OAI.PerfectCompleteness.NormalizedTargetMachine.targetComputation line 287
  31. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.workAlphabet_finite line 304
  32. theorem OAI.PerfectCompleteness.NormalizedTargetMachine.finiteAlphabet line 308