OAI/Computability/BinPacking/Reductions/MachineTransducer.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Reduction.MachineTransducer.tapeStacks line 13
  2. theorem OAI.BinPackingGames.Reduction.MachineTransducer.update_input line 16
  3. theorem OAI.BinPackingGames.Reduction.MachineTransducer.update_output line 21
  4. def OAI.BinPackingGames.Reduction.MachineTransducer.output line 28
  5. def OAI.BinPackingGames.Reduction.MachineTransducer.loop line 34
  6. def OAI.BinPackingGames.Reduction.MachineTransducer.program line 41
  7. def OAI.BinPackingGames.Reduction.MachineTransducer.machine line 49
  8. def OAI.BinPackingGames.Reduction.MachineTransducer.maxEmission line 61
  9. theorem OAI.BinPackingGames.Reduction.MachineTransducer.emission_le line 64
  10. theorem OAI.BinPackingGames.Reduction.MachineTransducer.statementPushBound_le line 69
  11. theorem OAI.BinPackingGames.Reduction.MachineTransducer.programPushBound_le line 78
  12. def OAI.BinPackingGames.Reduction.MachineTransducer.running line 89
  13. def OAI.BinPackingGames.Reduction.MachineTransducer.emitting line 94
  14. def OAI.BinPackingGames.Reduction.MachineTransducer.halted line 99
  15. theorem OAI.BinPackingGames.Reduction.MachineTransducer.step_empty line 103
  16. theorem OAI.BinPackingGames.Reduction.MachineTransducer.step_cons line 114
  17. theorem OAI.BinPackingGames.Reduction.MachineTransducer.step_emit line 126
  18. def OAI.BinPackingGames.Reduction.MachineTransducer.next line 145
  19. theorem OAI.BinPackingGames.Reduction.MachineTransducer.two_steps_cons line 150
  20. theorem OAI.BinPackingGames.Reduction.MachineTransducer.transduce_steps line 163
  21. theorem OAI.BinPackingGames.Reduction.MachineTransducer.initList_eq line 180
  22. theorem OAI.BinPackingGames.Reduction.MachineTransducer.haltList_eq line 189
  23. theorem OAI.BinPackingGames.Reduction.MachineTransducer.transduce_init_steps line 196
  24. def OAI.BinPackingGames.Reduction.MachineTransducer.outputsInTime line 204
  25. theorem OAI.BinPackingGames.Reduction.MachineTransducer.outputsInTime_steps line 212
  26. def OAI.BinPackingGames.Reduction.MachineTransducer.reversedComputableInPolyTime line 216
  27. def OAI.BinPackingGames.Reduction.MachineTransducer.computableInPolyTime line 236