OAI/Computability/QuantumFactoring/ExpressionResources.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExactQuantumFactoring.nat_size_max line 13
  2. def OAI.ExactQuantumFactoring.NatExpr.weight line 22

    Source documentation

    Actual syntax length, sharing-sensitive compiler cost and constant bit size.

    def weight (e : NatExpr v) : ℕ := e.size + e.sharedCost + e.maxConst.size

    Mentions: OAI.ExactQuantumFactoring.NatExpr

  3. lemma OAI.ExactQuantumFactoring.NatExpr.weight_var line 23
  4. lemma OAI.ExactQuantumFactoring.NatExpr.weight_const line 24
  5. lemma OAI.ExactQuantumFactoring.NatExpr.weight_add line 26
  6. lemma OAI.ExactQuantumFactoring.NatExpr.weight_sub line 28
  7. lemma OAI.ExactQuantumFactoring.NatExpr.weight_mul line 30
  8. lemma OAI.ExactQuantumFactoring.NatExpr.weight_div line 32
  9. lemma OAI.ExactQuantumFactoring.NatExpr.weight_mod line 34
  10. lemma OAI.ExactQuantumFactoring.NatExpr.weight_iteLe line 36
  11. lemma OAI.ExactQuantumFactoring.NatExpr.weight_pos line 39
  12. lemma OAI.ExactQuantumFactoring.NatExpr.size_le_weight line 43
  13. lemma OAI.ExactQuantumFactoring.NatExpr.sharedCost_le_weight line 44
  14. lemma OAI.ExactQuantumFactoring.NatExpr.constSize_le_weight line 45
  15. lemma OAI.ExactQuantumFactoring.NatExpr.weight_pow line 46
  16. lemma OAI.ExactQuantumFactoring.NatExpr.templateWidth_le line 53
  17. lemma OAI.ExactQuantumFactoring.NatExpr.template_weight_count line 57
  18. def OAI.ExactQuantumFactoring.NatExprPoly line 71

    Source documentation

    Uniform polynomial growth of a family of literal natural expressions. Nothing here bounds the values of dynamic variables or assumes arithmetic is free.

    def NatExprPoly {v : ℕ → Type*} (f : ∀ n, NatExpr (v n)) : Prop :=
…

    Mentions: OAI.ExactQuantumFactoring.NatExpr

  19. lemma OAI.ExactQuantumFactoring.NatExprPoly.var line 76
  20. lemma OAI.ExactQuantumFactoring.NatExprPoly.const line 78
  21. lemma OAI.ExactQuantumFactoring.NatExprPoly.add line 81
  22. lemma OAI.ExactQuantumFactoring.NatExprPoly.sub line 85
  23. lemma OAI.ExactQuantumFactoring.NatExprPoly.mul line 89
  24. lemma OAI.ExactQuantumFactoring.NatExprPoly.div line 93
  25. lemma OAI.ExactQuantumFactoring.NatExprPoly.mod line 97
  26. lemma OAI.ExactQuantumFactoring.NatExprPoly.iteLe line 101
  27. lemma OAI.ExactQuantumFactoring.NatExprPoly.pow line 105
  28. lemma OAI.ExactQuantumFactoring.NatExprPoly.templateWidth line 109