OAI/Computability/BinPacking/Computation/MachineInitialHeaders.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.Alphabet line 14
  2. def OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixScan line 16
  3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.update_source line 27
  4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.update_scratch line 41
  5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.update_output line 52
  6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_true line 58
  7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_false line 69
  8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.replicate_append_cons line 79
  9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixScanTrace line 84
  10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixTrace line 121
  11. def OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixInTime line 171
  12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.prefixScan_pushBound line 190
  13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.literalTrace line 197
  14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.trace_trans line 210
  15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.headerTrace line 214
  16. def OAI.BinPackingGames.Foundations.Complexity.MachineInitialHeaders.headerInTime line 294