OAI/Computability/QuantumFactoring/AIGInputs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.AIGCompiler.inputsPrefix line 13

   Source documentation

   One real AIG atom per input bit. The initial graph has one false node.

   def inputsPrefix (n : ℕ) : (k : ℕ) → k ≤ n →
       (g : AIG (Fin n)) × (Fin k → AIG.Ref g)
     | 0, _ => ⟨AIG.empty, Fin.elim0⟩
     | k+1, h =>
       let old := inputsPrefix n k (by omega)
   …

2. lemma OAI.ExactQuantumFactoring.AIGCompiler.inputsPrefix_size line 21
3. lemma OAI.ExactQuantumFactoring.AIGCompiler.inputsPrefix_correct line 26
4. def OAI.ExactQuantumFactoring.AIGCompiler.inputs line 41
5. lemma OAI.ExactQuantumFactoring.AIGCompiler.inputs_size line 43
6. lemma OAI.ExactQuantumFactoring.AIGCompiler.inputs_correct line 45
7. def OAI.ExactQuantumFactoring.AIGCompiler.refVector line 49

   Source documentation

   A vector of ordinary references; this constructor emits no graph nodes.

   def refVector {α : Type} [Hashable α] [DecidableEq α] {g : AIG α} {w : ℕ}
       (f : Fin w → AIG.Ref g) : AIG.RefVec g w where
   …

8. lemma OAI.ExactQuantumFactoring.AIGCompiler.refVector_get line 54