OAI/Computability/QuantumFactoring/BitStackRelabel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.Program.relabel line 13
2. def OAI.ExactQuantumFactoring.BitStackProgram.overlay line 21

   Source documentation

   An extension of a small register store with arbitrary untouched registers.

   noncomputable def overlay (f : K ↪ L) (base : Store L) (s : Store K) : Store L := by
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Store

3. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_at line 25
4. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_outside line 34
5. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_update line 42
6. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_self line 57
7. lemma OAI.ExactQuantumFactoring.BitStackProgram.Runs.relabel line 66

   Source documentation

   Exact-cost subroutine embedding. Scratch separation is proved, not assumed as an extra TM operation.

   lemma Runs.relabel {p : Program K} {s t : Store K} {c : ℕ}
       (h : Runs p s t c) (f : K ↪ L) (base : Store L) :
       Runs (p.relabel f) (overlay f base s) (overlay f base t) c := by
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Program, OAI.ExactQuantumFactoring.BitStackProgram.Store, OAI.ExactQuantumFactoring.BitStackProgram.Runs, OAI.ExactQuantumFactoring.BitStackProgram.overlay