OAI/Analysis/MatrixSigning/Realization/OriginalParserRoutine.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.OriginalParserRoutine.state line 11
  2. def OAI.CurrentKS.OriginalParserRoutine.start line 14
  3. def OAI.CurrentKS.OriginalParserRoutine.clearTemplate line 15
  4. def OAI.CurrentKS.OriginalParserRoutine.clearCount line 16
  5. def OAI.CurrentKS.OriginalParserRoutine.unaryPorts line 17
  6. def OAI.CurrentKS.OriginalParserRoutine.decode line 18
  7. def OAI.CurrentKS.OriginalParserRoutine.framePorts line 19
  8. def OAI.CurrentKS.OriginalParserRoutine.frameDimension line 20
  9. def OAI.CurrentKS.OriginalParserRoutine.prefixWord line 21
  10. def OAI.CurrentKS.OriginalParserRoutine.finish line 22
  11. def OAI.CurrentKS.OriginalParserRoutine.program line 24
  12. lemma OAI.CurrentKS.OriginalParserRoutine.start_spec line 27
  13. lemma OAI.CurrentKS.OriginalParserRoutine.clearTemplate_spec line 31
  14. lemma OAI.CurrentKS.OriginalParserRoutine.clearCount_spec line 37
  15. lemma OAI.CurrentKS.OriginalParserRoutine.decode_spec line 42
  16. lemma OAI.CurrentKS.OriginalParserRoutine.frameDimension_spec line 51
  17. lemma OAI.CurrentKS.OriginalParserRoutine.prefixWord_spec line 56
  18. lemma OAI.CurrentKS.OriginalParserRoutine.finish_spec line 62
  19. lemma OAI.CurrentKS.OriginalParserRoutine.canonical_eq line 67
  20. def OAI.CurrentKS.OriginalParserRoutine.ticks line 72
  21. theorem OAI.CurrentKS.OriginalParserRoutine.program_spec line 77
  22. def OAI.CurrentKS.OriginalParserRoutine.routine line 92
  23. lemma OAI.CurrentKS.OriginalParserRoutine.originalCode_length line 94
  24. lemma OAI.CurrentKS.OriginalParserRoutine.ticks_le line 101