OAI/Combinatorics/IndependentSets/PCP/Redirect.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.redirectLabel line 17
  2. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.redirectCfg line 21
  3. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.redirectStmt line 25
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.stepAux_redirect line 38
  5. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.chosen line 57
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.chosen_length line 61
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.mem_chosen line 63
  8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.Label line 66
  9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.cleanupLabel line 70
  10. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.resetLabel line 73
  11. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.cleanupEntry line 75
  12. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.completedProgram line 78
  13. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.completedMachine line 86
  14. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.embeddedCfg line 97
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.step_simulation line 102
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.embedded_init line 121
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.finalTapes_eq line 125
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.haltList_eq line 135
  19. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.cleanupExecution line 141
  20. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.outputsInTime line 174
  21. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.completedTime line 206
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFCleanup.completedTime_eval line 210