OAI/Computability/PerfectCompleteness/Reduction/FixedQueryCodec.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.FixedQueryCodec.LeftOutput line 16
  2. def OAI.PerfectCompleteness.FixedQueryCodec.leftCount line 19
  3. def OAI.PerfectCompleteness.FixedQueryCodec.leftEquiv line 22
  4. def OAI.PerfectCompleteness.FixedQueryCodec.leftEncode line 26
  5. theorem OAI.PerfectCompleteness.FixedQueryCodec.leftEncode_injective line 30
  6. abbrev OAI.PerfectCompleteness.FixedQueryCodec.TestIndex line 34
  7. instance OAI.PerfectCompleteness.FixedQueryCodec.testIndexFintype line 37
  8. abbrev OAI.PerfectCompleteness.FixedQueryCodec.RightOutput line 44
  9. instance OAI.PerfectCompleteness.FixedQueryCodec.rightOutputFintype line 48
  10. def OAI.PerfectCompleteness.FixedQueryCodec.project line 51
  11. abbrev OAI.PerfectCompleteness.FixedQueryCodec.TaggedRight line 55
  12. instance OAI.PerfectCompleteness.FixedQueryCodec.taggedRightFintype line 58
  13. def OAI.PerfectCompleteness.FixedQueryCodec.rightCount line 65
  14. def OAI.PerfectCompleteness.FixedQueryCodec.rightEquiv line 68
  15. def OAI.PerfectCompleteness.FixedQueryCodec.rightEncode line 72
  16. theorem OAI.PerfectCompleteness.FixedQueryCodec.rightEncode_injective line 76
  17. def OAI.PerfectCompleteness.FixedQueryCodec.outputMap line 80
  18. theorem OAI.PerfectCompleteness.FixedQueryCodec.outputMap_leftEncode line 84
  19. def OAI.PerfectCompleteness.FixedQueryCodec.decodedFiberEquiv line 91
  20. theorem OAI.PerfectCompleteness.FixedQueryCodec.outputMap_fiber_le_two line 98
  21. theorem OAI.PerfectCompleteness.FixedQueryCodec.left_key line 132
  22. theorem OAI.PerfectCompleteness.FixedQueryCodec.right_key line 139
  23. theorem OAI.PerfectCompleteness.FixedQueryCodec.right_kernel line 147
  24. def OAI.PerfectCompleteness.FixedQueryCodec.leftTable line 158
  25. theorem OAI.PerfectCompleteness.FixedQueryCodec.leftTable_key line 164
  26. theorem OAI.PerfectCompleteness.FixedQueryCodec.rightTable_key line 172
  27. def OAI.PerfectCompleteness.FixedQueryCodec.testIndex line 180
  28. def OAI.PerfectCompleteness.FixedQueryCodec.rawTestIndex line 184
  29. theorem OAI.PerfectCompleteness.FixedQueryCodec.testIndex_encodeRaw line 188
  30. def OAI.PerfectCompleteness.FixedQueryCodec.withProjection line 192
  31. def OAI.PerfectCompleteness.FixedQueryCodec.partialInput line 196
  32. theorem OAI.PerfectCompleteness.FixedQueryCodec.partialInput_encodeRaw line 201
  33. def OAI.PerfectCompleteness.FixedQueryCodec.rightInputOfPartial line 213
  34. def OAI.PerfectCompleteness.FixedQueryCodec.rightKeyInput line 217
  35. theorem OAI.PerfectCompleteness.FixedQueryCodec.rightKeyInput_encodeRaw line 222
  36. theorem OAI.PerfectCompleteness.FixedQueryCodec.partialInput_admissible line 233