OAI/Computability/BinPacking/Packing/PairExpressionCompiler.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.PairExpressionCompiler.Reg line 14
  2. def OAI.BinPackingGap.PairExpressionCompiler.input line 16
  3. def OAI.BinPackingGap.PairExpressionCompiler.numNodes line 18
  4. def OAI.BinPackingGap.PairExpressionCompiler.denNodes line 22
  5. def OAI.BinPackingGap.PairExpressionCompiler.initial line 26
  6. def OAI.BinPackingGap.PairExpressionCompiler.numCommands line 30
  7. def OAI.BinPackingGap.PairExpressionCompiler.denCommands line 33
  8. def OAI.BinPackingGap.PairExpressionCompiler.commands line 36
  9. def OAI.BinPackingGap.PairExpressionCompiler.numRoot line 38
  10. def OAI.BinPackingGap.PairExpressionCompiler.denRoot line 39
  11. theorem OAI.BinPackingGap.PairExpressionCompiler.numRoot_ne_denRoot line 42
  12. theorem OAI.BinPackingGap.PairExpressionCompiler.num_correct line 47
  13. theorem OAI.BinPackingGap.PairExpressionCompiler.den_correct line 52
  14. theorem OAI.BinPackingGap.PairExpressionCompiler.first_preserves_input line 57
  15. theorem OAI.BinPackingGap.PairExpressionCompiler.first_den_empty line 62
  16. theorem OAI.BinPackingGap.PairExpressionCompiler.ready line 70
  17. theorem OAI.BinPackingGap.PairExpressionCompiler.numerator_output line 76
  18. theorem OAI.BinPackingGap.PairExpressionCompiler.denominator_output line 87
  19. theorem OAI.BinPackingGap.PairExpressionCompiler.preserves_input line 93
  20. def OAI.BinPackingGap.PairExpressionCompiler.clearList line 100
  21. theorem OAI.BinPackingGap.PairExpressionCompiler.clearList_ready line 102
  22. theorem OAI.BinPackingGap.PairExpressionCompiler.clearList_result line 108
  23. def OAI.BinPackingGap.PairExpressionCompiler.temporaryList line 122
  24. theorem OAI.BinPackingGap.PairExpressionCompiler.mem_temporaryList line 126
  25. def OAI.BinPackingGap.PairExpressionCompiler.clearCommands line 130
  26. theorem OAI.BinPackingGap.PairExpressionCompiler.clear_ready line 132
  27. theorem OAI.BinPackingGap.PairExpressionCompiler.clear_result line 135
  28. def OAI.BinPackingGap.PairExpressionCompiler.consumed line 143
  29. theorem OAI.BinPackingGap.PairExpressionCompiler.consumed_input line 146
  30. theorem OAI.BinPackingGap.PairExpressionCompiler.clear_after_consumed line 150
  31. theorem OAI.BinPackingGap.PairExpressionCompiler.initial_width line 160