OAI/Computability/UniqueGames/Machines/MachineProductProgram.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.Extra line 19
  2. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.Tape line 20
  3. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.State line 21
  4. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.auxiliary line 23
  5. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.constantDigit line 24
  6. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.accumulator line 25
  7. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.output line 26
  8. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.rowRole line 28
  9. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.decodeRow line 38
  10. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.decodeRow_role line 49
  11. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.rowSlots line 58
  12. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.powerRole line 65
  13. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.powerRole_injective line 74
  14. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.powerSlots line 86
  15. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.initRole line 89
  16. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.initRole_injective line 95
  17. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.seedCommands line 99
  18. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.clearKeys line 102
  19. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.mem_clearKeys line 105
  20. inductive OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.Label line 111
  21. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.headerDestination line 126
  22. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.rowMain line 131
  23. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.nextCheck line 134
  24. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.resetAt line 136
  25. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.headerNext line 138
  26. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.program line 141
  27. def OAI.UniqueGamesTheorem.Explicit.MachineProductProgram.machine line 167