OAI/Computability/MatchingCount/RawInput.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryMatching.Raw.InputData.Rec line 9
  2. abbrev OAI.BinaryMatching.Raw.InputData.Data line 10
  3. def OAI.BinaryMatching.Raw.InputData.repr line 12
  4. def OAI.BinaryMatching.Raw.InputData.decodeRecord line 13
  5. lemma OAI.BinaryMatching.Raw.InputData.decodeRecord_repr line 15
  6. theorem OAI.BinaryMatching.Raw.InputData.decodeRecord_poly line 20
  7. def OAI.BinaryMatching.Raw.InputData.bound line 24
  8. def OAI.BinaryMatching.Raw.InputData.decode line 25
  9. lemma OAI.BinaryMatching.Raw.InputData.decode_encoded line 27
  10. lemma OAI.BinaryMatching.Raw.InputData.decode_n_encoded line 37
  11. lemma OAI.BinaryMatching.Raw.InputData.decode_length line 40
  12. theorem OAI.BinaryMatching.Raw.InputData.decode_poly line 41
  13. def OAI.BinaryMatching.Raw.InputData.multiplicityBits line 48
  14. lemma OAI.BinaryMatching.Raw.InputData.multiplicityBits_repr line 50
  15. lemma OAI.BinaryMatching.Raw.InputData.multiplicityBits_pair line 56
  16. theorem OAI.BinaryMatching.Raw.InputData.multiplicityBits_poly line 61
  17. def OAI.BinaryMatching.Raw.InputData.bitsBudget line 67
  18. lemma OAI.BinaryMatching.Raw.InputData.bitsBudget_repr line 68
  19. theorem OAI.BinaryMatching.Raw.InputData.bitsBudget_poly line 71
  20. def OAI.BinaryMatching.Raw.InputData.pairs line 78
  21. lemma OAI.BinaryMatching.Raw.InputData.pairs_eq line 79
  22. theorem OAI.BinaryMatching.Raw.InputData.pairs_poly line 85
  23. def OAI.BinaryMatching.Raw.InputData.betaValue line 90
  24. lemma OAI.BinaryMatching.Raw.InputData.betaValue_repr line 93
  25. theorem OAI.BinaryMatching.Raw.InputData.betaValue_poly line 98
  26. def OAI.BinaryMatching.Raw.InputData.betaMatrix line 102
  27. lemma OAI.BinaryMatching.Raw.InputData.betaMatrix_repr line 104
  28. theorem OAI.BinaryMatching.Raw.InputData.betaMatrix_poly line 111
  29. def OAI.BinaryMatching.Raw.InputData.parameters line 119
  30. lemma OAI.BinaryMatching.Raw.InputData.parameters_repr line 126
  31. theorem OAI.BinaryMatching.Raw.InputData.parameters_poly line 130