OAI/Combinatorics/IndependentSets/PCP/RawInitialTables.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.unitOrder line 13
  2. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.slotOrder line 19
  3. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.binaryOrder line 28
  4. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.labelOrder line 37
  5. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.vertexOrder line 39
  6. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.eventOrder line 43
  7. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.dartOrder line 46
  8. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.raw64 line 50
  9. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table line 54
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table_vertices line 57
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table_darts line 60
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table_vertices_positive line 62
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table_darts_positive line 65
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.raw64_satisfiable_iff line 68
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table_semantics line 73
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.table_satisfiable_iff line 81
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.initial_rejection line 87
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialTables.initial_size line 93
  19. structure OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle line 103
  20. instance OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeVertex line 117
  21. instance OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.instFintypeDart line 118
  22. instance OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqVertex line 119
  23. instance OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.instDecidableEqDart line 120
  24. instance OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyDart line 121
  25. instance OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.instNonemptyVertex line 123
  26. def OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph line 127
  27. def OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.size line 139
  28. def OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.Satisfiable line 141
  29. def OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.rejectionCount line 143
  30. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.size_positive line 146
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.dartCard_le_size line 149
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_graph line 152
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_size line 156
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_satisfiable line 160
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_rejectionCount line 164