OAI/Computability/PerfectCompleteness/Reduction/
743 declarations, 0 contain sorry, 0 declared as axioms; 44 files
Files
- CanonicalGameLemmas.lean 58 declarations
- CanonicalNamedGame.lean 22 declarations
- CompletedOccurrenceOrder.lean 12 declarations
- CompletedVisitOrder.lean 12 declarations
- CompletionAlphabetLemmas.lean 32 declarations
- CompletionLemmas.lean 30 declarations
- CompletionOutputLemmas.lean 17 declarations
- CompletionSoundness.lean 33 declarations
- ExactPreliminaryTarget.lean 12 declarations
- FinitePreliminaryCompletion.lean 19 declarations
- FixedCallBudgetLemmas.lean 17 declarations
- FixedComparisonErrorsLemmas.lean 8 declarations
- FixedNativeHigh.lean 5 declarations
- FixedPhysicalStoppedComparison.lean 8 declarations
- FixedPreliminarySoundness.lean 1 declarations
- FixedQueryCodec.lean 36 declarations
- FixedRows.lean 11 declarations
- FixedSourcePhysicalHighLemmas.lean 6 declarations
- FixedStoppedActualBounds.lean 2 declarations
- FixedStoppedContradiction.lean 1 declarations
- FixedStoppedDirections.lean 15 declarations
- FixedStoppedError.lean 5 declarations
- FixedStoppedHighBound.lean 11 declarations
- FixedStoppedInverseBound.lean 18 declarations
- FixedStoppedMeetingEquality.lean 19 declarations
- FixedStoppedPair.lean 1 declarations
- FixedStoppedUsefulMass.lean 30 declarations
- FixedTarget.lean 8 declarations
- FixedTargetValue.lean 2 declarations
- HierarchicalFixedAdviceFamilyLemmas.lean 12 declarations
- NormalizedTarget.lean 23 declarations
- NormalizedTargetInitialization.lean 33 declarations
- OccurrenceGame.lean 27 declarations
- OddListGame.lean 8 declarations
- PreliminaryAveraging.lean 5 declarations
- PreliminaryLevelPair.lean 3 declarations
- PreliminaryOutputLemmas.lean 14 declarations
- SignedCompletionSchedule.lean 29 declarations
- SourceCompleteness.lean 17 declarations
- SourceGame.lean 29 declarations
- Target.lean 6 declarations
- TargetFinalizeBound.lean 5 declarations
- TargetGameLemmas.lean 73 declarations
- Value.lean 8 declarations