OAI/Computability/QuantumFactoring/BitStackLists.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.reverseMove line 14

   Source documentation

   Reverse one stack onto another, preserving all symbols.

   def reverseMove (a b : K) : Program K := .loop a (.push b false) (.push b true)

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Program

2. def OAI.ExactQuantumFactoring.BitStackProgram.clear line 15
3. def OAI.ExactQuantumFactoring.BitStackProgram.duplicateReverse line 17
4. lemma OAI.ExactQuantumFactoring.BitStackProgram.update_comm line 21
5. lemma OAI.ExactQuantumFactoring.BitStackProgram.clear_runs line 27
6. lemma OAI.ExactQuantumFactoring.BitStackProgram.reverseMove_runs line 44
7. lemma OAI.ExactQuantumFactoring.BitStackProgram.duplicateReverse_loop_runs line 71
8. lemma OAI.ExactQuantumFactoring.BitStackProgram.duplicateReverse_runs line 106