OAI/Computability/BinPacking/Computation/FinalCNFCleanup.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.redirectLabel line 16
  2. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.redirectCfg line 20
  3. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.redirectStmt line 24
  4. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.stepAux_redirect line 37
  5. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.chosen line 56
  6. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.chosen_length line 60
  7. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.mem_chosen line 62
  8. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.Label line 65
  9. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.cleanupLabel line 69
  10. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.resetLabel line 72
  11. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.cleanupEntry line 74
  12. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.completedProgram line 77
  13. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.completedMachine line 85
  14. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.embeddedCfg line 96
  15. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.step_simulation line 101
  16. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.embedded_init line 120
  17. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.finalTapes_eq line 124
  18. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.haltList_eq line 134
  19. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.cleanupExecution line 140
  20. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.outputsInTime line 171
  21. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.completedTime line 203
  22. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFCleanup.completedTime_eval line 207