OAI/Computability/QuantumFactoring/NodeStateCircuit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.width line 18
  2. abbrev OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.inWidth line 19
  3. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.pending line 21
  4. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.output line 23
  5. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.bad line 25
  6. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.top line 27
  7. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.old line 28
  8. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.supplied line 29
  9. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nodeInput line 30
  10. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextPending line 32
  11. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.emission line 34
  12. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextOutput line 36
  13. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextBad line 39
  14. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.step line 41
  15. def OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.pack line 44
  16. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.pending_pack line 47
  17. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.output_pack line 51
  18. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.bad_pack line 58
  19. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.top_pack line 62
  20. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.old_append line 67
  21. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.supplied_append line 71
  22. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nodeInput_pack line 75
  23. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.nextBad_pack line 80
  24. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.step_prime line 88
  25. lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.step_split line 109