OAI/Combinatorics/IndependentSets/PCP/Emitter.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.Command line 12
  2. inductive OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.Phase line 19
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.Alphabet line 24
  4. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.State line 25
  5. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.transition line 27
  6. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.payload line 28
  7. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandBits line 31
  8. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps line 40
  9. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandStatement line 49
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.output_encodeWord line 83
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandTrace line 97
  12. abbrev OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.Label line 174
  13. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.labelAt line 176
  14. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandAt line 179
  15. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.statement line 183
  16. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.program line 193
  17. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.machine line 198
  18. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits line 211
  19. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps line 217
  20. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes line 222
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_output line 225
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.resultTapes_other line 229
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.prefixTrace line 233
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.planTrace line 272
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.prefixSteps_le line 293
  26. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.planInTime line 312
  27. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.listCommands line 333
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.prefixBits_listCommands line 336
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.bits_listCommands line 348
  30. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands line 354
  31. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.affineValue line 358
  32. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.scaleBits line 361
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_bits line 371
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.affineCommands_length line 379
  35. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands line 383
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.bitCommands_bits line 385
  37. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.affineInTime line 394
  38. def OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.Command.mapAmbient line 418
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandBits_mapAmbient line 426
  40. theorem OAI.IndependentSetsGames.Foundations.PCP.AlphabetTable.Emitter.commandSteps_mapAmbient line 432