OAI/Computability/DegreeRigidity/Syntax/
665 declarations, 0 contain sorry, 0 declared as axioms; 87 files
Files
- AtomicCertificate.lean 9 declarations
- AtomicDecisionFormula.lean 16 declarations
- AtomicDefinability.lean 3 declarations
- AtomicEncoding.lean 9 declarations
- AtomicFormula.lean 18 declarations
- AtomicGraph.lean 3 declarations
- AtomicGraphCorrect.lean 5 declarations
- AtomicRequirements.lean 11 declarations
- AtomicTruth.lean 3 declarations
- BooleanEvaluationWitness.lean 14 declarations
- BooleanExpressionAssembly.lean 9 declarations
- BooleanExpressionCertificate.lean 9 declarations
- BooleanExpressionCoverage.lean 4 declarations
- BooleanExpressionSyntax.lean 13 declarations
- BooleanExpressionTruth.lean 13 declarations
- BooleanFilterReconstruction.lean 5 declarations
- BooleanProjection.lean 17 declarations
- BooleanTruthReading.lean 7 declarations
- BoundedAutomorphismOutput.lean 3 declarations
- BoundedCertificate.lean 6 declarations
- BoundedDecoding.lean 14 declarations
- BoundedDefinability.lean 25 declarations
- BoundedFormulaRename.lean 1 declarations
- BoundedHierarchyCertificates.lean 2 declarations
- BoundedOmegaGraph.lean 3 declarations
- BoundedRecursive.lean 4 declarations
- BoundedRelations.lean 14 declarations
- BoundedSeparationName.lean 1 declarations
- BoundedSetTheory.lean 29 declarations
- BoundedSupport.lean 6 declarations
- BoundedTruthRecursion.lean 17 declarations
- CertificateMatrix.lean 12 declarations
- CheckGraphConstruction.lean 8 declarations
- CheckedCode.lean 12 declarations
- CheckedDefSuccessor.lean 4 declarations
- CheckedHierarchySyntax.lean 5 declarations
- CheckedMembershipSeparation.lean 6 declarations
- DefinablePower.lean 13 declarations
- DefinableSubsetCertificates.lean 9 declarations
- DefinedOutputTailCone.lean 1 declarations
- DefinedPrefixRemoval.lean 3 declarations
- FiniteFragment.lean 15 declarations
- FiniteGraphSatisfaction.lean 7 declarations
- FiniteModelGraph.lean 6 declarations
- FiniteSatisfactionCertificate.lean 14 declarations
- FiniteTerm.lean 13 declarations
- FormulaIsomorphism.lean 3 declarations
- LevySigmaNormalization.lean 6 declarations
- LevySigmaSchemas.lean 5 declarations
- MembershipInterpretation.lean 2 declarations
- PiOneOneSatisfaction.lean 5 declarations
- PrimitivePredicateFormula.lean 3 declarations
- SatisfactionCertificateBound.lean 3 declarations
- SatisfactionRecursion.lean 7 declarations
- SatisfactionSystemCertificate.lean 4 declarations
- SentenceCode.lean 19 declarations
- SentenceCodeDefinability.lean 15 declarations
- SentenceCodeFamily.lean 14 declarations
- SentenceFamilyFormula.lean 7 declarations
- SentenceInlining.lean 6 declarations
- SentenceSupportCertificate.lean 11 declarations
- SentenceSupportFormula.lean 9 declarations
- SetRankCertificate.lean 7 declarations
- SetSatisfactionBounded.lean 6 declarations
- SigmaBoundedUniversal.lean 7 declarations
- SigmaCollection.lean 5 declarations
- SigmaCollectionClosure.lean 1 declarations
- SigmaDefinability.lean 2 declarations
- SigmaDisjunction.lean 6 declarations
- SigmaDomainCollection.lean 4 declarations
- SigmaHull.lean 9 declarations
- SigmaInterpretation.lean 6 declarations
- SigmaParameterized.lean 5 declarations
- SigmaParameterizedClosure.lean 5 declarations
- SigmaSeparationName.lean 2 declarations
- SigmaSequenceTrace.lean 4 declarations
- SigmaSyntax.lean 9 declarations
- SigmaTransitiveWitness.lean 2 declarations
- TermCertificate.lean 3 declarations
- TermEvaluationGraph.lean 4 declarations
- TermFormula.lean 10 declarations
- TermFunctionality.lean 4 declarations
- VariableCertificateBounds.lean 9 declarations
- VariableTruthSyntax.lean 10 declarations
- WeakCheckedMembership.lean 2 declarations
- WeakCheckedValue.lean 2 declarations
- WeakExtensionContext.lean 1 declarations