OAI/Analysis/MatrixSigning/Realization/PSDCleanRoutine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.PSDCleanRoutine.Datum line 13
  2. def OAI.CurrentKS.PSDCleanRoutine.input line 15
  3. def OAI.CurrentKS.PSDCleanRoutine.output line 17
  4. def OAI.CurrentKS.PSDCleanRoutine.parsed line 20
  5. def OAI.CurrentKS.PSDCleanRoutine.decode line 22
  6. def OAI.CurrentKS.PSDCleanRoutine.install line 23
  7. def OAI.CurrentKS.PSDCleanRoutine.extract line 24
  8. def OAI.CurrentKS.PSDCleanRoutine.program line 25
  9. lemma OAI.CurrentKS.PSDCleanRoutine.decode_spec line 27
  10. lemma OAI.CurrentKS.PSDCleanRoutine.install_spec line 35
  11. lemma OAI.CurrentKS.PSDCleanRoutine.extract_spec line 43
  12. def OAI.CurrentKS.PSDCleanRoutine.controllerTicks line 51
  13. def OAI.CurrentKS.PSDCleanRoutine.ticks line 55
  14. lemma OAI.CurrentKS.PSDCleanRoutine.program_spec line 59
  15. def OAI.CurrentKS.PSDCleanRoutine.routine line 66
  16. lemma OAI.CurrentKS.PSDCleanRoutine.output_length line 71
  17. lemma OAI.CurrentKS.PSDCleanRoutine.ticks_le line 79