OAI/Computability/PerfectCompleteness/Foundations/
2942 declarations, 0 contain sorry, 0 declared as axioms; 137 files
Files
- CanonicalCoarseningErasure.lean 11 declarations
- CanonicalDictionaryNames.lean 12 declarations
- CanonicalDirections.lean 13 declarations
- CanonicalEdgesLemmas.lean 57 declarations
- CanonicalKeys.lean 18 declarations
- CanonicalPartialTable.lean 25 declarations
- CanonicalVertexNames.lean 20 declarations
- ClauseSupportLemmas.lean 66 declarations
- CommonAccuracy.lean 3 declarations
- CoordinateReplacementLemmas.lean 25 declarations
- CutCallExtension.lean 9 declarations
- CutContinuationAveraging.lean 7 declarations
- CutNativeForms.lean 27 declarations
- CutSlotAssembly.lean 5 declarations
- CutSlotOutside.lean 2 declarations
- CutTerminalSplit.lean 18 declarations
- CutTerminalZero.lean 5 declarations
- DependentPredictionDifferenceLemmas.lean 20 declarations
- DescriptorKeyTemplate.lean 15 declarations
- DesignatedLeavesLemmas.lean 17 declarations
- DualQuotientRowsLemmas.lean 44 declarations
- DummyEliminationLemmas.lean 49 declarations
- DummyEliminationWeighted.lean 14 declarations
- ExactConditionalOutput.lean 26 declarations
- ExtraCutCall.lean 18 declarations
- FiniteProduct.lean 11 declarations
- FiniteRangeInverse.lean 6 declarations
- GeometricPathLemmas.lean 17 declarations
- GeometricPrefixSplit.lean 16 declarations
- GlobalityLemmas.lean 85 declarations
- GoodAdviceEventsLemmas.lean 26 declarations
- HeterogeneousAdviceFamily.lean 11 declarations
- HeterogeneousPairAdvice.lean 14 declarations
- HierarchicalAdviceExperimentLemmas.lean 68 declarations
- HierarchicalAgreementMean.lean 12 declarations
- HierarchicalArrays.lean 27 declarations
- HierarchicalFrozenTablesLemmas.lean 70 declarations
- HierarchicalPairCoarse.lean 20 declarations
- HierarchicalPrediction.lean 11 declarations
- HierarchicalProjectedExperimentLemmas.lean 22 declarations
- HierarchicalProjectedPredictionLemmas.lean 39 declarations
- HierarchicalProjectedRawAverage.lean 17 declarations
- HierarchicalProjectedRawMeeting.lean 3 declarations
- HierarchicalProjectedSliceLemmas.lean 76 declarations
- HierarchicalRawAverage.lean 17 declarations
- HierarchicalRawPredictionLemmas.lean 27 declarations
- HierarchicalUsefulBackground.lean 3 declarations
- KeyFiniteness.lean 14 declarations
- LegalOutputLemmas.lean 6 declarations
- LegalRationalOutputLemmas.lean 2 declarations
- LinearEvaluationLemmas.lean 57 declarations
- ManyGoodRowsLemmas.lean 44 declarations
- MultiplicationFormInjectiveLemmas.lean 42 declarations
- NormalizationLemmas.lean 74 declarations
- OccurrenceStochasticLemmas.lean 12 declarations
- OddListAlphabetTransport.lean 3 declarations
- OddListExtraction.lean 25 declarations
- OddLists.lean 38 declarations
- OriginalBelowCut.lean 7 declarations
- OriginalExtraCutComparison.lean 7 declarations
- OriginalHiddenConditional.lean 1 declarations
- OriginalPrefixContinuation.lean 20 declarations
- OriginalTerminalSplitLemmas.lean 25 declarations
- OriginalWholeCut.lean 16 declarations
- OriginalWholeCutBridge.lean 12 declarations
- OriginalWholeCutComparison.lean 3 declarations
- OutputAnnihilator.lean 17 declarations
- PCPSource.lean 38 declarations
- PCPSourceHardness.lean 4 declarations
- PartialTableInverse.lean 17 declarations
- PartitionsLemmas.lean 108 declarations
- PrefixTests.lean 10 declarations
- ProjectedCallRestriction.lean 16 declarations
- ProjectedCardinality.lean 16 declarations
- ProjectedCutChoices.lean 14 declarations
- ProjectedFiberBackground.lean 11 declarations
- ProjectedFiberRawPair.lean 16 declarations
- ProjectedFiberSquare.lean 10 declarations
- ProjectedMeetingTransport.lean 2 declarations
- ProjectedPrefixComparison.lean 5 declarations
- ProjectedPrefixConditional.lean 1 declarations
- ProjectedWholeCut.lean 13 declarations
- QuarterBalanceLemmas.lean 31 declarations
- QuotientTableAgreementLemmas.lean 32 declarations
- RawOccurrenceOrderLemmas.lean 31 declarations
- RecursiveSpaceEquivLemmas.lean 89 declarations
- RecursiveSpaces.lean 27 declarations
- ReducedDomains.lean 12 declarations
- RetainedKeyTransport.lean 11 declarations
- SignedCostEnvelope.lean 15 declarations
- SignedScheduleIndex.lean 14 declarations
- SignedTupleLayout.lean 20 declarations
- SignedTupleSemantics.lean 23 declarations
- SlotProjectedExperiment.lean 40 declarations
- SourceClause.lean 32 declarations
- SourceKeyBoundsLemmas.lean 20 declarations
- SourceOddListsLemmas.lean 46 declarations
- SourcePhysicalCallExtension.lean 7 declarations
- SourcePhysicalExteriorReplay.lean 6 declarations
- SourcePhysicalExteriorSwap.lean 14 declarations
- SourcePhysicalSourceSwapLemmas.lean 19 declarations
- SourcePrefixComparison.lean 20 declarations
- SourceProjectedChoices.lean 16 declarations
- SourceProjectedTag.lean 13 declarations
- SourceProjectedWholeChoices.lean 8 declarations
- SourceStrategy.lean 7 declarations
- SourceTupleData.lean 17 declarations
- SourceTuplePlacement.lean 20 declarations
- SourceTupleResetPlacementLemmas.lean 24 declarations
- SourceVisitOrder.lean 9 declarations
- StoppedPathHead.lean 8 declarations
- StoppedPhysicalPrefixSwap.lean 2 declarations
- StoppedProjectedArrays.lean 9 declarations
- StoppedProjectedCoarseLemmas.lean 7 declarations
- StoppedProjectedContext.lean 11 declarations
- StoppedProjectedExperiment.lean 40 declarations
- StoppedProjectedOldRecord.lean 10 declarations
- StoppedProjectedPhysicalAdvice.lean 11 declarations
- StoppedProjectedUsefulAverage.lean 4 declarations
- StoppedProjectedUsefulEvent.lean 18 declarations
- StoppedSharedComparison.lean 5 declarations
- StoppedSharedEvents.lean 6 declarations
- TerminalCalls.lean 21 declarations
- TriangularFolding.lean 15 declarations
- TupleIndexEmitterLemmas.lean 72 declarations
- WholeArrayComposition.lean 15 declarations
- WholeArrayInteriorExteriorLemmas.lean 32 declarations
- WholeArrayPositiveSplit.lean 14 declarations
- WholeArrayRawAssembly.lean 9 declarations
- WholeArraySubtreeSplit.lean 21 declarations
- WholeCutCallsLemmas.lean 26 declarations
- WholeCutExteriorTransportLemmas.lean 18 declarations
- WholeCutGrouping.lean 11 declarations
- WholeCutReplayGroupingTransport.lean 16 declarations
- WholeCutReplayKeys.lean 14 declarations
- WholeCutReplayLemmas.lean 45 declarations
- WholeReplaySubtreeLemmas.lean 29 declarations