OAI/Computability/PerfectCompleteness/Machines/BinaryNameSearch.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.BinaryNameSearch.Token line 15
  2. def OAI.PerfectCompleteness.BinaryNameSearch.tokenBits line 17
  3. def OAI.PerfectCompleteness.BinaryNameSearch.stream line 20
  4. def OAI.PerfectCompleteness.BinaryNameSearch.payloads line 24
  5. def OAI.PerfectCompleteness.BinaryNameSearch.afterMatch line 26
  6. def OAI.PerfectCompleteness.BinaryNameSearch.steps line 30
  7. def OAI.PerfectCompleteness.BinaryNameSearch.payloadSize line 36
  8. theorem OAI.PerfectCompleteness.BinaryNameSearch.stream_nil line 38
  9. theorem OAI.PerfectCompleteness.BinaryNameSearch.stream_cons line 40
  10. theorem OAI.PerfectCompleteness.BinaryNameSearch.payloads_nil line 43
  11. theorem OAI.PerfectCompleteness.BinaryNameSearch.payloads_cons line 45
  12. theorem OAI.PerfectCompleteness.BinaryNameSearch.payloadSize_nil line 48
  13. theorem OAI.PerfectCompleteness.BinaryNameSearch.payloadSize_cons line 50
  14. theorem OAI.PerfectCompleteness.BinaryNameSearch.stream_length line 53
  15. theorem OAI.PerfectCompleteness.BinaryNameSearch.steps_le line 62
  16. theorem OAI.PerfectCompleteness.BinaryNameSearch.steps_le_stream line 71
  17. abbrev OAI.PerfectCompleteness.BinaryNameSearch.Alphabet line 81
  18. abbrev OAI.PerfectCompleteness.BinaryNameSearch.State line 82
  19. abbrev OAI.PerfectCompleteness.BinaryNameSearch.clean line 84
  20. inductive OAI.PerfectCompleteness.BinaryNameSearch.Label line 86
  21. def OAI.PerfectCompleteness.BinaryNameSearch.compareTapes line 92
  22. theorem OAI.PerfectCompleteness.BinaryNameSearch.compareTapes_injective line 95
  23. def OAI.PerfectCompleteness.BinaryNameSearch.exitAt line 101
  24. def OAI.PerfectCompleteness.BinaryNameSearch.finish line 106
  25. def OAI.PerfectCompleteness.BinaryNameSearch.instruction line 109
  26. theorem OAI.PerfectCompleteness.BinaryNameSearch.stepAux_finish line 120
  27. theorem OAI.PerfectCompleteness.BinaryNameSearch.update_source line 124
  28. theorem OAI.PerfectCompleteness.BinaryNameSearch.update_counter line 135
  29. theorem OAI.PerfectCompleteness.BinaryNameSearch.joinTrace line 141
  30. theorem OAI.PerfectCompleteness.BinaryNameSearch.signStep line 154
  31. theorem OAI.PerfectCompleteness.BinaryNameSearch.emptyStep line 165
  32. theorem OAI.PerfectCompleteness.BinaryNameSearch.incrementStep line 176
  33. theorem OAI.PerfectCompleteness.BinaryNameSearch.tokenTrace line 186
  34. theorem OAI.PerfectCompleteness.BinaryNameSearch.searchTrace line 232
  35. def OAI.PerfectCompleteness.BinaryNameSearch.searchInTime line 283
  36. def OAI.PerfectCompleteness.BinaryNameSearch.machine line 304
  37. theorem OAI.PerfectCompleteness.BinaryNameSearch.machine_finiteAlphabet line 317