OAI/Computability/QuantumFactoring/BitStackListCode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.listCode line 14
  2. def OAI.ExactQuantumFactoring.BitStackProgram.emptyCode line 18
  3. def OAI.ExactQuantumFactoring.BitStackProgram.listView line 20
  4. lemma OAI.ExactQuantumFactoring.BitStackProgram.listCode_length_cons line 24
  5. lemma OAI.ExactQuantumFactoring.BitStackProgram.listCode_length_append line 28
  6. lemma OAI.ExactQuantumFactoring.BitStackProgram.listCode_length_rev line 34
  7. lemma OAI.ExactQuantumFactoring.BitStackProgram.listCode_length_pos line 45
  8. lemma OAI.ExactQuantumFactoring.BitStackProgram.list_length_le_code line 48
  9. lemma OAI.ExactQuantumFactoring.BitStackProgram.listCode_tail_le line 53
  10. lemma OAI.ExactQuantumFactoring.BitStackProgram.code_le_of_mem line 59
  11. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.listUncons line 72
  12. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.listCons line 76
  13. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.listHead line 80
  14. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.listTail line 84
  15. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.listEmpty line 88