OAI/Computability/BinPacking/Arithmetic/PackingRegisterUpdate.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.PackingRegisterUpdate.Kind line 13
  2. instance OAI.BinPackingGap.PackingRegisterUpdate.(instance at line 17) line 17
  3. def OAI.BinPackingGap.PackingRegisterUpdate.operation line 21
  4. def OAI.BinPackingGap.PackingRegisterUpdate.operands line 26
  5. def OAI.BinPackingGap.PackingRegisterUpdate.operator line 34
  6. def OAI.BinPackingGap.PackingRegisterUpdate.commands line 38
  7. def OAI.BinPackingGap.PackingRegisterUpdate.values line 41
  8. theorem OAI.BinPackingGap.PackingRegisterUpdate.commands_ready line 43
  9. theorem OAI.BinPackingGap.PackingRegisterUpdate.commands_result line 47
  10. theorem OAI.BinPackingGap.PackingRegisterUpdate.operation_size_le line 54
  11. theorem OAI.BinPackingGap.PackingRegisterUpdate.commands_budget line 64
  12. theorem OAI.BinPackingGap.PackingRegisterUpdate.commands_budget_le line 71
  13. def OAI.BinPackingGap.PackingRegisterUpdate.main line 79
  14. def OAI.BinPackingGap.PackingRegisterUpdate.code line 84
  15. theorem OAI.BinPackingGap.PackingRegisterUpdate.exec line 88