OAI/Analysis/MatrixSigning/Arithmetic/RationalSignClassifier.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W06.RationalSignClassifier.outputCode line 15
  2. def OAI.KS.W06.RationalSignClassifier.rawCode line 18
  3. def OAI.KS.W06.RationalSignClassifier.classifyDispatch line 21
  4. def OAI.KS.W06.RationalSignClassifier.classifyProgram line 26
  5. def OAI.KS.W06.RationalSignClassifier.classifiedState line 29
  6. theorem OAI.KS.W06.RationalSignClassifier.classify_spec line 32
  7. theorem OAI.KS.W06.RationalSignClassifier.encodeNat_eq_nil line 55
  8. theorem OAI.KS.W06.RationalSignClassifier.rawCode_canonical line 63
  9. def OAI.KS.W06.RationalSignClassifier.parsedState line 72
  10. def OAI.KS.W06.RationalSignClassifier.classifiedCanonical line 74
  11. def OAI.KS.W06.RationalSignClassifier.outputState line 77
  12. def OAI.KS.W06.RationalSignClassifier.readProgram line 79
  13. def OAI.KS.W06.RationalSignClassifier.readTicks line 81
  14. theorem OAI.KS.W06.RationalSignClassifier.read_spec line 83
  15. theorem OAI.KS.W06.RationalSignClassifier.classified_length line 90
  16. theorem OAI.KS.W06.RationalSignClassifier.cleared_classified line 101
  17. def OAI.KS.W06.RationalSignClassifier.program line 108
  18. theorem OAI.KS.W06.RationalSignClassifier.canonical_spec line 110
  19. def OAI.KS.W06.RationalSignClassifier.onPorts line 123
  20. theorem OAI.KS.W06.RationalSignClassifier.onPorts_spec line 125
  21. theorem OAI.KS.W06.RationalSignClassifier.coinIndependent line 134
  22. theorem OAI.KS.W06.RationalSignClassifier.program_output line 141