ComparatorChallenges/WitnessedChoice.lean

GitHub source file

57 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.WitnessedSeparation.Hereditary.HF line 13

    Distinct definitions of this name: OAI/Computability/WitnessedChoice/Model.lean:11 (same statement text; different proof or body). Qualify references as OAI.WitnessedSeparation.Hereditary.HF@path.

  2. def OAI.WitnessedSeparation.Hereditary.mk line 21

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:17 (same declaration text).

  3. def OAI.WitnessedSeparation.Hereditary.atom line 23

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:19 (same declaration text).

  4. def OAI.WitnessedSeparation.Hereditary.isSet line 25

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:24 (same declaration text).

  5. def OAI.WitnessedSeparation.Hereditary.rawElements line 28

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:27 (same declaration text).

  6. def OAI.WitnessedSeparation.Hereditary.elements line 32

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:61 (same declaration text).

  7. instance OAI.WitnessedSeparation.Hereditary.(instance at line 60) line 60
  8. def OAI.WitnessedSeparation.Hereditary.ofFinset line 62

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:93 (same declaration text).

  9. def OAI.WitnessedSeparation.Hereditary.rawRank' line 65

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:96 (same declaration text).

  10. def OAI.WitnessedSeparation.Hereditary.rawRank line 70

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:101 (same declaration text).

  11. def OAI.WitnessedSeparation.Hereditary.rank line 72

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:125 (same declaration text).

  12. def OAI.WitnessedSeparation.Hereditary.rawMap' line 95

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:161 (same declaration text).

  13. def OAI.WitnessedSeparation.Hereditary.rawMap line 100

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:166 (same declaration text).

  14. def OAI.WitnessedSeparation.Hereditary.map line 102

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:187 (same declaration text).

  15. instance OAI.WitnessedSeparation.Hereditary.(instance at line 122) line 122
  16. def OAI.WitnessedSeparation.Hereditary.singleton line 169

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:296 (same declaration text).

  17. def OAI.WitnessedSeparation.Hereditary.double line 171

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:298 (same declaration text).

  18. def OAI.WitnessedSeparation.Hereditary.pair line 173

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:300 (same declaration text).

  19. def OAI.WitnessedSeparation.Hereditary.ordinal line 175

    Distinct definitions of this name: OAI/Computability/WitnessedChoice/Model.lean:302 (different declaration text). Qualify references as OAI.WitnessedSeparation.Hereditary.ordinal@path.

  20. def OAI.WitnessedSeparation.Hereditary.closure line 181

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:333 (same declaration text).

  21. abbrev OAI.WitnessedSeparation.Scalar line 234

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:312 (same declaration text).

  22. inductive OAI.WitnessedSeparation.Symbol line 236

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:314 (same declaration text).

  23. structure OAI.WitnessedSeparation.Input line 240

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:318 (same declaration text).

  24. inductive OAI.WitnessedChoice.BGS.Term line 253
  25. def OAI.WitnessedChoice.dropFree line 275
  26. def OAI.WitnessedChoice.Term.free line 280
  27. def OAI.Term.wscCount line 298
  28. abbrev OAI.Result line 315

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:452 (same declaration text).

  29. def OAI.emptyHF line 317

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:454 (same declaration text).

  30. def OAI.TC line 319

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:456 (same declaration text).

  31. def OAI.unionHF line 321

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:458 (same declaration text).

  32. def OAI.uniqueHF line 323

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:460 (same declaration text).

  33. def OAI.cardHF line 326

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:463 (same declaration text).

  34. def OAI.inputHF line 328

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:465 (same declaration text).

  35. def OAI.lift₂ line 331

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:468 (same declaration text).

  36. def OAI.collect line 334

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:471 (same declaration text).

  37. def OAI.iterationLoop line 342

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:479 (same declaration text).

  38. def OAI.ordinaryIteration line 350

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:487 (same declaration text).

  39. def OAI.resource line 353

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:490 (same declaration text).

  40. def OAI.permutationGraph line 357

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:494 (same declaration text).

  41. def OAI.Automorphism line 360

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:497 (same declaration text).

  42. def OAI.ChoicePrefix line 363

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:500 (same declaration text).

  43. def OAI.StrictPrefix line 369

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:506 (same declaration text).

  44. def OAI.FirstPath line 371

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:508 (same declaration text).

  45. def OAI.FixesParameters line 375

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:512 (same declaration text).

  46. def OAI.WitnessesHistory line 378

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:515 (same declaration text).

  47. def OAI.GoodWSC line 387

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:524 (same declaration text).

  48. def OAI.witnessedIteration line 398

    Distinct definitions of this name: OAI/Computability/WitnessedChoice/Model.lean:535 (same statement text; different proof or body). Qualify references as OAI.witnessedIteration@path.

  49. def OAI.Term.eval line 408
  50. structure FiniteInput line 440

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:575 (same declaration text).

  51. structure Sentence line 447

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:582 (same declaration text).

  52. def Sentence.eval line 451

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:586 (same declaration text).

  53. def Sentence.isCPT line 454

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:589 (same declaration text).

  54. def Sentence.BooleanOnAllInputs line 456

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:591 (same declaration text).

  55. def Sentence.TrueModels line 459

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:594 (same declaration text).

  56. def MainStatement line 461

    Also declared: OAI/Computability/WitnessedChoice/Model.lean:596 (same declaration text).

  57. theorem WitnessedChoice.main sorry line 469