OAI/Computability/BinPacking/Machines/DropPackingBoundMachine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.DropPackingBoundMachine.Mode line 10
  2. abbrev OAI.BinPackingGap.DropPackingBoundMachine.Mode.enumList line 14
  3. theorem OAI.BinPackingGap.DropPackingBoundMachine.Mode.enumList_getElem?_ctorIdx_eq line 16
  4. theorem OAI.BinPackingGap.DropPackingBoundMachine.Mode.enumList_nodup line 20
  5. instance OAI.BinPackingGap.DropPackingBoundMachine.(instance at line 22) line 22
  6. def OAI.BinPackingGap.DropPackingBoundMachine.transition line 26
  7. def OAI.BinPackingGap.DropPackingBoundMachine.emit line 32
  8. def OAI.BinPackingGap.DropPackingBoundMachine.output line 36
  9. theorem OAI.BinPackingGap.DropPackingBoundMachine.output_copy line 38
  10. theorem OAI.BinPackingGap.DropPackingBoundMachine.output_frame line 45
  11. theorem OAI.BinPackingGap.DropPackingBoundMachine.output_encoded line 54
  12. def OAI.BinPackingGap.DropPackingBoundMachine.reversedMachine line 58
  13. def OAI.BinPackingGap.DropPackingBoundMachine.reversedRun line 60
  14. def OAI.BinPackingGap.DropPackingBoundMachine.machine line 77
  15. def OAI.BinPackingGap.DropPackingBoundMachine.run line 80
  16. def OAI.BinPackingGap.DropPackingBoundMachine.computation line 102
  17. theorem OAI.BinPackingGap.DropPackingBoundMachine.finiteAlphabet line 115