OAI/Computability/QuantumFactoring/NetworkEmissionPack.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ExactQuantumFactoring.NetworkEmission.PackData line 12
  2. abbrev OAI.ExactQuantumFactoring.NetworkEmission.Pack line 15
  3. def OAI.ExactQuantumFactoring.NetworkEmission.packCode line 16
  4. def OAI.ExactQuantumFactoring.NetworkEmission.pairPack line 17
  5. def OAI.ExactQuantumFactoring.NetworkEmission.compPack line 23
  6. lemma OAI.ExactQuantumFactoring.NetworkEmission.pairPack_inputs line 29
  7. lemma OAI.ExactQuantumFactoring.NetworkEmission.compPack_inputs line 31
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.pairPack_value line 33
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.compPack_value line 35
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.packCode_bound line 37
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.packBudget_le_code line 41
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.packBudgets_le_code line 43
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.fold_budget line 49
  14. def OAI.ExactQuantumFactoring.NetworkEmission.selectPack line 55
  15. def OAI.ExactQuantumFactoring.NetworkEmission.emptyPack line 57
  16. def OAI.ExactQuantumFactoring.NetworkEmission.nodePack line 58
  17. def OAI.ExactQuantumFactoring.NetworkEmission.erasePack line 60
  18. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.packViewP line 63
  19. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.packBudgetP line 65
  20. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.packValueP line 67
  21. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.pairPackP line 69
  22. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.compPackP line 78
  23. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.foldPack line 88
  24. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.foldPairP line 106
  25. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.foldCompP line 108