OAI/Computability/PerfectCompleteness/Reduction/NormalizedTargetInitialization.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.NormalizedTargetInitialization.Tape line 17
  2. abbrev OAI.PerfectCompleteness.NormalizedTargetInitialization.Alphabet line 18
  3. abbrev OAI.PerfectCompleteness.NormalizedTargetInitialization.State line 19
  4. def OAI.PerfectCompleteness.NormalizedTargetInitialization.clean line 21
  5. def OAI.PerfectCompleteness.NormalizedTargetInitialization.countTape line 25
  6. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.countTape_injective line 31
  7. def OAI.PerfectCompleteness.NormalizedTargetInitialization.currents line 35
  8. def OAI.PerfectCompleteness.NormalizedTargetInitialization.remaining line 36
  9. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.destinations_nodup line 38
  10. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.count_not_destination line 54
  11. inductive OAI.PerfectCompleteness.NormalizedTargetInitialization.Label line 58
  12. def OAI.PerfectCompleteness.NormalizedTargetInitialization.instruction line 66
  13. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.instruction_pushBound line 77
  14. def OAI.PerfectCompleteness.NormalizedTargetInitialization.inputTapes line 105
  15. def OAI.PerfectCompleteness.NormalizedTargetInitialization.seededTapes line 109
  16. def OAI.PerfectCompleteness.NormalizedTargetInitialization.countedTapes line 112
  17. def OAI.PerfectCompleteness.NormalizedTargetInitialization.zeroDigits line 116
  18. def OAI.PerfectCompleteness.NormalizedTargetInitialization.readyTapes line 120
  19. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.seeded_count line 124
  20. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.counted_count line 128
  21. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.initializedTapes_eq_ready line 133
  22. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.ready_table line 174
  23. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.ready_current line 178
  24. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.ready_remaining line 182
  25. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.ready_extra line 187
  26. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.ready_eq_native line 191
  27. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.seedStep line 224
  28. def OAI.PerfectCompleteness.NormalizedTargetInitialization.initializeExactInTime line 231
  29. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.count_length_le line 273
  30. def OAI.PerfectCompleteness.NormalizedTargetInitialization.initializeInTime line 279
  31. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.finite_tapes line 292
  32. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.finite_state line 293
  33. theorem OAI.PerfectCompleteness.NormalizedTargetInitialization.finite_alphabet line 294