OAI/Computability/BinPacking/Machines/PackingSetupGraph.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGap.PackingSetupExpression.Parameters line 17
  2. inductive OAI.BinPackingGap.PackingSetupExpression.Input line 24
  3. abbrev OAI.BinPackingGap.PackingSetupExpression.Input.enumList line 28
  4. theorem OAI.BinPackingGap.PackingSetupExpression.Input.enumList_getElem?_ctorIdx_eq line 30
  5. theorem OAI.BinPackingGap.PackingSetupExpression.Input.enumList_nodup line 34
  6. instance OAI.BinPackingGap.PackingSetupExpression.(instance at line 36) line 36
  7. inductive OAI.BinPackingGap.PackingSetupExpression.Output line 40
  8. abbrev OAI.BinPackingGap.PackingSetupExpression.Output.enumList line 46
  9. theorem OAI.BinPackingGap.PackingSetupExpression.Output.enumList_getElem?_ctorIdx_eq line 49
  10. theorem OAI.BinPackingGap.PackingSetupExpression.Output.enumList_nodup line 53
  11. instance OAI.BinPackingGap.PackingSetupExpression.(instance at line 55) line 55
  12. def OAI.BinPackingGap.PackingSetupExpression.inputs line 59
  13. def OAI.BinPackingGap.PackingSetupExpression.repetitions line 64
  14. def OAI.BinPackingGap.PackingSetupExpression.edgeRepetitions line 68
  15. def OAI.BinPackingGap.PackingSetupExpression.jobFlags line 71
  16. def OAI.BinPackingGap.PackingSetupExpression.expression line 74
  17. def OAI.BinPackingGap.PackingSetupExpression.outputValues line 92
  18. theorem OAI.BinPackingGap.PackingSetupExpression.eval_expression line 108
  19. def OAI.BinPackingGap.PackingSetupExpression.inventoryOutput line 114
  20. theorem OAI.BinPackingGap.PackingSetupExpression.outputValues_eq_inventory line 129
  21. abbrev OAI.BinPackingGap.PackingSetupMachine.Reg line 149
  22. def OAI.BinPackingGap.PackingSetupMachine.input line 151
  23. def OAI.BinPackingGap.PackingSetupMachine.output line 152
  24. def OAI.BinPackingGap.PackingSetupMachine.nodes line 154
  25. def OAI.BinPackingGap.PackingSetupMachine.frame line 161
  26. theorem OAI.BinPackingGap.PackingSetupMachine.frame_update line 166
  27. def OAI.BinPackingGap.PackingSetupMachine.block line 176
  28. theorem OAI.BinPackingGap.PackingSetupMachine.block_correct line 183
  29. def OAI.BinPackingGap.PackingSetupMachine.outputOrder line 201
  30. theorem OAI.BinPackingGap.PackingSetupMachine.mem_outputOrder line 205
  31. def OAI.BinPackingGap.PackingSetupMachine.commandsFor line 208
  32. def OAI.BinPackingGap.PackingSetupMachine.outputsAfter line 211
  33. theorem OAI.BinPackingGap.PackingSetupMachine.outputsAfter_eq line 217
  34. theorem OAI.BinPackingGap.PackingSetupMachine.commandsFor_correct line 231
  35. def OAI.BinPackingGap.PackingSetupMachine.commands line 249
  36. theorem OAI.BinPackingGap.PackingSetupMachine.commands_correct line 251
  37. def OAI.BinPackingGap.PackingSetupMachine.code line 263
  38. def OAI.BinPackingGap.PackingSetupMachine.timePolynomial line 267
  39. theorem OAI.BinPackingGap.PackingSetupMachine.exec line 270
  40. theorem OAI.BinPackingGap.PackingSetupMachine.exec_graph line 301