OAI/Computability/BinPacking/Packing/PackingTokenAffine.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.PackingTokenAffine.transition line 12
  2. def OAI.BinPackingGap.PackingTokenAffine.emit line 14
  3. def OAI.BinPackingGap.PackingTokenAffine.scanOutput line 18
  4. theorem OAI.BinPackingGap.PackingTokenAffine.scanOutput_nil line 21
  5. theorem OAI.BinPackingGap.PackingTokenAffine.scanOutput_cons line 23
  6. theorem OAI.BinPackingGap.PackingTokenAffine.scanOutput_replicate_append line 27
  7. theorem OAI.BinPackingGap.PackingTokenAffine.scanOutput_replicate line 46
  8. theorem OAI.BinPackingGap.PackingTokenAffine.scanOutput_encodeWord line 52
  9. theorem OAI.BinPackingGap.PackingTokenAffine.tokens_encodeWord line 57
  10. theorem OAI.BinPackingGap.PackingTokenAffine.emit_length_le line 62
  11. abbrev OAI.BinPackingGap.PackingTokenAffine.State line 66
  12. def OAI.BinPackingGap.PackingTokenAffine.clean line 68
  13. inductive OAI.BinPackingGap.PackingTokenAffine.Label line 70
  14. def OAI.BinPackingGap.PackingTokenAffine.instruction line 79
  15. theorem OAI.BinPackingGap.PackingTokenAffine.scanTrace line 91
  16. theorem OAI.BinPackingGap.PackingTokenAffine.tokensTrace line 113
  17. theorem OAI.BinPackingGap.PackingTokenAffine.seedStep line 130
  18. theorem OAI.BinPackingGap.PackingTokenAffine.seededScanTrace line 143
  19. theorem OAI.BinPackingGap.PackingTokenAffine.seededTrace line 172
  20. theorem OAI.BinPackingGap.PackingTokenAffine.encodedAccumulateTrace line 189
  21. def OAI.BinPackingGap.PackingTokenAffine.seededInTime line 206
  22. def OAI.BinPackingGap.PackingTokenAffine.encodedAccumulateInTime line 225