OAI/Computability/QuantumFactoring/BooleanNetworkFurther.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BooleanNetwork.eval line 11
  2. def OAI.ExactQuantumFactoring.BooleanNetwork.select line 14
  3. def OAI.ExactQuantumFactoring.BooleanNetwork.node line 16
  4. def OAI.ExactQuantumFactoring.BooleanNetwork.comp line 19
  5. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_comp line 23
  6. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_comp line 30
  7. def OAI.ExactQuantumFactoring.BooleanNetwork.pair line 34

    Source documentation

    Parallel computations share the input but retain disjoint new traces.

    def pair {n m l : ℕ} (a : BooleanNetwork n m) (b : BooleanNetwork n l) : BooleanNetwork n (m+l) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

  8. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_pair line 40
  9. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_pair line 54
  10. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_select line 57
  11. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_select line 60
  12. lemma OAI.ExactQuantumFactoring.BooleanNetwork.eval_node line 63
  13. lemma OAI.ExactQuantumFactoring.BooleanNetwork.count_node line 67