OAI/Computability/WitnessedChoice/Model.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

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

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

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

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

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

    Also declared: ComparatorChallenges/WitnessedChoice.lean:23 (same declaration text).

  4. theorem OAI.WitnessedSeparation.Hereditary.mk_eq_mk line 21
  5. def OAI.WitnessedSeparation.Hereditary.isSet line 24

    Also declared: ComparatorChallenges/WitnessedChoice.lean:25 (same declaration text).

  6. def OAI.WitnessedSeparation.Hereditary.rawElements line 27

    Also declared: ComparatorChallenges/WitnessedChoice.lean:28 (same declaration text).

  7. theorem OAI.WitnessedSeparation.Hereditary.mem_rawElements line 31
  8. theorem OAI.WitnessedSeparation.Hereditary.raw_mem_congr_right line 45
  9. theorem OAI.WitnessedSeparation.Hereditary.rawElements_congr line 52
  10. def OAI.WitnessedSeparation.Hereditary.elements line 61

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

  11. instance OAI.WitnessedSeparation.Hereditary.(instance at line 89) line 89
  12. theorem OAI.WitnessedSeparation.Hereditary.mem_mk line 91
  13. def OAI.WitnessedSeparation.Hereditary.ofFinset line 93

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

  14. def OAI.WitnessedSeparation.Hereditary.rawRank' line 96

    Also declared: ComparatorChallenges/WitnessedChoice.lean:65 (same declaration text).

  15. def OAI.WitnessedSeparation.Hereditary.rawRank line 101

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

  16. theorem OAI.WitnessedSeparation.Hereditary.rawRank_lt_of_mem line 103
  17. theorem OAI.WitnessedSeparation.Hereditary.rawRank_congr line 113
  18. def OAI.WitnessedSeparation.Hereditary.rank line 125

    Also declared: ComparatorChallenges/WitnessedChoice.lean:72 (same declaration text).

  19. theorem OAI.WitnessedSeparation.Hereditary.rank_lt_of_mem line 148
  20. def OAI.WitnessedSeparation.Hereditary.rawMap' line 161

    Also declared: ComparatorChallenges/WitnessedChoice.lean:95 (same declaration text).

  21. def OAI.WitnessedSeparation.Hereditary.rawMap line 166

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

  22. theorem OAI.WitnessedSeparation.Hereditary.toList_rawMap' line 168
  23. theorem OAI.WitnessedSeparation.Hereditary.rawMap_congr line 175
  24. def OAI.WitnessedSeparation.Hereditary.map line 187

    Also declared: ComparatorChallenges/WitnessedChoice.lean:102 (same declaration text).

  25. theorem OAI.WitnessedSeparation.Hereditary.map_mk line 207
  26. theorem OAI.WitnessedSeparation.Hereditary.rawMap_id line 209
  27. theorem OAI.WitnessedSeparation.Hereditary.map_id line 218
  28. theorem OAI.WitnessedSeparation.Hereditary.rawMap_comp line 224
  29. theorem OAI.WitnessedSeparation.Hereditary.map_comp line 234
  30. instance OAI.WitnessedSeparation.Hereditary.(instance at line 241) line 241
  31. def OAI.WitnessedSeparation.Hereditary.singleton line 296

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

  32. def OAI.WitnessedSeparation.Hereditary.double line 298

    Also declared: ComparatorChallenges/WitnessedChoice.lean:171 (same declaration text).

  33. def OAI.WitnessedSeparation.Hereditary.pair line 300

    Also declared: ComparatorChallenges/WitnessedChoice.lean:173 (same declaration text).

  34. def OAI.WitnessedSeparation.Hereditary.ordinal line 302

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

  35. abbrev OAI.WitnessedSeparation.Scalar line 312

    Also declared: ComparatorChallenges/WitnessedChoice.lean:234 (same declaration text).

  36. inductive OAI.WitnessedSeparation.Symbol line 314

    Also declared: ComparatorChallenges/WitnessedChoice.lean:236 (same declaration text).

  37. structure OAI.WitnessedSeparation.Input line 318

    Also declared: ComparatorChallenges/WitnessedChoice.lean:240 (same declaration text).

  38. def OAI.WitnessedSeparation.Hereditary.closure line 333

    Also declared: ComparatorChallenges/WitnessedChoice.lean:181 (same declaration text).

  39. def OAI.WitnessedChoice.BGS.dropFree line 416
  40. abbrev OAI.Result line 452

    Also declared: ComparatorChallenges/WitnessedChoice.lean:315 (same declaration text).

  41. def OAI.emptyHF line 454

    Also declared: ComparatorChallenges/WitnessedChoice.lean:317 (same declaration text).

  42. def OAI.TC line 456

    Also declared: ComparatorChallenges/WitnessedChoice.lean:319 (same declaration text).

  43. def OAI.unionHF line 458

    Also declared: ComparatorChallenges/WitnessedChoice.lean:321 (same declaration text).

  44. def OAI.uniqueHF line 460

    Also declared: ComparatorChallenges/WitnessedChoice.lean:323 (same declaration text).

  45. def OAI.cardHF line 463

    Also declared: ComparatorChallenges/WitnessedChoice.lean:326 (same declaration text).

  46. def OAI.inputHF line 465

    Also declared: ComparatorChallenges/WitnessedChoice.lean:328 (same declaration text).

  47. def OAI.lift₂ line 468

    Also declared: ComparatorChallenges/WitnessedChoice.lean:331 (same declaration text).

  48. def OAI.collect line 471

    Also declared: ComparatorChallenges/WitnessedChoice.lean:334 (same declaration text).

  49. def OAI.iterationLoop line 479

    Also declared: ComparatorChallenges/WitnessedChoice.lean:342 (same declaration text).

  50. def OAI.ordinaryIteration line 487

    Also declared: ComparatorChallenges/WitnessedChoice.lean:350 (same declaration text).

  51. def OAI.resource line 490

    Also declared: ComparatorChallenges/WitnessedChoice.lean:353 (same declaration text).

  52. def OAI.permutationGraph line 494

    Also declared: ComparatorChallenges/WitnessedChoice.lean:357 (same declaration text).

  53. def OAI.Automorphism line 497

    Also declared: ComparatorChallenges/WitnessedChoice.lean:360 (same declaration text).

  54. def OAI.ChoicePrefix line 500

    Also declared: ComparatorChallenges/WitnessedChoice.lean:363 (same declaration text).

  55. def OAI.StrictPrefix line 506

    Also declared: ComparatorChallenges/WitnessedChoice.lean:369 (same declaration text).

  56. def OAI.FirstPath line 508

    Also declared: ComparatorChallenges/WitnessedChoice.lean:371 (same declaration text).

  57. def OAI.FixesParameters line 512

    Also declared: ComparatorChallenges/WitnessedChoice.lean:375 (same declaration text).

  58. def OAI.WitnessesHistory line 515

    Also declared: ComparatorChallenges/WitnessedChoice.lean:378 (same declaration text).

  59. def OAI.GoodWSC line 524

    Also declared: ComparatorChallenges/WitnessedChoice.lean:387 (same declaration text).

  60. def OAI.witnessedIteration line 535

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

  61. structure FiniteInput line 575

    Also declared: ComparatorChallenges/WitnessedChoice.lean:440 (same declaration text).

  62. structure Sentence line 582

    Also declared: ComparatorChallenges/WitnessedChoice.lean:447 (same declaration text).

  63. def Sentence.eval line 586

    Also declared: ComparatorChallenges/WitnessedChoice.lean:451 (same declaration text).

  64. def Sentence.isCPT line 589

    Also declared: ComparatorChallenges/WitnessedChoice.lean:454 (same declaration text).

  65. def Sentence.BooleanOnAllInputs line 591

    Also declared: ComparatorChallenges/WitnessedChoice.lean:456 (same declaration text).

  66. def Sentence.TrueModels line 594

    Also declared: ComparatorChallenges/WitnessedChoice.lean:459 (same declaration text).

  67. def MainStatement line 596

    Also declared: ComparatorChallenges/WitnessedChoice.lean:461 (same declaration text).