OAI/Computability/QuantumFactoring/CircuitBooleanEmission.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.CircuitEmission.notOp line 15
  2. def OAI.ExactQuantumFactoring.CircuitEmission.cnotOp line 16
  3. def OAI.ExactQuantumFactoring.CircuitEmission.toffoliOp line 17
  4. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_notAt line 18
  5. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_cnotAt line 19
  6. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_toffoliAt line 20
  7. def OAI.ExactQuantumFactoring.CircuitEmission.nodeOps line 23
  8. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_node_compile line 29
  9. def OAI.ExactQuantumFactoring.CircuitEmission.netOps line 40
  10. lemma OAI.ExactQuantumFactoring.CircuitEmission.netOps_append_one line 42
  11. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_net_compile line 45
  12. def OAI.ExactQuantumFactoring.CircuitEmission.copyOps line 54
  13. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_copyPrefix line 55
  14. def OAI.ExactQuantumFactoring.CircuitEmission.oracleOps line 68
  15. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_oracle line 71