OAI/Computability/BinPacking/Hardness/LiteralSlotGraphComputation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literal_variable_add_two_le_bits line 12
  2. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.two_mul_length_le_literalsBits_length line 17
  3. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literal_bits_length_le_literalsBits line 26
  4. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literal_variable_le_literalsBits line 40
  5. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.literalsBits_formula_length_le line 47
  6. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.formula_literal_variable_le_input line 53
  7. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.natBits_length_le_unary line 58
  8. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.pairRecord_length_le line 65
  9. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexRecord_length_le line 72
  10. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.vertexRecords_length_le line 78
  11. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rowEdges_length_le line 88
  12. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rowEdges_endpoint_bounds line 97
  13. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.suffixEdges_endpoint_bounds line 116
  14. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.suffixEdges_length_le_sq line 131
  15. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.edgeRecords_length_le line 141
  16. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rowEdgeRecords_length_le line 154
  17. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.suffixEdgeRecords_length_le line 163
  18. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.formulaEdgeRecords_length_le line 172
  19. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.formulaGraphWord_length_le line 184
  20. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.edgeRecords_listBits line 207
  21. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rawInput_formula line 217
  22. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rawGraphWord_graphBits line 221
  23. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.rawCost_formula_le line 242
  24. def OAI.BinPackingGap.LiteralSlotGraphMachine.outputsInTime line 279
  25. def OAI.BinPackingGap.LiteralSlotGraphMachine.computation line 291
  26. theorem OAI.BinPackingGap.LiteralSlotGraphMachine.computation_finiteAlphabet line 308