OAI/Computability/PerfectCompleteness/Reduction/NormalizedTarget.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.NormalizedTarget.inputBits line 20
  2. theorem OAI.PerfectCompleteness.NormalizedTarget.inputBits_eq line 23
  3. theorem OAI.PerfectCompleteness.NormalizedTarget.decode_inputBits line 26
  4. theorem OAI.PerfectCompleteness.NormalizedTarget.inputBits_injective line 30
  5. abbrev OAI.PerfectCompleteness.NormalizedTarget.SourceTuple line 33
  6. def OAI.PerfectCompleteness.NormalizedTarget.tupleQuestion line 37
  7. theorem OAI.PerfectCompleteness.NormalizedTarget.tupleQuestion_digits line 42
  8. def OAI.PerfectCompleteness.NormalizedTarget.sourceShapes line 47
  9. def OAI.PerfectCompleteness.NormalizedTarget.parsedVariableIDs line 53
  10. theorem OAI.PerfectCompleteness.NormalizedTarget.parsedVariableIDs_eq line 58
  11. theorem OAI.PerfectCompleteness.NormalizedTarget.sourceSigns_eq line 64
  12. theorem OAI.PerfectCompleteness.NormalizedTarget.signTuple_eq line 72
  13. theorem OAI.PerfectCompleteness.NormalizedTarget.numberedSlots_eq line 79
  14. theorem OAI.PerfectCompleteness.NormalizedTarget.sourceTable_eq line 93
  15. theorem OAI.PerfectCompleteness.NormalizedTarget.digit_counter line 98
  16. theorem OAI.PerfectCompleteness.NormalizedTarget.variable_counter line 105
  17. def OAI.PerfectCompleteness.NormalizedTarget.construct line 117
  18. def OAI.PerfectCompleteness.NormalizedTarget.outputBits line 121
  19. theorem OAI.PerfectCompleteness.NormalizedTarget.construct_eq line 124
  20. theorem OAI.PerfectCompleteness.NormalizedTarget.edge_count line 129
  21. theorem OAI.PerfectCompleteness.NormalizedTarget.value_le line 156
  22. theorem OAI.PerfectCompleteness.NormalizedTarget.perfectlyComplete line 163
  23. theorem OAI.PerfectCompleteness.NormalizedTarget.outputBits_length_le line 172