OAI/Probability/ThorpRouting/HighTail/Model.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThorpNine.HighTail.Thorp.Card line 11

   Also declared: ComparatorChallenges/ThorpRouting.lean:2007 (same declaration text).

2. def OAI.ThorpNine.HighTail.Thorp.switchFun line 13

   Also declared: ComparatorChallenges/ThorpRouting.lean:2009 (same declaration text).

3. theorem OAI.ThorpNine.HighTail.Thorp.switchFun_involutive line 16

   Also declared: ComparatorChallenges/ThorpRouting.lean:2012 (same declaration text).

4. def OAI.ThorpNine.HighTail.Thorp.pairSwitch line 25

   Also declared: ComparatorChallenges/ThorpRouting.lean:2021 (same declaration text).

5. def OAI.ThorpNine.HighTail.Thorp.Butterfly line 31

   Also declared: ComparatorChallenges/ThorpRouting.lean:2027 (same declaration text).

6. def OAI.ThorpNine.HighTail.Thorp.childLift line 35

   Also declared: ComparatorChallenges/ThorpRouting.lean:2031 (same declaration text).

7. def OAI.ThorpNine.HighTail.Thorp.butterflyPerm line 41

   Also declared: ComparatorChallenges/ThorpRouting.lean:2037 (same declaration text).

8. def OAI.ThorpNine.HighTail.Thorp.finiteMean line 45

   Also declared: ComparatorChallenges/ThorpRouting.lean:2041 (same declaration text).

9. def OAI.ThorpNine.HighTail.Thorp.SwitchIndex line 48

   Also declared: ComparatorChallenges/ThorpRouting.lean:2044 (same declaration text).

10. instance OAI.ThorpNine.HighTail.Thorp.(instance at line 52) line 52
11. instance OAI.ThorpNine.HighTail.Thorp.(instance at line 57) line 57
12. def OAI.ThorpNine.HighTail.Thorp.decodeButterfly line 62

    Also declared: ComparatorChallenges/ThorpRouting.lean:2058 (same declaration text).

13. def OAI.ThorpNine.HighTail.Thorp.orbitSet line 69

    Also declared: ComparatorChallenges/ThorpRouting.lean:2065 (same declaration text).

14. abbrev OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.SelectedCycle line 80

    Also declared: ComparatorChallenges/ThorpRouting.lean:2076 (same declaration text).

15. instance OAI.ThorpNine.HighTail.Thorp.RoutingNetwork.(instance at line 83) line 83
16. def OAI.ThorpNine.HighTail.Thorp.cardSplit line 92

    Also declared: ComparatorChallenges/ThorpRouting.lean:2088 (same declaration text).

17. def OAI.ThorpNine.HighTail.Thorp.assembleBits line 112

    Also declared: ComparatorChallenges/ThorpRouting.lean:2108 (same declaration text).

18. def OAI.ThorpNine.HighTail.Thorp.pairLayer line 123

    Also declared: ComparatorChallenges/ThorpRouting.lean:2119 (same declaration text).

19. def OAI.ThorpNine.HighTail.Thorp.coinStepEquiv line 137

    Also declared: ComparatorChallenges/ThorpRouting.lean:2133 (same declaration text).

20. def OAI.ThorpNine.HighTail.Thorp.headTailEquiv line 151

    Also declared: ComparatorChallenges/ThorpRouting.lean:2147 (same declaration text).

21. def OAI.ThorpNine.HighTail.Thorp.CycleColoring.alternatingPerm line 161

    Also declared: ComparatorChallenges/ThorpRouting.lean:2157 (same declaration text).

22. def OAI.ThorpNine.HighTail.Thorp.PairRouting.required line 174

    Also declared: ComparatorChallenges/ThorpRouting.lean:2170 (same declaration text).

23. def OAI.ThorpNine.HighTail.Thorp.PairRouting.Compatible line 176

    Also declared: ComparatorChallenges/ThorpRouting.lean:2172 (same declaration text).

24. def OAI.ThorpNine.HighTail.Thorp.PairRouting.colors line 179

    Also declared: ComparatorChallenges/ThorpRouting.lean:2175 (same declaration text).

25. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.required_colors line 183

    Also declared: ComparatorChallenges/ThorpRouting.lean:2179 (same declaration text).

26. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.colors_compatible line 189

    Also declared: ComparatorChallenges/ThorpRouting.lean:2185 (same declaration text).

27. lemma OAI.ThorpNine.HighTail.Thorp.PairRouting.Compatible.tail_injective line 194

    Also declared: ComparatorChallenges/ThorpRouting.lean:2190 (same declaration text).

28. def OAI.ThorpNine.HighTail.Thorp.PairRouting.childEmbedding line 205

    Also declared: ComparatorChallenges/ThorpRouting.lean:2201 (same declaration text).

29. def OAI.ThorpNine.HighTail.Thorp.PairRouting.labelSet line 208

    Also declared: ComparatorChallenges/ThorpRouting.lean:2204 (same declaration text).

30. def OAI.ThorpNine.HighTail.Thorp.PairRouting.alternatingProjection line 210

    Also declared: ComparatorChallenges/ThorpRouting.lean:2206 (same declaration text).

31. def OAI.ThorpNine.HighTail.Thorp.PairRouting.alternatingCycles line 212

    Also declared: ComparatorChallenges/ThorpRouting.lean:2208 (same declaration text).

32. def OAI.ThorpNine.HighTail.Thorp.PairRouting.switchedEmbedding line 216

    Also declared: ComparatorChallenges/ThorpRouting.lean:2212 (same declaration text).

33. abbrev OAI.ThorpNine.HighTail.Thorp.BenesCoins line 227

    Also declared: ComparatorChallenges/ThorpRouting.lean:2223 (same declaration text).

34. def OAI.ThorpNine.HighTail.Thorp.palindromePerm line 229

    Also declared: ComparatorChallenges/ThorpRouting.lean:2225 (same declaration text).

35. def OAI.ThorpNine.HighTail.Thorp.sandwichShuffle line 232

    Also declared: ComparatorChallenges/ThorpRouting.lean:2228 (same declaration text).

36. def OAI.ThorpNine.HighTail.Thorp.benesStepEquiv line 239

    Also declared: ComparatorChallenges/ThorpRouting.lean:2235 (same declaration text).

37. def OAI.ThorpNine.HighTail.Thorp.palindromeCost line 243

    Also declared: ComparatorChallenges/ThorpRouting.lean:2239 (same declaration text).

38. def OAI.ThorpNine.HighTail.Thorp.palindromeLowCost line 258

    Also declared: ComparatorChallenges/ThorpRouting.lean:2254 (same declaration text).

39. def OAI.ThorpNine.HighTail.Thorp.HighHeight.highCost line 276

    Also declared: ComparatorChallenges/ThorpRouting.lean:2272 (same declaration text).

40. def OAI.ThorpNine.HighTail.Thorp.HighHeight.MainStatement line 280

    Also declared: ComparatorChallenges/ThorpRouting.lean:2276 (same declaration text).