OAI/Computability/QuantumFactoring/CircuitEmissionModel.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ExactQuantumFactoring.CircuitEmission.Op line 13
  2. def OAI.ExactQuantumFactoring.CircuitEmission.eraseOp line 17
  3. def OAI.ExactQuantumFactoring.CircuitEmission.Op.encode line 18
  4. lemma OAI.ExactQuantumFactoring.CircuitEmission.eraseOp_encode line 20
  5. def OAI.ExactQuantumFactoring.CircuitEmission.Op.map line 22
  6. def OAI.ExactQuantumFactoring.CircuitEmission.Op.reverse line 23
  7. lemma OAI.ExactQuantumFactoring.CircuitEmission.eraseOp_place line 24
  8. lemma OAI.ExactQuantumFactoring.CircuitEmission.eraseOp_reverse line 28
  9. structure OAI.ExactQuantumFactoring.CircuitEmission.Data line 30
  10. def OAI.ExactQuantumFactoring.CircuitEmission.erase line 34
  11. def OAI.ExactQuantumFactoring.CircuitEmission.Data.encode line 35
  12. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_encode line 36
  13. def OAI.ExactQuantumFactoring.CircuitEmission.primitiveCode line 39
  14. def OAI.ExactQuantumFactoring.CircuitEmission.gateView line 40
  15. def OAI.ExactQuantumFactoring.CircuitEmission.gatePayload line 41
  16. def OAI.ExactQuantumFactoring.CircuitEmission.gateCode line 43
  17. def OAI.ExactQuantumFactoring.CircuitEmission.opView line 44
  18. def OAI.ExactQuantumFactoring.CircuitEmission.opPayload line 45
  19. def OAI.ExactQuantumFactoring.CircuitEmission.opCode line 46
  20. def OAI.ExactQuantumFactoring.CircuitEmission.dataView line 47
  21. def OAI.ExactQuantumFactoring.CircuitEmission.dataPayload line 48
  22. def OAI.ExactQuantumFactoring.CircuitEmission.dataCode line 49
  23. def OAI.ExactQuantumFactoring.CircuitEmission.Op.encodeClipped line 51
  24. def OAI.ExactQuantumFactoring.CircuitEmission.Data.encodeClipped line 54
  25. lemma OAI.ExactQuantumFactoring.CircuitEmission.eraseOp_encodeClipped line 56
  26. lemma OAI.ExactQuantumFactoring.CircuitEmission.erase_encodeClipped line 64