OAI/Computability/QuantumFactoring/AIGBitArithmeticEmission.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.AIGNetworkEmission.binaryPack line 17
  2. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.binaryPack_value line 21
  3. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.addPack_value line 28
  4. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.mulPack_value line 32
  5. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.subPack_value line 36
  6. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.divPack_value line 40
  7. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.modPack_value line 44
  8. def OAI.ExactQuantumFactoring.AIGNetworkEmission.ultPack line 49
  9. lemma OAI.ExactQuantumFactoring.AIGNetworkEmission.ultPack_value line 52
  10. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.binaryPackP line 61
  11. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.addPackP line 71
  12. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.mulPackP line 72
  13. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.subPackP line 73
  14. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.divPackP line 74
  15. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.modPackP line 75
  16. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.inputUltP line 76
  17. def OAI.ExactQuantumFactoring.AIGNetworkEmission.Emission.ultPackP line 84