OAI/Computability/UniqueGames/PCP/RawInitialMachineLoopData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The exact input and output streams at successive clause-loop iterations. These tape invariants use the actual word codecs and clause occurrence order.

  1. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseInput line 16
  2. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseInput_nil line 19
  3. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseInput_cons line 21
  4. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseOutput line 25
  5. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.mapIdx_ofFn line 29
  6. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_nil line 35
  7. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_cons line 37
  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_numbered line 44
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.tableWords_decomposition line 54
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.loopTapes line 61
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.startTapes_eq line 69
  12. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.decrement_counter line 75
  13. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RawInitialMachineLoopData.increment_index line 81