OAI/Computability/PerfectCompleteness/Machines/
4531 declarations, 0 contain sorry, 0 declared as axioms; 139 files
Files
- AcceptanceMachine.lean 48 declarations
- AcceptanceStage.lean 23 declarations
- BinaryDualCoordinates.lean 28 declarations
- BinaryFormulaLemmas.lean 62 declarations
- BinaryGapReduction.lean 3 declarations
- BinaryHeaderMachine.lean 26 declarations
- BinaryInputReduction.lean 4 declarations
- BinaryLiteralMachine.lean 20 declarations
- BinaryNameCompare.lean 18 declarations
- BinaryNameMachine.lean 29 declarations
- BinaryNameSearch.lean 37 declarations
- BinaryOccurrenceRename.lean 17 declarations
- BinaryPairMachine.lean 32 declarations
- BinaryParsingLemmas.lean 24 declarations
- BinaryRankOneCount.lean 5 declarations
- BinaryRenameLoop.lean 46 declarations
- BinaryRenameMachine.lean 31 declarations
- BinaryRenameWords.lean 22 declarations
- BinaryTokenMachine.lean 45 declarations
- BinaryTotalInputMachine.lean 37 declarations
- BinaryValidatorMachine.lean 40 declarations
- BoundedExecution.lean 37 declarations
- CanonicalCoarseningEncoding.lean 18 declarations
- CanonicalDictionaryAppendMachine.lean 24 declarations
- CanonicalDictionaryMachine.lean 27 declarations
- CanonicalEndpointMachine.lean 14 declarations
- CanonicalKeyMachine.lean 35 declarations
- CanonicalKeyShapeMachineLemmas.lean 39 declarations
- CanonicalLabelEncoding.lean 8 declarations
- CellsMachine.lean 31 declarations
- CellsTokensAlignmentLemmas.lean 41 declarations
- CircuitBatchLemmas.lean 54 declarations
- CircuitEmission.lean 48 declarations
- CircuitEncodingLemmas.lean 30 declarations
- CircuitFinish.lean 39 declarations
- CircuitLemmas.lean 111 declarations
- CircuitProducerStagesLemmas.lean 80 declarations
- ClashMachine.lean 47 declarations
- ClashMachineFull.lean 38 declarations
- CleanRecordDecoderInput.lean 14 declarations
- ClockPreparation.lean 63 declarations
- CompletedEdgeMachine.lean 27 declarations
- Completeness.lean 4 declarations
- DescriptorKeyMachine.lean 15 declarations
- DescriptorProjectionMachine.lean 21 declarations
- DomainEncoding.lean 20 declarations
- EncodingLemmas.lean 27 declarations
- ExactTargetOdometer.lean 68 declarations
- ExactTargetOnlineEncoding.lean 9 declarations
- FiniteBlockMachineLemmas.lean 85 declarations
- FiniteConstraintMachine.lean 18 declarations
- FixedBinaryGapReduction.lean 1 declarations
- FixedStoppedNativeTape.lean 12 declarations
- FixedUnaryRepresentationMachine.lean 47 declarations
- ForestStage.lean 46 declarations
- HierarchicalLowerMatrixInput.lean 11 declarations
- InitializationControl.lean 17 declarations
- InitializationMachine.lean 39 declarations
- InitializationMachineAt.lean 39 declarations
- InitializationStageLemmas.lean 61 declarations
- InitializationTemplateLemmas.lean 56 declarations
- InputCellsMachineLemmas.lean 73 declarations
- InputFrame.lean 25 declarations
- KeyMetadataMachine.lean 35 declarations
- LocalCompletionMachineLemmas.lean 33 declarations
- LowerCutDecoderInput.lean 5 declarations
- LowerCutInstalledInput.lean 17 declarations
- LowerCutOwnInput.lean 10 declarations
- MachineCircuit.lean 14 declarations
- MetadataFreeTapeLemmas.lean 25 declarations
- NormalizationEmitMachine.lean 37 declarations
- NormalizationLoopMachine.lean 37 declarations
- NormalizationMachine.lean 29 declarations
- NormalizationReadMachine.lean 35 declarations
- NormalizedTargetMachine.lean 32 declarations
- NormalizedTargetProducer.lean 7 declarations
- NormalizedTargetTapeBound.lean 10 declarations
- OrClosure.lean 30 declarations
- OriginalWholeCutTape.lean 22 declarations
- OutputOrder.lean 4 declarations
- OwnInputAffineSliceLemmas.lean 32 declarations
- OwnInputHeavyBounds.lean 8 declarations
- OwnInputReferenceLemmas.lean 53 declarations
- PaddingCellsMachine.lean 33 declarations
- PayloadCellsAlignment.lean 5 declarations
- PayloadCellsMachine.lean 37 declarations
- PayloadPresenceMachine.lean 25 declarations
- PayloadRowsLoop.lean 26 declarations
- PositionLemmas.lean 54 declarations
- PostfixAlignment.lean 22 declarations
- PostfixBounds.lean 17 declarations
- PostfixMachine.lean 73 declarations
- PreprocessingMachineLemmas.lean 17 declarations
- ProducerArenaLemmas.lean 123 declarations
- ProducerBootstrapLemmas.lean 74 declarations
- ProducerInvariant.lean 55 declarations
- ProducerTimeLemmas.lean 89 declarations
- ScalarTapeCardinality.lean 6 declarations
- SignedDescriptorStageMachine.lean 21 declarations
- SignedRuntimeBounds.lean 13 declarations
- SignedTupleBodyMachine.lean 39 declarations
- SignedTupleCleanupMachineLemmas.lean 62 declarations
- SourceClauseCountMachine.lean 21 declarations
- SourceClauseLookupMachine.lean 29 declarations
- SourceClauseReaderMachineLemmas.lean 39 declarations
- SourceClauseSelectMachine.lean 24 declarations
- SourceCoordinateMachine.lean 20 declarations
- SourceOccurrenceIndexMachine.lean 16 declarations
- SourceOccurrenceLoopMachine.lean 32 declarations
- SourceOccurrenceMachine.lean 30 declarations
- SourceOccurrenceProducerLemmas.lean 40 declarations
- SourcePhysicalTapeFiber.lean 1 declarations
- SourcePhysicalTapeLaw.lean 21 declarations
- SourceTupleMachine.lean 29 declarations
- SourceTupleResetMachine.lean 21 declarations
- StatementCircuit.lean 77 declarations
- StoppedCleanOwnInputGeometry.lean 5 declarations
- StoppedOwnInputGeometry.lean 21 declarations
- TargetFinalizeMachine.lean 12 declarations
- TargetHeaderMachine.lean 20 declarations
- TargetTapeEnvelope.lean 5 declarations
- TermMachine.lean 71 declarations
- TransitionIteration.lean 24 declarations
- TransitionMachine.lean 56 declarations
- TransitionTemplate.lean 70 declarations
- TupleEnumerationMachine.lean 35 declarations
- TupleIndexMachine.lean 42 declarations
- TupleInitializationMachine.lean 48 declarations
- UnaryBlockCopyMachine.lean 30 declarations
- UnaryBlockSkipMachine.lean 18 declarations
- UnaryRepresentationMachine.lean 26 declarations
- ValidityComposition.lean 13 declarations
- ValidityMachine.lean 33 declarations
- VerifierCircuit.lean 50 declarations
- VerifierFront.lean 47 declarations
- WholeArrayInteriorOwnInputLaw.lean 15 declarations
- WholeArrayOwnInputLaw.lean 10 declarations
- WitnessCircuit.lean 39 declarations
- WitnessEncodingLemmas.lean 59 declarations