OAI/Computability/BinPacking/Computation/MachineExpanderRowEmit.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.emitSteps line 10
  2. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.affinePlan_bits line 12
  3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.affinePlan_steps line 23
  4. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.emittedWord line 30
  5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.emittedWord_target line 34
  6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.emittedWord_other line 39
  7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.program_firstEmit line 47
  8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.program_secondEmit line 53
  9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.program_outputEmit line 59
  10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstEmitTraceAt line 69
  11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondEmitTraceAt line 100
  12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.outputEmitTraceAt line 131
  13. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTimeAt line 162
  14. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTimeAt line 180
  15. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTimeAt line 198
  16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstEmitTrace line 218
  17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondEmitTrace line 230
  18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.outputEmitTrace line 242
  19. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstEmitInTime line 254
  20. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondEmitInTime line 266
  21. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.outputEmitInTime line 278