OAI/Combinatorics/IndependentSets/Machines/RawInitialMachineLoopData.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput line 10
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_nil line 13
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseInput_cons line 15
  4. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput line 19
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.mapIdx_ofFn line 23
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_nil line 29
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_cons line 31
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.clauseOutput_numbered line 38
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.tableWords_decomposition line 48
  10. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.loopTapes line 55
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.startTapes_eq line 63
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.decrement_counter line 69
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachineLoopData.increment_index line 75
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_scratch line 86
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.copySource_ne_reversed line 89
  16. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.copyInTime line 92
  17. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.relationInTime line 107
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.bitWord_head line 120
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.loadSigns_step line 124
  20. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.loadSignsInTime line 133
  21. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.cleanupFieldInTime line 144
  22. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialMachinePhases.cleanupFinalInTime line 152