OAI/Computability/QuantumFactoring/NetworkEmissionModel.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.ExactQuantumFactoring.NetworkEmission.Node line 11
  2. def OAI.ExactQuantumFactoring.NetworkEmission.Node.map line 18
  3. def OAI.ExactQuantumFactoring.NetworkEmission.eraseNode line 23
  4. lemma OAI.ExactQuantumFactoring.NetworkEmission.eraseNode_map line 28
  5. def OAI.ExactQuantumFactoring.NetworkEmission.eraseNet line 31
  6. lemma OAI.ExactQuantumFactoring.NetworkEmission.eraseNet_length line 34
  7. def OAI.ExactQuantumFactoring.NetworkEmission.attachIndex line 39
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.attachIndex_input line 41
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.attachIndex_work line 43
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.attach_output line 45
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.attach_erase line 61
  12. structure OAI.ExactQuantumFactoring.NetworkEmission.Data line 69
  13. def OAI.ExactQuantumFactoring.NetworkEmission.erase line 75
  14. def OAI.ExactQuantumFactoring.NetworkEmission.attachRawIndex line 77
  15. lemma OAI.ExactQuantumFactoring.NetworkEmission.attachRawIndex_ofFn line 79
  16. def OAI.ExactQuantumFactoring.NetworkEmission.comp line 89
  17. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_comp line 92
  18. def OAI.ExactQuantumFactoring.NetworkEmission.select line 102
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_select line 103
  20. def OAI.ExactQuantumFactoring.NetworkEmission.node line 106
  21. lemma OAI.ExactQuantumFactoring.NetworkEmission.erase_node line 107