OAI/Computability/QuantumFactoring/NaturalExpressionCircuit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitArithmetic.natSubOn line 16
  2. lemma OAI.ExactQuantumFactoring.BitArithmetic.natSubOn_value line 19
  3. lemma OAI.ExactQuantumFactoring.BitArithmetic.natSubOn_count line 34
  4. def OAI.ExactQuantumFactoring.NatExpr.compile line 45
  5. lemma OAI.ExactQuantumFactoring.NatExpr.compile_value line 56
  6. def OAI.ExactQuantumFactoring.NatExpr.cost line 88

    Source documentation

    Syntactic duplication cost; independent of the numerical constants.

    def cost : NatExpr v → ℕ
  | .var _ | .const _ => 1
  | .add a b | .mul a b | .sub a b | .div a b | .mod a b => 2*(cost a+cost b)+1
  | .iteLe a b c d => 2*(cost a+cost b+cost c+cost d)+1

    Mentions: OAI.ExactQuantumFactoring.NatExpr

  7. def OAI.ExactQuantumFactoring.NatExpr.operationBound line 93
  8. lemma OAI.ExactQuantumFactoring.NatExpr.compile_count line 95