OAI/Computability/PerfectCompleteness/Machines/TargetFinalizeMachine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.TargetFinalizeMachine.Alphabet line 16
  2. abbrev OAI.PerfectCompleteness.TargetFinalizeMachine.State line 17
  3. def OAI.PerfectCompleteness.TargetFinalizeMachine.headerTape line 19
  4. theorem OAI.PerfectCompleteness.TargetFinalizeMachine.headerTape_injective line 25
  5. abbrev OAI.PerfectCompleteness.TargetFinalizeMachine.WorkLabel line 31
  6. inductive OAI.PerfectCompleteness.TargetFinalizeMachine.Label line 34
  7. abbrev OAI.PerfectCompleteness.TargetFinalizeMachine.Labels line 41
  8. def OAI.PerfectCompleteness.TargetFinalizeMachine.instruction line 44
  9. def OAI.PerfectCompleteness.TargetFinalizeMachine.bodyTapes line 58
  10. def OAI.PerfectCompleteness.TargetFinalizeMachine.headerTapes line 61
  11. def OAI.PerfectCompleteness.TargetFinalizeMachine.budget line 66
  12. def OAI.PerfectCompleteness.TargetFinalizeMachine.finalizeInTime line 73