OAI/Computability/BinPacking/Reductions/MachineReverse.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Reduction.MachineReverse.loop line 9
  2. def OAI.BinPackingGames.Reduction.MachineReverse.machine line 15
  3. def OAI.BinPackingGames.Reduction.MachineReverse.tapeStacks line 26
  4. def OAI.BinPackingGames.Reduction.MachineReverse.running line 29
  5. def OAI.BinPackingGames.Reduction.MachineReverse.halted line 32
  6. theorem OAI.BinPackingGames.Reduction.MachineReverse.update_input line 35
  7. theorem OAI.BinPackingGames.Reduction.MachineReverse.update_output line 40
  8. theorem OAI.BinPackingGames.Reduction.MachineReverse.step_empty line 45
  9. theorem OAI.BinPackingGames.Reduction.MachineReverse.step_cons line 52
  10. def OAI.BinPackingGames.Reduction.MachineReverse.next line 60
  11. theorem OAI.BinPackingGames.Reduction.MachineReverse.reverse_steps line 63
  12. theorem OAI.BinPackingGames.Reduction.MachineReverse.initList_eq line 77
  13. theorem OAI.BinPackingGames.Reduction.MachineReverse.haltList_eq line 84
  14. theorem OAI.BinPackingGames.Reduction.MachineReverse.reverse_init_steps line 88
  15. def OAI.BinPackingGames.Reduction.MachineReverse.outputsInTime line 94
  16. theorem OAI.BinPackingGames.Reduction.MachineReverse.outputsInTime_steps line 100
  17. def OAI.BinPackingGames.Reduction.MachineReverse.computableInPolyTime line 103