OAI/Computability/VertexCover/Reduction/SourceEncoding.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Reduction.SourceEncoding.Input line 43
  2. abbrev OAI.UniqueGames.Reduction.SourceEncoding.Table line 48
  3. def OAI.UniqueGames.Reduction.SourceEncoding.equationWords line 50
  4. def OAI.UniqueGames.Reduction.SourceEncoding.inputWords line 53
  5. def OAI.UniqueGames.Reduction.SourceEncoding.inputBits line 56
  6. def OAI.UniqueGames.Reduction.SourceEncoding.parseEquation line 58
  7. theorem OAI.UniqueGames.Reduction.SourceEncoding.parseEquation_encoded line 74
  8. def OAI.UniqueGames.Reduction.SourceEncoding.parseEquations line 81
  9. theorem OAI.UniqueGames.Reduction.SourceEncoding.parseEquations_encoded line 89
  10. def OAI.UniqueGames.Reduction.SourceEncoding.decodeInputWords line 98
  11. theorem OAI.UniqueGames.Reduction.SourceEncoding.decodeInputWords_encoded line 108
  12. def OAI.UniqueGames.Reduction.SourceEncoding.decodeInputBits line 117
  13. theorem OAI.UniqueGames.Reduction.SourceEncoding.decodeInputBits_encoded line 120
  14. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputWords_injective line 124
  15. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputBits_injective line 129
  16. theorem OAI.UniqueGames.Reduction.SourceEncoding.equationWords_length line 134
  17. theorem OAI.UniqueGames.Reduction.SourceEncoding.equationsWords_length line 137
  18. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputWords_length line 146
  19. theorem OAI.UniqueGames.Reduction.SourceEncoding.equationBits_length_le line 151
  20. theorem OAI.UniqueGames.Reduction.SourceEncoding.equationsBits_length_le line 158
  21. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputBits_length line 169
  22. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputBits_length_le line 176
  23. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputBits_length_ge_variables line 182
  24. theorem OAI.UniqueGames.Reduction.SourceEncoding.inputBits_length_ge_equations line 185