OAI/Combinatorics/IndependentSets/Encoding/Concrete.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.clauseAnswerEncoding line 16
  2. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.slotEncoding line 18
  3. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.iEncoding line 26
  4. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.jEncoding line 27
  5. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.variableEncoding line 28
  6. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.clauseEncoding line 30
  7. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.slotContextEncoding line 32
  8. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.proofEncoding line 35
  9. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.nBits line 39
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.nBits_eq line 41
  11. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.dummyIndex line 45
  12. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.leftAnchor line 48
  13. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.rightAnchor line 50
  14. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.rightAnchor_none_iff line 53
  15. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.halfTableKeyAssignment line 57
  16. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.extendHalfTables line 69
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_left line 76
  18. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.extendHalfTables_right line 87
  19. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.emptyAddress line 104
  20. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.contextEquation line 109
  21. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.leftResponse line 118
  22. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.rightResponse line 122
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.contextEquation_satisfied line 129
  24. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.testTapeEncoding line 146
  25. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.SourceIndex line 150
  26. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceIndexEncoding line 153
  27. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceEquation line 156
  28. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.rawSourceList line 160
  29. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.rawSourceList_length line 163
  30. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.rawSourceList_acceptance line 170
  31. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation line 193
  32. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceList line 196
  33. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceList_empty line 199
  34. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceList_nonempty line 202
  35. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceList_length_le_raw_add_one line 208
  36. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceList_ne_nil line 217
  37. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.sourceInput line 228
  38. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.emptyFormulaEquation_satisfied line 232