OAI/Computability/VertexCover/PCP/PortTables.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.PortTables.Label line 13
  2. def OAI.UniqueGames.Foundations.PCP.PortTables.rowIndex line 15
  3. theorem OAI.UniqueGames.Foundations.PCP.PortTables.rowIndex_val line 18
  4. structure OAI.UniqueGames.Foundations.PCP.PortTables.Table line 21
  5. def OAI.UniqueGames.Foundations.PCP.PortTables.rotation line 32
  6. def OAI.UniqueGames.Foundations.PCP.PortTables.accepts line 35
  7. theorem OAI.UniqueGames.Foundations.PCP.PortTables.rowIndex_rotation line 38
  8. theorem OAI.UniqueGames.Foundations.PCP.PortTables.rotation_involutive line 42
  9. theorem OAI.UniqueGames.Foundations.PCP.PortTables.accepts_rotation line 48
  10. def OAI.UniqueGames.Foundations.PCP.PortTables.portGraph line 52
  11. theorem OAI.UniqueGames.Foundations.PCP.PortTables.portGraph_rot line 60
  12. def OAI.UniqueGames.Foundations.PCP.PortTables.baseGraph line 63
  13. theorem OAI.UniqueGames.Foundations.PCP.PortTables.baseGraph_reverse line 70
  14. theorem OAI.UniqueGames.Foundations.PCP.PortTables.baseGraph_tail line 73
  15. theorem OAI.UniqueGames.Foundations.PCP.PortTables.baseGraph_head line 76
  16. theorem OAI.UniqueGames.Foundations.PCP.PortTables.baseGraph_accepts line 79
  17. def OAI.UniqueGames.Foundations.PCP.PortTables.ofPortGraph line 82
  18. theorem OAI.UniqueGames.Foundations.PCP.PortTables.rotation_ofPortGraph line 99
  19. theorem OAI.UniqueGames.Foundations.PCP.PortTables.accepts_ofPortGraph line 106
  20. def OAI.UniqueGames.Foundations.PCP.PortTables.flatRows line 114
  21. theorem OAI.UniqueGames.Foundations.PCP.PortTables.reverseAt_flatRows line 118
  22. theorem OAI.UniqueGames.Foundations.PCP.PortTables.acceptsAt_flatRows line 122
  23. theorem OAI.UniqueGames.Foundations.PCP.PortTables.flatRows_valid line 126
  24. def OAI.UniqueGames.Foundations.PCP.PortTables.graphTable line 133
  25. def OAI.UniqueGames.Foundations.PCP.PortTables.tableWords line 136
  26. def OAI.UniqueGames.Foundations.PCP.PortTables.tableBits line 138
  27. abbrev OAI.UniqueGames.Foundations.PCP.PortTables.Input line 140
  28. def OAI.UniqueGames.Foundations.PCP.PortTables.inputBits line 142
  29. theorem OAI.UniqueGames.Foundations.PCP.PortTables.tableWords_eq line 144
  30. theorem OAI.UniqueGames.Foundations.PCP.PortTables.tableWords_length line 147
  31. theorem OAI.UniqueGames.Foundations.PCP.PortTables.vertices_le_tableBits_length line 151