OAI/Computability/PerfectCompleteness/Reduction/CompletionLemmas.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.Completion.fiberEquivTwo line 15
  2. theorem OAI.PerfectCompleteness.Completion.exists_slot_embedding line 26
  3. theorem OAI.PerfectCompleteness.Completion.exists_exact_two_completion line 41
  4. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.Mode line 76
  5. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.Tape line 77
  6. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.Label line 78
  7. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.CleanupLabel line 80
  8. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.State line 81
  9. abbrev OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.Alphabet line 82
  10. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.nativeProgram line 86
  11. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.instruction line 90
  12. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.entry line 95
  13. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.tapes line 99
  14. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.tapes_eq_base line 104
  15. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.cleanupNativeProgram line 118
  16. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.cleanupInstruction line 122
  17. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.cleanupEntry line 127
  18. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.familyTrace line 132
  19. def OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.familyInTime line 151
  20. theorem OAI.PerfectCompleteness.FixedUnaryRepresentationPlacement.cleanupTrace line 173
  21. def OAI.PerfectCompleteness.InitialParameters.epsilon line 202
  22. def OAI.PerfectCompleteness.InitialParameters.simultaneous line 203
  23. def OAI.PerfectCompleteness.InitialParameters.useful line 204
  24. def OAI.PerfectCompleteness.InitialParameters.inverse line 205
  25. theorem OAI.PerfectCompleteness.InitialParameters.epsilon_pos line 207
  26. theorem OAI.PerfectCompleteness.InitialParameters.simultaneous_pos line 212
  27. theorem OAI.PerfectCompleteness.InitialParameters.useful_pos line 217
  28. theorem OAI.PerfectCompleteness.InitialParameters.inverse_pos line 222
  29. theorem OAI.PerfectCompleteness.InitialParameters.epsilon_lt_one line 227
  30. theorem OAI.PerfectCompleteness.InitialParameters.exists_initial line 232