OAI/ModelTheory/Choiceless/Model.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CPTSeparation.Scalar line 11

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

2. inductive OAI.CPTSeparation.Symbol line 13

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

3. structure OAI.CPTSeparation.Input line 17

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

4. abbrev OAI.CPTSeparation.Input.Edge line 24

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

5. abbrev OAI.CPTSeparation.Input.Config line 26

   Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:26 (same declaration text).

6. instance OAI.CPTSeparation.Input.(instance at line 28) line 28
7. instance OAI.CPTSeparation.Input.(instance at line 30) line 30
8. def OAI.CPTSeparation.Input.coefficient line 32

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

9. def OAI.CPTSeparation.Input.incident line 37

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

10. def OAI.CPTSeparation.Input.normalized line 41

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:41 (same declaration text).

11. def OAI.CPTSeparation.Input.consistent line 44

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:44 (same declaration text).

12. def OAI.CPTSeparation.Input.query line 48

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:48 (same declaration text).

13. structure OAI.CPTSeparation.Input.Iso line 51

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:51 (same declaration text).

14. abbrev OAI.CPTSeparation.Hereditary.HF line 62

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:60 (same declaration text).

15. def OAI.CPTSeparation.Hereditary.mk line 68

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:66 (same declaration text).

16. def OAI.CPTSeparation.Hereditary.atom line 70

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

17. theorem OAI.CPTSeparation.Hereditary.mk_eq_mk line 72
18. def OAI.CPTSeparation.Hereditary.isSet line 75

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

19. def OAI.CPTSeparation.Hereditary.rawElements line 78

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

20. theorem OAI.CPTSeparation.Hereditary.mem_rawElements line 82
21. theorem OAI.CPTSeparation.Hereditary.raw_mem_congr_right line 96
22. theorem OAI.CPTSeparation.Hereditary.rawElements_congr line 103
23. def OAI.CPTSeparation.Hereditary.elements line 112

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:77 (same declaration text).

24. instance OAI.CPTSeparation.Hereditary.(instance at line 140) line 140
25. theorem OAI.CPTSeparation.Hereditary.mem_mk line 142
26. def OAI.CPTSeparation.Hereditary.ofFinset line 144

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:107 (same declaration text).

27. def OAI.CPTSeparation.Hereditary.rawRank' line 147

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:110 (same declaration text).

28. def OAI.CPTSeparation.Hereditary.rawRank line 152

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

29. theorem OAI.CPTSeparation.Hereditary.rawRank_lt_of_mem line 154
30. theorem OAI.CPTSeparation.Hereditary.rawRank_congr line 164
31. def OAI.CPTSeparation.Hereditary.rank line 176

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

32. theorem OAI.CPTSeparation.Hereditary.rank_lt_of_mem line 199
33. def OAI.CPTSeparation.Hereditary.double line 218

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:146 (same declaration text).

34. def OAI.CPTSeparation.Hereditary.ordinal line 220

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:148 (same declaration text).

35. abbrev OAI.CPTSeparation.Operational.empty line 234

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:162 (same declaration text).

36. abbrev OAI.CPTSeparation.Operational.truth line 236

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

37. def OAI.CPTSeparation.Operational.boolean line 238

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:166 (same declaration text).

38. def OAI.CPTSeparation.Operational.inputRelation line 240

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:168 (same declaration text).

39. def OAI.CPTSeparation.Operational.allAtoms line 243

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

40. def OAI.CPTSeparation.Operational.unionHF line 245

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

41. def OAI.CPTSeparation.Operational.uniqueHF line 247

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:175 (same declaration text).

42. def OAI.CPTSeparation.Operational.cardinalityHF line 250

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:178 (same declaration text).

43. abbrev OAI.CPTSeparation.Operational.Location line 252

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:180 (same declaration text).

44. structure OAI.CPTSeparation.Operational.State line 254

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

45. def OAI.CPTSeparation.Operational.State.initial line 260

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:188 (same declaration text).

46. def OAI.CPTSeparation.Operational.State.support line 262

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

47. abbrev OAI.CPTSeparation.Operational.Update line 266

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:194 (same declaration text).

48. def OAI.CPTSeparation.Operational.State.Consistent line 270

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:196 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.Consistent@path.

49. def OAI.CPTSeparation.Operational.State.updatedValue line 273

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:199 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.updatedValue@path.

50. def OAI.CPTSeparation.Operational.State.applyUpdates line 277

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:203 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.applyUpdates@path.

51. inductive OAI.CPTSeparation.Operational.Control line 289

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:213 (same declaration text).

52. def OAI.CPTSeparation.Hereditary.closure line 301

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:225 (different declaration text). Qualify references as OAI.CPTSeparation.Hereditary.closure@path.

53. def OAI.CPTSeparation.Hereditary.familyClosure line 352

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:276 (different declaration text). Qualify references as OAI.CPTSeparation.Hereditary.familyClosure@path.

54. def OAI.CPTSeparation.Operational.State.critical line 366

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:288 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.critical@path.

55. def OAI.CPTSeparation.Operational.State.active line 369

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:291 (different declaration text). Qualify references as OAI.CPTSeparation.Operational.State.active@path.

56. inductive OAI.CPTSeparation.FullCPT.Term line 386

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:306 (same declaration text).

57. def OAI.CPTSeparation.FullCPT.Term.eval line 411

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

58. inductive OAI.CPTSeparation.FullCPT.Rule line 436

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:356 (same declaration text).

59. def OAI.CPTSeparation.FullCPT.Rule.updates line 446

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:366 (same declaration text).

60. structure OAI.CPTSeparation.FullCPT.Program line 458

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

61. abbrev OAI.CPTSeparation.FullCPT.Program.functionArity line 468

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:388 (same declaration text).

62. abbrev OAI.CPTSeparation.FullCPT.Program.Store line 470

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:390 (same declaration text).

63. def OAI.CPTSeparation.FullCPT.Program.flag line 472

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:392 (same declaration text).

64. def OAI.CPTSeparation.FullCPT.Program.step line 474

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:394 (same declaration text).

65. def OAI.CPTSeparation.FullCPT.Program.run line 479

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:399 (same declaration text).

66. def OAI.CPTSeparation.FullCPT.Program.active line 483

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:403 (same declaration text).

67. def OAI.CPTSeparation.FullCPT.Term.roots line 502

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:422 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Term.roots@path.

68. def OAI.CPTSeparation.FullCPT.Rule.roots line 526

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:440 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Rule.roots@path.

69. def OAI.CPTSeparation.FullCPT.Program.stepRoots line 545

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:459 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Program.stepRoots@path.

70. def OAI.CPTSeparation.FullCPT.Program.occurring line 548

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:462 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Program.occurring@path.

71. def OAI.CPTSeparation.FullCPT.Program.evaluationAccepts line 553

    Distinct definitions of this name: ComparatorChallenges/ChoicelessPolynomialTime.lean:467 (different declaration text). Qualify references as OAI.CPTSeparation.FullCPT.Program.evaluationAccepts@path.

72. def OAI.CPTSeparation.FullCPT.EvaluationDefinable line 559

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:473 (same declaration text).

73. abbrev OAI.CPTSeparation.OrderedQuery.Data line 573

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:487 (same declaration text).

74. def OAI.CPTSeparation.OrderedQuery.indexSymbol line 577

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:491 (same declaration text).

75. def OAI.CPTSeparation.OrderedQuery.cellValue line 586

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:500 (same declaration text).

76. def OAI.CPTSeparation.OrderedQuery.tableBits line 591

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:505 (same declaration text).

77. abbrev OAI.CPTSeparation.OrderedQuery.OrderedInput line 593

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:507 (same declaration text).

78. abbrev OAI.CPTSeparation.GaussMachine.Letter line 599

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:513 (same declaration text).

79. def OAI.CPTSeparation.GaussMachine.boolCode line 601

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:515 (same declaration text).

80. abbrev OAI.CPTSeparation.CounterLang.Letter line 607

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:521 (same declaration text).

81. def OAI.CPTSeparation.TableMachine.bitLetter line 615

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:529 (same declaration text).

82. def OAI.CPTSeparation.TableMachine.tableInput line 617

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:531 (same declaration text).

83. def OAI.CPTSeparation.TableMachine.code line 620

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:534 (same declaration text).

84. def OAI.CPTSeparation.Input.ordered line 627

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:539 (same declaration text).

85. def OAI.CPTSeparation.OrdinaryPolynomialTime line 630

    Also declared: ComparatorChallenges/ChoicelessPolynomialTime.lean:542 (same declaration text).