OAI/Computability/PerfectCompleteness/Machines/CanonicalEndpointMachine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CanonicalEndpointMachine.Alphabet line 20
  2. abbrev OAI.PerfectCompleteness.CanonicalEndpointMachine.State line 21
  3. abbrev OAI.PerfectCompleteness.CanonicalEndpointMachine.clean line 22
  4. inductive OAI.PerfectCompleteness.CanonicalEndpointMachine.Label line 24
  5. def OAI.PerfectCompleteness.CanonicalEndpointMachine.main line 31
  6. def OAI.PerfectCompleteness.CanonicalEndpointMachine.instruction line 33
  7. def OAI.PerfectCompleteness.CanonicalEndpointMachine.finalTapes line 46
  8. def OAI.PerfectCompleteness.CanonicalEndpointMachine.budget line 52
  9. def OAI.PerfectCompleteness.CanonicalEndpointMachine.endpointInTime line 60
  10. theorem OAI.PerfectCompleteness.CanonicalEndpointMachine.finalTapes_frame line 172
  11. theorem OAI.PerfectCompleteness.CanonicalEndpointMachine.finalTapes_sources line 179
  12. theorem OAI.PerfectCompleteness.CanonicalEndpointMachine.label_finite line 188
  13. theorem OAI.PerfectCompleteness.CanonicalEndpointMachine.state_finite line 190
  14. theorem OAI.PerfectCompleteness.CanonicalEndpointMachine.workAlphabet_finite line 193