OAI/Computability/QuantumFactoring/ArithmeticSyntaxEmission.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iOfNat line 19
  2. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iOfInt line 21
  3. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iAdd line 24
  4. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iNeg line 26
  5. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iSub line 27
  6. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iMul line 28
  7. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iScale line 30
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iToNat line 32
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iNatAbs line 33
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iIte line 35
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iIfLe line 37
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rOfInt line 40
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rOfNat line 41
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rConst line 42
  15. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rNormalize line 44
  16. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rAdd line 47
  17. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rNeg line 50
  18. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rSub line 51
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rMul line 52
  20. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rInv line 54
  21. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rDiv line 56
  22. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rPow line 57
  23. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rIfNatLe line 61
  24. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rIfIntLe line 64
  25. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rIfLe line 67
  26. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rIfLt line 71
  27. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rIfEq line 73
  28. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rMax line 75
  29. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rMin line 76
  30. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iCeilRatio line 77
  31. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.iFloorRatio line 79
  32. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rCeilNat line 81
  33. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rFloor line 82
  34. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.rCeil line 83