OAI/Computability/QuantumFactoring/BitStackProducts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.prodCode line 14
2. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.left line 22

   Source documentation

   Run a procedure on the first component, keeping the second component literally on a disjoint stack. Parsing and re-quoting are explicitly charged.

   noncomputable def left (p : Procedure ea eb f) (ec : γ→List Bool) :
       Procedure (prodCode ea ec) (prodCode eb ec) (fun x=>(f x.1,x.2)) where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.prodCode

3. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.swap line 75

   Source documentation

   Exchange two quoted word fields, without a unit-cost tuple operation.

   noncomputable def swap (ea : α→List Bool) (eb : β→List Bool) :
       Procedure (prodCode ea eb) (prodCode eb ea) Prod.swap where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.prodCode

4. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.parallel line 107

   Source documentation

   Two arbitrary already verified subroutines acting independently on a pair.

   noncomputable def parallel {δ : Type} {ed : δ→List Bool} {g : γ→δ}
       (p : Procedure ea eb f) (q : Procedure ec ed g) :
       Procedure (prodCode ea ec) (prodCode eb ed) (fun x=>(f x.1,g x.2)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.prodCode