OAI/Combinatorics/ParityLifts/Model.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ParityWL.Bit line 11

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

2. abbrev OAI.ParityWL.MainPair line 12

   Also declared: ComparatorChallenges/ParityLifts.lean:12 (same declaration text).

3. abbrev OAI.ParityWL.Helper line 13

   Also declared: ComparatorChallenges/ParityLifts.lean:13 (same declaration text).

4. abbrev OAI.ParityWL.TemplateVertex line 15

   Also declared: ComparatorChallenges/ParityLifts.lean:15 (same declaration text).

5. structure OAI.ParityWL.ChoiceSystem line 17

   Also declared: ComparatorChallenges/ParityLifts.lean:17 (same declaration text).

6. def OAI.ParityWL.ChoiceSystem.Successful line 27

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

7. def OAI.ParityWL.ChoiceSystem.SizeAtMost line 31

   Also declared: ComparatorChallenges/ParityLifts.lean:31 (same declaration text).

8. def OAI.ParityWL.helperIncident line 34

   Also declared: ComparatorChallenges/ParityLifts.lean:34 (same declaration text).

9. def OAI.ParityWL.templateAdj line 37

   Also declared: ComparatorChallenges/ParityLifts.lean:37 (same declaration text).

10. def OAI.ParityWL.template line 43

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

11. abbrev OAI.ParityWL.BaseVertex line 52

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

12. def OAI.ParityWL.baseType line 55

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

13. inductive OAI.ParityWL.BaseArc line 59

    Also declared: ComparatorChallenges/ParityLifts.lean:59 (same declaration text).

14. def OAI.ParityWL.baseGraph line 70

    Also declared: ComparatorChallenges/ParityLifts.lean:70 (same declaration text).

15. def OAI.ParityWL.baseProjection line 73

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

16. def OAI.ParityWL.Tag line 92

    Also declared: ComparatorChallenges/ParityLifts.lean:92 (same declaration text).

17. instance OAI.ParityWL.tagFintype line 96

    Also declared: ComparatorChallenges/ParityLifts.lean:96 (same declaration text).

18. abbrev OAI.ParityWL.LiftVertex line 101

    Also declared: ComparatorChallenges/ParityLifts.lean:101 (same declaration text).

19. def OAI.ParityWL.liftGraph line 103

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

20. def OAI.ParityWL.starParity line 117

    Also declared: ComparatorChallenges/ParityLifts.lean:117 (same declaration text).

21. def OAI.ParityWL.zeroLift line 120

    Also declared: ComparatorChallenges/ParityLifts.lean:120 (same declaration text).

22. def OAI.ParityWL.starLift line 123

    Also declared: ComparatorChallenges/ParityLifts.lean:123 (same declaration text).

23. inductive OAI.ParityWL.Convention line 126

    Also declared: ComparatorChallenges/ParityLifts.lean:126 (same declaration text).

24. def OAI.ParityWL.bagParameter line 129

    Also declared: ComparatorChallenges/ParityLifts.lean:129 (same declaration text).

25. def OAI.ParityWL.detectionRound line 132

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

26. def OAI.ParityWL.orderFactor line 134

    Also declared: ComparatorChallenges/ParityLifts.lean:134 (same declaration text).

27. abbrev OAI.ParityWL.AtomicType line 137

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

28. def OAI.ParityWL.JointColor line 139

    Also declared: ComparatorChallenges/ParityLifts.lean:139 (same declaration text).

29. def OAI.ParityWL.SeparateColor line 143

    Also declared: ComparatorChallenges/ParityLifts.lean:143 (same declaration text).

30. def OAI.ParityWL.atomicType line 147

    Also declared: ComparatorChallenges/ParityLifts.lean:147 (same declaration text).

31. def OAI.ParityWL.jointColor line 152

    Also declared: ComparatorChallenges/ParityLifts.lean:152 (same declaration text).

32. def OAI.ParityWL.separateColor line 158

    Also declared: ComparatorChallenges/ParityLifts.lean:158 (same declaration text).

33. def OAI.ParityWL.sameHistogram line 164

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

34. def OAI.ParityWL.samePureHistogram line 172

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

35. def OAI.ParityWL.WLEquivalent line 182

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

36. def OAI.ParityWL.PureWLEquivalent line 186

    Also declared: ComparatorChallenges/ParityLifts.lean:186 (same declaration text).

37. def OAI.ParityWL.ParityReductionStatement line 190

    Also declared: ComparatorChallenges/ParityLifts.lean:190 (same declaration text).