OAI/Computability/QuantumFactoring/NetworkEmissionBasic.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NetworkEmission.bit line 14
  2. def OAI.ExactQuantumFactoring.NetworkEmission.constant line 15
  3. def OAI.ExactQuantumFactoring.NetworkEmission.bnot line 16
  4. def OAI.ExactQuantumFactoring.NetworkEmission.band line 17
  5. def OAI.ExactQuantumFactoring.NetworkEmission.bor line 18
  6. def OAI.ExactQuantumFactoring.NetworkEmission.bxor line 19
  7. def OAI.ExactQuantumFactoring.NetworkEmission.mux line 20
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_bit line 21
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_constant line 23
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_bnot line 25
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_band line 27
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_bor line 29
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_bxor line 31
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_mux line 33
  15. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.selectP line 38
  16. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.nodeP line 42
  17. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.pairIndexP line 48
  18. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.pairP line 56
  19. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.bitP line 68
  20. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.constantP line 71
  21. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.bnotP line 73
  22. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.bandP line 75
  23. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.borP line 77
  24. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.bxorP line 79
  25. def OAI.ExactQuantumFactoring.NetworkEmission.Emission.muxP line 83