OAI/Computability/BinPacking/CookLevin/InitializationMachine.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.Tape line 11
  2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.Tape.enumList line 16
  3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.Tape.enumList_getElem?_ctorIdx_eq line 19
  4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.Tape.enumList_nodup line 23
  5. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.(instance at line 25) line 25
  6. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.Label line 29
  7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.Alphabet line 34
  8. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.State line 35
  9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.initialState line 37
  10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.program line 39
  11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.machine line 51
  12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes line 62
  13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes_current line 71
  14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes_reversed line 74
  15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.update_reversed line 77
  16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.push_current line 84
  17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.counterTapes_remaining line 90
  18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.counterTapes_threshold line 97
  19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.chain line 104
  20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.inputTagStep line 108
  21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.identity_output line 118
  22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.indexTrace line 125
  23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.thresholdStep line 138
  24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.resultStep line 153
  25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.termTokens line 162
  26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.termTokens_bits line 165
  27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.bodySteps line 171
  28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.bodyTrace line 173
  29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.guardStep_succ line 206
  30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.guardStep_zero line 213
  31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tokens_append_bits line 220
  32. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.selectorSteps line 224
  33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.selectorTrace line 228
  34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.selectorSteps_le line 256
  35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.selectorInTime line 270
  36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes_rawInput line 280
  37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes_witnessBound line 283
  38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes_capacity line 286
  39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationMachine.tapes_closure line 289