OAI/Analysis/MatrixSigning/Realization/OriginalOutputRoutine.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Realization.wordCode line 12
  2. def OAI.CurrentKS.Realization.appendBit line 14
  3. lemma OAI.CurrentKS.Realization.fold_appendBit line 17
  4. def OAI.CurrentKS.Realization.outputBits line 22
  5. def OAI.CurrentKS.Realization.fullBody line 26
  6. def OAI.CurrentKS.OriginalTailRoutine.clearD line 36
  7. def OAI.CurrentKS.OriginalTailRoutine.clearN line 37
  8. def OAI.CurrentKS.OriginalTailRoutine.program line 38
  9. lemma OAI.CurrentKS.OriginalTailRoutine.clearD_spec line 39
  10. lemma OAI.CurrentKS.OriginalTailRoutine.clearN_spec line 44
  11. def OAI.CurrentKS.OriginalTailRoutine.ticks line 49
  12. lemma OAI.CurrentKS.OriginalTailRoutine.program_spec line 51
  13. def OAI.CurrentKS.OriginalTailRoutine.routine line 59
  14. lemma OAI.CurrentKS.OriginalTailRoutine.ticks_le line 60
  15. def OAI.CurrentKS.Realization.originalEmpty line 73
  16. lemma OAI.CurrentKS.Realization.signing_empty line 84
  17. def OAI.CurrentKS.Realization.originalSigning line 91
  18. theorem OAI.CurrentKS.Realization.originalSigning_good line 98