OAI/Combinatorics/IndependentSets/PCP/Addresses.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.Terms line 12
  2. structure OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.Field line 14
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.values line 18
  4. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.eval line 20
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound line 23
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound_pos line 26
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.tapeCount_lt_bound line 30
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.pairTapeCount_lt_bound line 34
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.localCount_lt_bound line 38
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.local_add_pair_lt_bound line 42
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.twelve_local_lt_bound line 46
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.zeroOffset line 50
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.eventOffset line 52
  14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryOffset line 56
  15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.reverseOffset line 62
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices line 72
  17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts line 75
  18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField line 78
  19. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.vertexQueryTerms line 82
  20. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.edgeQueryTerms line 85
  21. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms line 88
  22. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField line 92
  23. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField line 95
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_eval line 99
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_eval line 105
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_eval line 110
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField_eval line 117
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_eval line 133
  29. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms line 143
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_query line 147
  31. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.queryEventOffset line 155
  32. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent line 159
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eq_rawQueryField line 163
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval line 170
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval_verifier line 179
  36. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms line 188
  37. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.dartTailOffset line 192
  38. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail line 196
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail_eval line 200
  40. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.CoefficientsBounded line 212
  41. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_coefficients line 215
  42. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_coefficients line 222
  43. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_coefficients line 228
  44. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_coefficients line 235
  45. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_coefficients line 253
  46. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_coefficients line 257
  47. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_length_le line 265
  48. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_length_le line 271
  49. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_coefficients line 275
  50. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_length_le line 282
  51. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Addresses.offset_lt line 289