OAI/Computability/QuantumFactoring/BitStackFrames.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.sumStore line 13
  2. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_left line 14
  3. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_right line 16
  4. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_empty line 18
  5. def OAI.ExactQuantumFactoring.BitStackProgram.leftEmbed line 21
  6. lemma OAI.ExactQuantumFactoring.BitStackProgram.overlay_left line 22
  7. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_update_left line 30
  8. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_update_right line 33
  9. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_singleton_left line 36
  10. lemma OAI.ExactQuantumFactoring.BitStackProgram.sumStore_singleton_right line 39
  11. lemma OAI.ExactQuantumFactoring.BitStackProgram.Runs.left line 42
  12. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.congrFun line 50
  13. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.identity line 60