OAI/Computability/BinPacking/Reductions/MachineTransfer.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Reduction.MachineTransfer.alphabet line 9
  2. def OAI.BinPackingGames.Reduction.MachineTransfer.loop line 15
  3. def OAI.BinPackingGames.Reduction.MachineTransfer.machine line 22
  4. def OAI.BinPackingGames.Reduction.MachineTransfer.tapeStacks line 34
  5. def OAI.BinPackingGames.Reduction.MachineTransfer.running line 39
  6. def OAI.BinPackingGames.Reduction.MachineTransfer.halted line 43
  7. theorem OAI.BinPackingGames.Reduction.MachineTransfer.update_input line 47
  8. theorem OAI.BinPackingGames.Reduction.MachineTransfer.update_output line 53
  9. theorem OAI.BinPackingGames.Reduction.MachineTransfer.step_empty line 58
  10. theorem OAI.BinPackingGames.Reduction.MachineTransfer.step_cons line 66
  11. def OAI.BinPackingGames.Reduction.MachineTransfer.next line 75
  12. theorem OAI.BinPackingGames.Reduction.MachineTransfer.transfer_steps line 78
  13. theorem OAI.BinPackingGames.Reduction.MachineTransfer.initList_eq line 95
  14. theorem OAI.BinPackingGames.Reduction.MachineTransfer.haltList_eq line 102
  15. theorem OAI.BinPackingGames.Reduction.MachineTransfer.transfer_init_steps line 109
  16. def OAI.BinPackingGames.Reduction.MachineTransfer.outputsInTime line 116
  17. theorem OAI.BinPackingGames.Reduction.MachineTransfer.outputsInTime_steps line 123
  18. def OAI.BinPackingGames.Reduction.MachineTransfer.computableInPolyTime line 126
  19. def OAI.BinPackingGames.Reduction.MachineTransfer.exitAt line 145
  20. def OAI.BinPackingGames.Reduction.MachineTransfer.loopAt line 150
  21. def OAI.BinPackingGames.Reduction.MachineTransfer.tapesAt line 157
  22. theorem OAI.BinPackingGames.Reduction.MachineTransfer.tapesAt_src line 161
  23. theorem OAI.BinPackingGames.Reduction.MachineTransfer.tapesAt_dst line 166
  24. theorem OAI.BinPackingGames.Reduction.MachineTransfer.tapesAt_other line 171
  25. theorem OAI.BinPackingGames.Reduction.MachineTransfer.tapesAt_self line 176
  26. theorem OAI.BinPackingGames.Reduction.MachineTransfer.update_tapesAt_src line 180
  27. theorem OAI.BinPackingGames.Reduction.MachineTransfer.update_tapesAt_dst line 194
  28. def OAI.BinPackingGames.Reduction.MachineTransfer.nextAt line 205
  29. theorem OAI.BinPackingGames.Reduction.MachineTransfer.stepAt_empty line 210
  30. theorem OAI.BinPackingGames.Reduction.MachineTransfer.stepAt_cons line 224
  31. theorem OAI.BinPackingGames.Reduction.MachineTransfer.transferAt_steps line 240
  32. theorem OAI.BinPackingGames.Reduction.MachineTransfer.transferAt_fromTapes line 264
  33. def OAI.BinPackingGames.Reduction.MachineTransfer.transferAtInTime line 277