OAI/Computability/QuantumFactoring/EmissionCombinators.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.Emits line 12

    Source documentation

    Existence of a charged, clean, finite-alphabet stack procedure.

    def Emits {α β : Type} (ea : α→List Bool) (eb : β→List Bool) (f : α→β) : Prop :=
…
  2. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.ofProcedure line 17
  3. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.id line 18
  4. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.const line 19
  5. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.comp line 20
  6. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.pair line 23
  7. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.fst line 26
  8. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.snd line 28
  9. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.congr line 30
  10. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.precompose line 32
  11. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.natAdd line 34
  12. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.natSub line 36
  13. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.natMul line 38
  14. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.natDiv line 40
  15. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.natMod line 42
  16. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.natMax line 44
  17. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.unaryNat line 46
  18. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nvar line 55
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nconst line 58
  20. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nadd line 61
  21. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nsub line 65
  22. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nmul line 69
  23. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.ndiv line 73
  24. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nmod line 77
  25. lemma OAI.ExactQuantumFactoring.NetworkEmission.Emits.nite line 81