OAI/Computability/BinPacking/Machines/PackingVertexUpdate.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.PackingMachineLayout.Reg line 18
  2. abbrev OAI.BinPackingGap.PackingMachineLayout.Tape line 21
  3. instance OAI.BinPackingGap.PackingMachineLayout.regDecidableEq line 24
  4. instance OAI.BinPackingGap.PackingMachineLayout.tapeDecidableEq line 28
  5. def OAI.BinPackingGap.PackingMachineLayout.registers line 32
  6. def OAI.BinPackingGap.PackingMachineLayout.inputs line 35
  7. def OAI.BinPackingGap.PackingMachineLayout.others line 39
  8. def OAI.BinPackingGap.PackingMachineLayout.itemRegisters line 43
  9. def OAI.BinPackingGap.PackingMachineLayout.itemSlots line 63
  10. def OAI.BinPackingGap.PackingMachineLayout.values line 67
  11. theorem OAI.BinPackingGap.PackingMachineLayout.values_inputs line 74
  12. theorem OAI.BinPackingGap.PackingMachineLayout.values_others line 79
  13. theorem OAI.BinPackingGap.PackingMachineLayout.values_itemRegisters line 84
  14. def OAI.BinPackingGap.PackingMachineLayout.tapes line 93
  15. theorem OAI.BinPackingGap.PackingMachineLayout.item_shape line 99
  16. theorem OAI.BinPackingGap.PackingMachineLayout.itemSlots_outside line 110
  17. theorem OAI.BinPackingGap.PackingMachineLayout.tapes_extra line 117
  18. theorem OAI.BinPackingGap.PackingMachineLayout.values_update_input line 125
  19. theorem OAI.BinPackingGap.PackingMachineLayout.values_update_other line 139
  20. theorem OAI.BinPackingGap.PackingLayoutCommands.values_width line 164
  21. theorem OAI.BinPackingGap.PackingLayoutCommands.input_ne_other line 175
  22. def OAI.BinPackingGap.PackingLayoutCommands.inputFromOther line 181
  23. def OAI.BinPackingGap.PackingLayoutCommands.inputFromOtherTime line 187
  24. theorem OAI.BinPackingGap.PackingLayoutCommands.inputFromOther_exec line 192
  25. def OAI.BinPackingGap.PackingLayoutCommands.otherFromInput line 208
  26. def OAI.BinPackingGap.PackingLayoutCommands.otherFromInputTime line 214
  27. theorem OAI.BinPackingGap.PackingLayoutCommands.otherFromInput_exec line 219
  28. def OAI.BinPackingGap.PackingLayoutCommands.setInput line 235
  29. def OAI.BinPackingGap.PackingLayoutCommands.setInputTime line 240
  30. theorem OAI.BinPackingGap.PackingLayoutCommands.setInput_exec line 245
  31. def OAI.BinPackingGap.PackingLayoutCommands.setOther line 260
  32. def OAI.BinPackingGap.PackingLayoutCommands.setOtherTime line 265
  33. theorem OAI.BinPackingGap.PackingLayoutCommands.setOther_exec line 270
  34. def OAI.BinPackingGap.PackingVertexUpdate.updateRegisters line 294
  35. theorem OAI.BinPackingGap.PackingVertexUpdate.updateRegisters_zero line 305
  36. theorem OAI.BinPackingGap.PackingVertexUpdate.updateRegisters_one line 311
  37. theorem OAI.BinPackingGap.PackingVertexUpdate.updateRegisters_two line 317
  38. def OAI.BinPackingGap.PackingVertexUpdate.updateSlots line 322
  39. theorem OAI.BinPackingGap.PackingVertexUpdate.values_updateRegisters line 329
  40. theorem OAI.BinPackingGap.PackingVertexUpdate.shape line 343
  41. theorem OAI.BinPackingGap.PackingVertexUpdate.updated_shape line 359
  42. theorem OAI.BinPackingGap.PackingVertexUpdate.exec line 384
  43. theorem OAI.BinPackingGap.PackingVertexUpdate.general_shape line 415
  44. theorem OAI.BinPackingGap.PackingVertexUpdate.general_updated_shape line 434
  45. theorem OAI.BinPackingGap.PackingVertexUpdate.general_exec line 464