OAI/Combinatorics/FiniteCircle/Model.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.FiniteCircle.EditStep line 11

   Also declared: ComparatorChallenges/FiniteCircle.lean:11 (same declaration text).

2. inductive OAI.FiniteCircle.EditScript line 16

   Also declared: ComparatorChallenges/FiniteCircle.lean:16 (same declaration text).

3. def OAI.FiniteCircle.editDistance line 21

   Also declared: ComparatorChallenges/FiniteCircle.lean:21 (same declaration text).

4. def OAI.FiniteCircle.lcs line 24

   Also declared: ComparatorChallenges/FiniteCircle.lean:24 (same declaration text).

5. def OAI.FiniteCircle.deficit line 27

   Also declared: ComparatorChallenges/FiniteCircle.lean:27 (same declaration text).

6. abbrev OAI.FiniteCircle.Words line 29

   Also declared: ComparatorChallenges/FiniteCircle.lean:29 (same declaration text).

7. abbrev OAI.FiniteCircle.RealL1 line 30

   Also declared: ComparatorChallenges/FiniteCircle.lean:30 (same declaration text).

8. def OAI.FiniteCircle.distortion line 32

   Also declared: ComparatorChallenges/FiniteCircle.lean:32 (same declaration text).

9. def OAI.FiniteCircle.optimalDistortion line 39

   Also declared: ComparatorChallenges/FiniteCircle.lean:39 (same declaration text).

10. def OAI.FiniteCircle.E line 43

    Also declared: ComparatorChallenges/FiniteCircle.lean:43 (same declaration text).

11. def OAI.FiniteCircle.setDistortion line 46

    Also declared: ComparatorChallenges/FiniteCircle.lean:46 (same declaration text).

12. def OAI.FiniteCircle.alphabetSupremum line 49

    Also declared: ComparatorChallenges/FiniteCircle.lean:49 (same declaration text).

13. def OAI.FiniteCircle.exponentScale line 52

    Also declared: ComparatorChallenges/FiniteCircle.lean:52 (same declaration text).

14. def OAI.FiniteCircle.encode line 55

    Also declared: ComparatorChallenges/FiniteCircle.lean:55 (same declaration text).

15. def OAI.FiniteCircle.interval line 58

    Also declared: ComparatorChallenges/FiniteCircle.lean:58 (same declaration text).

16. def OAI.FiniteCircle.OffsetLocal line 62

    Also declared: ComparatorChallenges/FiniteCircle.lean:62 (same declaration text).

17. def OAI.FiniteCircle.indexSpan line 68

    Also declared: ComparatorChallenges/FiniteCircle.lean:68 (same declaration text).

18. def OAI.FiniteCircle.AnchorLocal line 73

    Also declared: ComparatorChallenges/FiniteCircle.lean:73 (same declaration text).

19. def OAI.FiniteCircle.SubstitutionBounds line 83

    Also declared: ComparatorChallenges/FiniteCircle.lean:83 (same declaration text).

20. def OAI.FiniteCircle.TwoCodes line 91

    Also declared: ComparatorChallenges/FiniteCircle.lean:91 (same declaration text).

21. def OAI.FiniteCircle.period line 98

    Also declared: ComparatorChallenges/FiniteCircle.lean:98 (same declaration text).

22. def OAI.FiniteCircle.circleSize line 100

    Also declared: ComparatorChallenges/FiniteCircle.lean:100 (same declaration text).

23. def OAI.FiniteCircle.MaskPrimes line 103

    Also declared: ComparatorChallenges/FiniteCircle.lean:103 (same declaration text).

24. def OAI.FiniteCircle.ExcludedPrimes line 108

    Also declared: ComparatorChallenges/FiniteCircle.lean:108 (same declaration text).

25. abbrev OAI.FiniteCircle.MaskTag line 113

    Also declared: ComparatorChallenges/FiniteCircle.lean:113 (same declaration text).

26. def OAI.FiniteCircle.maskTags line 115

    Also declared: ComparatorChallenges/FiniteCircle.lean:115 (same declaration text).

27. def OAI.FiniteCircle.MaskAlphabet line 118

    Also declared: ComparatorChallenges/FiniteCircle.lean:118 (same declaration text).

28. instance OAI.FiniteCircle.maskAlphabetFintype line 122

    Also declared: ComparatorChallenges/FiniteCircle.lean:122 (same declaration text).

29. def OAI.FiniteCircle.MaskState line 128

    Also declared: ComparatorChallenges/FiniteCircle.lean:128 (same declaration text).

30. def OAI.FiniteCircle.shiftMaskState line 132

    Also declared: ComparatorChallenges/FiniteCircle.lean:132 (same declaration text).

31. def OAI.FiniteCircle.maskGamma line 137

    Also declared: ComparatorChallenges/FiniteCircle.lean:137 (same declaration text).

32. def OAI.FiniteCircle.maskWord line 142

    Also declared: ComparatorChallenges/FiniteCircle.lean:142 (same declaration text).

33. def OAI.FiniteCircle.ExcludedAlphabet line 151

    Also declared: ComparatorChallenges/FiniteCircle.lean:151 (same declaration text).

34. instance OAI.FiniteCircle.excludedAlphabetFintype line 155

    Also declared: ComparatorChallenges/FiniteCircle.lean:155 (same declaration text).

35. def OAI.FiniteCircle.ExcludedState line 160

    Also declared: ComparatorChallenges/FiniteCircle.lean:160 (same declaration text).

36. def OAI.FiniteCircle.shiftExcludedState line 164

    Also declared: ComparatorChallenges/FiniteCircle.lean:164 (same declaration text).

37. def OAI.FiniteCircle.excludedTranslation line 169

    Also declared: ComparatorChallenges/FiniteCircle.lean:169 (same declaration text).

38. def OAI.FiniteCircle.excludedWord line 172

    Also declared: ComparatorChallenges/FiniteCircle.lean:172 (same declaration text).

39. def OAI.FiniteCircle.MaskWitness line 182

    Also declared: ComparatorChallenges/FiniteCircle.lean:182 (same declaration text).

40. def OAI.FiniteCircle.ExcludedWitness line 193

    Also declared: ComparatorChallenges/FiniteCircle.lean:193 (same declaration text).

41. def OAI.FiniteCircle.UniformUpper line 204

    Also declared: ComparatorChallenges/FiniteCircle.lean:204 (same declaration text).

42. def OAI.FiniteCircle.FullMain line 211

    Also declared: ComparatorChallenges/FiniteCircle.lean:211 (same declaration text).

43. def OAI.FiniteCircle.unequalDeficit line 223