OAI/Computability/UniqueGames/Machines/MachineExpanderFamilyTapes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Static, pointwise Boolean presentation of the actual family tape alphabet. Every conversion below is an identity on symbols and has no machine runtime.

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolWord line 14
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolWord line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes line 24
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolTapes line 27
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolWord_boolWord line 30
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.boolWord_toBoolWord line 36
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBool_fromBool line 42
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.fromBool_toBool line 47
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.transport_tapes_apply line 52
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_eq_transport line 59
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_eq_transport line 67
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_update line 75
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_update line 84
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.configuration_fromBool line 94
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.configuration_toBool line 100