OAI/Computability/PerfectCompleteness/Foundations/SourceOddListsLemmas.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceOddLists.Occurrences line 16
  2. abbrev OAI.PerfectCompleteness.SourceOddLists.LeftLabels line 17
  3. abbrev OAI.PerfectCompleteness.SourceOddLists.RightLabels line 18
  4. def OAI.PerfectCompleteness.SourceOddLists.tupleLaw line 20
  5. def OAI.PerfectCompleteness.SourceOddLists.left line 23
  6. def OAI.PerfectCompleteness.SourceOddLists.right line 26
  7. def OAI.PerfectCompleteness.SourceOddLists.projection line 30
  8. def OAI.PerfectCompleteness.SourceOddLists.base line 34
  9. theorem OAI.PerfectCompleteness.SourceOddLists.base_eq_repetition line 39
  10. theorem OAI.PerfectCompleteness.SourceOddLists.base_endpointDetermined line 54
  11. def OAI.PerfectCompleteness.SourceOddLists.game line 63
  12. def OAI.PerfectCompleteness.SourceOddLists.tolerance line 69
  13. theorem OAI.PerfectCompleteness.SourceOddLists.tolerance_positive line 71
  14. def OAI.PerfectCompleteness.SourceOddLists.repetitionLength line 76
  15. theorem OAI.PerfectCompleteness.SourceOddLists.repetitionLength_positive line 80
  16. theorem OAI.PerfectCompleteness.SourceOddLists.amplified_base_gap line 85
  17. def OAI.PerfectCompleteness.SourceOddLists.alphabetLog line 105
  18. theorem OAI.PerfectCompleteness.SourceOddLists.exists_alphabet_budget line 110
  19. theorem OAI.PerfectCompleteness.SourceOddLists.value_le_half line 117
  20. theorem OAI.PerfectCompleteness.SourceOddLists.repetition_halfRate line 125
  21. def OAI.PerfectCompleteness.SourceAnswerEquiv.clauseAnswerEquiv line 148
  22. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.clauseAnswerEquiv_symm_val line 160
  23. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.clauseAnswerEquiv_decode line 163
  24. def OAI.PerfectCompleteness.SourceAnswerEquiv.leftSlots line 168
  25. def OAI.PerfectCompleteness.SourceAnswerEquiv.rightSlots line 172
  26. abbrev OAI.PerfectCompleteness.SourceAnswerEquiv.LeftDomain line 176
  27. abbrev OAI.PerfectCompleteness.SourceAnswerEquiv.RightDomain line 179
  28. instance OAI.PerfectCompleteness.SourceAnswerEquiv.rightDomainDecidableEq line 182
  29. def OAI.PerfectCompleteness.SourceAnswerEquiv.leftEquiv line 186
  30. def OAI.PerfectCompleteness.SourceAnswerEquiv.rightEquiv line 197
  31. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.leftEquiv_apply line 201
  32. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.leftEquiv_symm_apply line 205
  33. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.rightEquiv_apply line 210
  34. def OAI.PerfectCompleteness.SourceAnswerEquiv.slotProjection line 214
  35. def OAI.PerfectCompleteness.SourceAnswerEquiv.actualProjection line 220
  36. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.actualProjection_apply line 226
  37. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.projection_decode line 231
  38. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.projection_encode line 237
  39. def OAI.PerfectCompleteness.SourceAnswerEquiv.encodeOddList line 246
  40. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.encodeOddList_projection line 252
  41. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.encodeOddList_accepted line 290
  42. def OAI.PerfectCompleteness.SourceAnswerEquiv.leftTreeSlots line 302
  43. def OAI.PerfectCompleteness.SourceAnswerEquiv.rightTreeSlots line 307
  44. def OAI.PerfectCompleteness.SourceAnswerEquiv.leftLeafEquiv line 312
  45. def OAI.PerfectCompleteness.SourceAnswerEquiv.rightLeafEquiv line 319
  46. theorem OAI.PerfectCompleteness.SourceAnswerEquiv.leaf_projection_encode line 326