OAI/Computability/BinPacking/PCP/SourceEncoding.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGames.Reduction.SourceEncoding.Input line 10
  2. abbrev OAI.BinPackingGames.Reduction.SourceEncoding.Table line 15
  3. def OAI.BinPackingGames.Reduction.SourceEncoding.equationWords line 17
  4. def OAI.BinPackingGames.Reduction.SourceEncoding.inputWords line 20
  5. def OAI.BinPackingGames.Reduction.SourceEncoding.inputBits line 23
  6. def OAI.BinPackingGames.Reduction.SourceEncoding.parseEquation line 25
  7. theorem OAI.BinPackingGames.Reduction.SourceEncoding.parseEquation_encoded line 41
  8. def OAI.BinPackingGames.Reduction.SourceEncoding.parseEquations line 48
  9. theorem OAI.BinPackingGames.Reduction.SourceEncoding.parseEquations_encoded line 56
  10. def OAI.BinPackingGames.Reduction.SourceEncoding.decodeInputWords line 65
  11. theorem OAI.BinPackingGames.Reduction.SourceEncoding.decodeInputWords_encoded line 75
  12. def OAI.BinPackingGames.Reduction.SourceEncoding.decodeInputBits line 84
  13. theorem OAI.BinPackingGames.Reduction.SourceEncoding.decodeInputBits_encoded line 87
  14. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputWords_injective line 91
  15. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputBits_injective line 96
  16. theorem OAI.BinPackingGames.Reduction.SourceEncoding.equationWords_length line 101
  17. theorem OAI.BinPackingGames.Reduction.SourceEncoding.equationsWords_length line 104
  18. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputWords_length line 113
  19. theorem OAI.BinPackingGames.Reduction.SourceEncoding.equationBits_length_le line 118
  20. theorem OAI.BinPackingGames.Reduction.SourceEncoding.equationsBits_length_le line 125
  21. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputBits_length line 136
  22. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputBits_length_le line 143
  23. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputBits_length_ge_variables line 149
  24. theorem OAI.BinPackingGames.Reduction.SourceEncoding.inputBits_length_ge_equations line 152