OAI/Computability/BinPacking/Arithmetic/GraphPackingRegisters.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.GraphPackingRegisters.parameters line 13
  2. inductive OAI.BinPackingGap.GraphPackingRegisters.Work line 16
  3. instance OAI.BinPackingGap.GraphPackingRegisters.(instance at line 21) line 21
  4. inductive OAI.BinPackingGap.GraphPackingRegisters.Extra line 26
  5. instance OAI.BinPackingGap.GraphPackingRegisters.(instance at line 32) line 32
  6. abbrev OAI.BinPackingGap.GraphPackingRegisters.Numerator line 38
  7. abbrev OAI.BinPackingGap.GraphPackingRegisters.Other line 39
  8. abbrev OAI.BinPackingGap.GraphPackingRegisters.Register line 40
  9. abbrev OAI.BinPackingGap.GraphPackingRegisters.Tape line 42
  10. def OAI.BinPackingGap.GraphPackingRegisters.slots line 45
  11. def OAI.BinPackingGap.GraphPackingRegisters.item line 48
  12. def OAI.BinPackingGap.GraphPackingRegisters.setup line 51
  13. def OAI.BinPackingGap.GraphPackingRegisters.work line 56
  14. def OAI.BinPackingGap.GraphPackingRegisters.input line 60
  15. def OAI.BinPackingGap.GraphPackingRegisters.output line 63
  16. def OAI.BinPackingGap.GraphPackingRegisters.setupSlots line 66
  17. def OAI.BinPackingGap.GraphPackingRegisters.graphSlots line 70
  18. inductive OAI.BinPackingGap.GraphPackingRegisters.CountSource line 77
  19. def OAI.BinPackingGap.GraphPackingRegisters.countRegister line 83
  20. def OAI.BinPackingGap.GraphPackingRegisters.tallyRegisters line 88
  21. def OAI.BinPackingGap.GraphPackingRegisters.tallySlots line 108
  22. theorem OAI.BinPackingGap.GraphPackingRegisters.tally_outside line 112
  23. def OAI.BinPackingGap.GraphPackingRegisters.endpointRegisters line 117
  24. def OAI.BinPackingGap.GraphPackingRegisters.endpointSlots line 127
  25. theorem OAI.BinPackingGap.GraphPackingRegisters.endpoint_outside line 131
  26. def OAI.BinPackingGap.GraphPackingRegisters.powerSlots line 136
  27. def OAI.BinPackingGap.GraphPackingRegisters.decoderSlots line 174
  28. def OAI.BinPackingGap.GraphPackingRegisters.thresholdSlots line 181