OAI/Computability/MatchingCount/PolyCoding.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. class OAI.BinaryMatching.StackCode.Coding line 9
  2. instance OAI.BinaryMatching.StackCode.(instance at line 12) line 12
  3. instance OAI.BinaryMatching.StackCode.(instance at line 13) line 13
  4. instance OAI.BinaryMatching.StackCode.(instance at line 14) line 14
  5. instance OAI.BinaryMatching.StackCode.(instance at line 15) line 15
  6. def OAI.BinaryMatching.StackCode.listCode line 18
  7. instance OAI.BinaryMatching.StackCode.(instance at line 21) line 21
  8. lemma OAI.BinaryMatching.StackCode.encode_nat line 23
  9. lemma OAI.BinaryMatching.StackCode.encode_bool line 24
  10. lemma OAI.BinaryMatching.StackCode.encode_pair line 25
  11. lemma OAI.BinaryMatching.StackCode.encode_prod line 27
  12. lemma OAI.BinaryMatching.StackCode.code_nil line 30
  13. lemma OAI.BinaryMatching.StackCode.code_cons line 31
  14. lemma OAI.BinaryMatching.StackCode.pairBits_append line 34
  15. lemma OAI.BinaryMatching.StackCode.code_append line 39
  16. lemma OAI.BinaryMatching.StackCode.list_length_le_code line 44
  17. def OAI.BinaryMatching.StackCode.Poly line 49
  18. def OAI.BinaryMatching.StackCode.Poly.routine line 54
  19. theorem OAI.BinaryMatching.StackCode.Poly.identity line 56
  20. theorem OAI.BinaryMatching.StackCode.Poly.constant line 57
  21. theorem OAI.BinaryMatching.StackCode.Poly.comp line 58
  22. theorem OAI.BinaryMatching.StackCode.Poly.pair line 60
  23. theorem OAI.BinaryMatching.StackCode.Poly.first line 62
  24. theorem OAI.BinaryMatching.StackCode.Poly.second line 64
  25. theorem OAI.BinaryMatching.StackCode.Poly.cond line 67
  26. theorem OAI.BinaryMatching.StackCode.Poly.codeLength line 72
  27. theorem OAI.BinaryMatching.StackCode.Poly.boundedIterate line 74
  28. theorem OAI.BinaryMatching.StackCode.Poly.congr line 79