OAI/Computability/BinPacking/Computation/MachineRegularTableRuntime.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.joinTrace line 12

    Also declared: OAI/Computability/BinPacking/Computation/MachineRegularTable.lean:1205 (same declaration text).

  2. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.normalizeEmptyAppend line 16
  3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerStartTrace line 20
  4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerOldTrace line 32
  5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.beforeCleanupTrace line 48
  6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleanupFinalTrace line 64
  7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.fullTrace line 72
  8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_output line 80
  9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.input_stacks_eq line 93
  10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.initial_cfg_eq line 113
  11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.trace line 121
  12. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopPolynomial line 150
  13. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopPolynomial line 155
  14. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.timePolynomial line 160
  15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_prefix_le line 166
  16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_le line 188
  17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_prefix_le line 196
  18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_le line 220
  19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.totalTime_le line 229
  20. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.machineInTime line 245
  21. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.rawProgram line 264
  22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.sourceMachine_eq line 272
  23. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.cleanupTapes line 276
  24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.cleanup_complete line 279
  25. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.terminalRun line 283
  26. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime line 301
  27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTableRuntime.finite_alphabet line 309