OAI/Combinatorics/IndependentSets/PCP/EmitRows.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.Context line 13
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand line 14
  3. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits line 16
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.vector_list_ofFn line 21
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.bitValues_ofFn line 26
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits_values line 35
  7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands line 43
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.rowContext line 52
  9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues line 56
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.encodedRow line 62
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_bits line 68
  12. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands line 99
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockWords line 104
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.tableWords_eq_blocks line 111
  15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands line 122
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_bits line 128
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_length line 142
  18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.headerInTime line 146
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.encodeWords_flatMap line 171
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_bits line 177
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_length_le line 184
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.flatMap_length_le line 192
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_length_le line 203
  24. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTime line 214
  25. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn line 243
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn_bits line 247
  27. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTimeAmbient line 256