-Q theories Complexity
-Q coq-library-undecidability/theories Undecidability

-arg -w -arg -notation-overridden
COQDOCFLAGS = "--charset utf-8 -s --with-header website/resources/header.html --with-footer website/resources/footer.html --index indexpage"

coq-library-undecidability/theories/L/L.v
coq-library-undecidability/theories/TM/TM.v
coq-library-undecidability/theories/TM/SBTM.v
coq-library-undecidability/theories/TM/L/Alphabets.v
coq-library-undecidability/theories/TM/L/CaseCom.v
coq-library-undecidability/theories/TM/L/HeapInterpreter/LookupTM.v
coq-library-undecidability/theories/TM/L/HeapInterpreter/StepTM.v
coq-library-undecidability/theories/TM/L/HeapInterpreter/M_LHeapInterpreter.v
coq-library-undecidability/theories/TM/L/HeapInterpreter/UnfoldClos.v
coq-library-undecidability/theories/TM/L/HeapInterpreter/JumpTargetTM.v
coq-library-undecidability/theories/TM/L/Transcode/Boollist_to_Enc.v
coq-library-undecidability/theories/TM/L/Transcode/Enc_to_Boollist.v
coq-library-undecidability/theories/TM/L/Transcode/BoollistEnc.v
coq-library-undecidability/theories/TM/L/Eval.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/Compiler_spec.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/LComp_to_TMComp.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/Compiler_facts.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/Compiler_nat_facts.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/EncBoolsTM_boolList.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/Compiler.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/NaryApp.v
coq-library-undecidability/theories/TM/L/CompilerBoolFuns/ClosedLAdmissible.v
coq-library-undecidability/theories/TM/Util/Prelim.v
coq-library-undecidability/theories/TM/Util/Relations.v
coq-library-undecidability/theories/TM/Util/ArithPrelim.v
coq-library-undecidability/theories/TM/Util/VectorPrelim.v
coq-library-undecidability/theories/TM/Util/TM_facts.v
coq-library-undecidability/theories/TM/Basic/Basic.v
coq-library-undecidability/theories/TM/Basic/Null.v
coq-library-undecidability/theories/TM/Basic/Mono.v
coq-library-undecidability/theories/TM/Basic/Duo.v
coq-library-undecidability/theories/TM/Combinators/Combinators.v
coq-library-undecidability/theories/TM/Combinators/Switch.v
coq-library-undecidability/theories/TM/Combinators/SequentialComposition.v
coq-library-undecidability/theories/TM/Combinators/If.v
coq-library-undecidability/theories/TM/Combinators/While.v
coq-library-undecidability/theories/TM/Combinators/StateWhile.v
coq-library-undecidability/theories/TM/Combinators/Mirror.v
coq-library-undecidability/theories/TM/Lifting/Lifting.v
coq-library-undecidability/theories/TM/Lifting/LiftTapes.v
coq-library-undecidability/theories/TM/Lifting/LiftAlphabet.v
coq-library-undecidability/theories/TM/Compound/TMTac.v
coq-library-undecidability/theories/TM/Compound/Multi.v
coq-library-undecidability/theories/TM/Compound/WriteString.v
coq-library-undecidability/theories/TM/Compound/MoveToSymbol.v
coq-library-undecidability/theories/TM/Compound/CopySymbols.v
coq-library-undecidability/theories/TM/Compound/Shift.v
coq-library-undecidability/theories/TM/Compound/Compare.v
coq-library-undecidability/theories/TM/Code/Code.v
coq-library-undecidability/theories/TM/Code/CodeTM.v
coq-library-undecidability/theories/TM/Code/WriteValue.v
coq-library-undecidability/theories/TM/Code/ChangeAlphabet.v
coq-library-undecidability/theories/TM/Code/Copy.v
coq-library-undecidability/theories/TM/Code/CompareValue.v
coq-library-undecidability/theories/TM/Code/ProgrammingTools.v
coq-library-undecidability/theories/TM/Code/CaseNat.v
coq-library-undecidability/theories/TM/Code/CaseSum.v
coq-library-undecidability/theories/TM/Code/CaseList.v
coq-library-undecidability/theories/TM/Code/CaseFin.v
coq-library-undecidability/theories/TM/Code/CasePair.v
coq-library-undecidability/theories/TM/Code/CaseBool.v
coq-library-undecidability/theories/TM/Code/NatTM.v
coq-library-undecidability/theories/TM/Code/NatSub.v
coq-library-undecidability/theories/TM/Code/ListTM.v
coq-library-undecidability/theories/TM/Code/List/App.v
coq-library-undecidability/theories/TM/Code/List/Concat_Repeat.v
coq-library-undecidability/theories/TM/Code/List/Cons_constant.v
coq-library-undecidability/theories/TM/Code/List/Length.v
coq-library-undecidability/theories/TM/Code/List/Nth.v
coq-library-undecidability/theories/TM/Code/List/Rev.v
coq-library-undecidability/theories/TM/Code/BinNumbers/EncodeBinNumbers.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosDefinitions.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosPointers.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosHelperMachines.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosIncrementTM.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosCompareTM.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosShiftTM.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosAddTM.v
coq-library-undecidability/theories/TM/Code/BinNumbers/PosMultTM.v
coq-library-undecidability/theories/TM/Code/BinNumbers/NTM.v
coq-library-undecidability/theories/TM/Single/EncodeTapes.v
coq-library-undecidability/theories/TM/Single/StepTM.v
coq-library-undecidability/theories/TM/Univ/LookupAssociativeListTM.v
coq-library-undecidability/theories/TM/Univ/LowLevel.v
coq-library-undecidability/theories/TM/Univ/Univ.v
coq-library-undecidability/theories/TM/PrettyBounds/MaxList.v
coq-library-undecidability/theories/TM/PrettyBounds/SizeBounds.v
coq-library-undecidability/theories/TM/Hoare/Hoare.v
coq-library-undecidability/theories/TM/Hoare/HoareLogic.v
coq-library-undecidability/theories/TM/Hoare/HoareCombinators.v
coq-library-undecidability/theories/TM/Hoare/HoareRegister.v
coq-library-undecidability/theories/TM/Hoare/HoareTactics.v
coq-library-undecidability/theories/TM/Hoare/HoareTacticsView.v
coq-library-undecidability/theories/TM/Hoare/HoareExamples.v
coq-library-undecidability/theories/TM/Hoare/HoareMult.v
coq-library-undecidability/theories/TM/Hoare/HoareStdLib.v
coq-library-undecidability/theories/TM/Hoare/HoareLegacy.v
coq-library-undecidability/theories/L/Prelim/MoreBase.v
coq-library-undecidability/theories/L/Prelim/ARS.v
coq-library-undecidability/theories/L/Prelim/StringBase.v
coq-library-undecidability/theories/L/Prelim/MoreList.v
coq-library-undecidability/theories/L/Prelim/LoopSum.v
coq-library-undecidability/theories/L/Util/L_facts.v
coq-library-undecidability/theories/L/Tactics/Computable.v
coq-library-undecidability/theories/L/Tactics/ComputableTime.v
coq-library-undecidability/theories/L/Tactics/LTactics.v
coq-library-undecidability/theories/L/Tactics/Extract.v
coq-library-undecidability/theories/L/Tactics/GenEncode.v
coq-library-undecidability/theories/L/Tactics/Lbeta_nonrefl.v
coq-library-undecidability/theories/L/Tactics/Lproc.v
coq-library-undecidability/theories/L/Tactics/Lbeta.v
coq-library-undecidability/theories/L/Tactics/Reflection.v
coq-library-undecidability/theories/L/Tactics/LClos.v
coq-library-undecidability/theories/L/Tactics/LClos_Eval.v
coq-library-undecidability/theories/L/Tactics/Lrewrite.v
coq-library-undecidability/theories/L/Tactics/Lsimpl.v
coq-library-undecidability/theories/L/Tactics/ComputableTactics.v
coq-library-undecidability/theories/L/Tactics/ComputableDemo.v
coq-library-undecidability/theories/L/Tactics/mixedTactics.v
coq-library-undecidability/theories/L/Datatypes/LUnit.v
coq-library-undecidability/theories/L/Datatypes/LBool.v
coq-library-undecidability/theories/L/Datatypes/List/List_basics.v
coq-library-undecidability/theories/L/Datatypes/List/List_enc.v
coq-library-undecidability/theories/L/Datatypes/List/List_eqb.v
coq-library-undecidability/theories/L/Datatypes/List/List_extra.v
coq-library-undecidability/theories/L/Datatypes/List/List_fold.v
coq-library-undecidability/theories/L/Datatypes/List/List_in.v
coq-library-undecidability/theories/L/Datatypes/List/List_nat.v
coq-library-undecidability/theories/L/Datatypes/Lists.v
coq-library-undecidability/theories/L/Datatypes/LNat.v
coq-library-undecidability/theories/L/Datatypes/LOptions.v
coq-library-undecidability/theories/L/Datatypes/LProd.v
coq-library-undecidability/theories/L/Datatypes/LSum.v
coq-library-undecidability/theories/L/Datatypes/LTerm.v
coq-library-undecidability/theories/L/Datatypes/LFinType.v
coq-library-undecidability/theories/L/Datatypes/LVector.v
coq-library-undecidability/theories/L/Functions/EqBool.v
coq-library-undecidability/theories/L/Functions/Equality.v
coq-library-undecidability/theories/L/Functions/Encoding.v
coq-library-undecidability/theories/L/Functions/Decoding.v
coq-library-undecidability/theories/L/Functions/Proc.v
coq-library-undecidability/theories/L/Functions/Size.v
coq-library-undecidability/theories/L/Functions/Subst.v
coq-library-undecidability/theories/L/Functions/Eval.v
coq-library-undecidability/theories/L/Functions/LoopSum.v
coq-library-undecidability/theories/L/Functions/UnboundIteration.v
coq-library-undecidability/theories/L/Functions/FinTypeLookup.v
coq-library-undecidability/theories/L/Functions/EnumInt.v
coq-library-undecidability/theories/L/Functions/Ackermann.v
coq-library-undecidability/theories/L/TM/TMEncoding.v
coq-library-undecidability/theories/L/TM/TMinL.v
coq-library-undecidability/theories/L/TM/TMinL/TMinL_extract.v
coq-library-undecidability/theories/L/TM/TapeFuns.v
coq-library-undecidability/theories/L/Complexity/UpToC.v
coq-library-undecidability/theories/L/Complexity/UpToCNary.v
coq-library-undecidability/theories/L/Complexity/GenericNary.v
coq-library-undecidability/theories/L/Complexity/ResourceMeasures.v
coq-library-undecidability/theories/L/Complexity/LinDecode/LTD_def.v
coq-library-undecidability/theories/L/Complexity/LinDecode/LTDnat.v
coq-library-undecidability/theories/L/Complexity/LinDecode/LTDlist.v
coq-library-undecidability/theories/L/Complexity/LinDecode/LTDbool.v
coq-library-undecidability/theories/L/AbstractMachines/LargestVar.v
coq-library-undecidability/theories/L/AbstractMachines/FlatPro/Programs.v
coq-library-undecidability/theories/L/AbstractMachines/FlatPro/ProgramsDef.v
coq-library-undecidability/theories/L/AbstractMachines/FlatPro/LM_heap_def.v
coq-library-undecidability/theories/L/AbstractMachines/FlatPro/LM_heap_correct.v
coq-library-undecidability/theories/L/AbstractMachines/FlatPro/UnfoldClos.v
coq-library-undecidability/theories/L/Computability/Acceptability.v
coq-library-undecidability/theories/L/Computability/Computability.v
coq-library-undecidability/theories/L/Computability/Decidability.v
coq-library-undecidability/theories/L/Computability/Enum.v
coq-library-undecidability/theories/L/Computability/Fixpoints.v
coq-library-undecidability/theories/L/Computability/MuRec.v
coq-library-undecidability/theories/L/Computability/Partial.v
coq-library-undecidability/theories/L/Computability/Por.v
coq-library-undecidability/theories/L/Computability/Rice.v
coq-library-undecidability/theories/L/Computability/Scott.v
coq-library-undecidability/theories/L/Computability/Seval.v
coq-library-undecidability/theories/L/Computability/Synthetic.v


coq-library-undecidability/theories/Shared/Dec.v
coq-library-undecidability/theories/Shared/ListAutomation.v
coq-library-undecidability/theories/Shared/FilterFacts.v
coq-library-undecidability/theories/Shared/embed_nat.v
coq-library-undecidability/theories/Shared/FinTypeEquiv.v
coq-library-undecidability/theories/Shared/FinTypeForallExists.v
coq-library-undecidability/theories/Synthetic/Definitions.v
coq-library-undecidability/theories/Synthetic/InformativeDefinitions.v
coq-library-undecidability/theories/Synthetic/Undecidability.v
coq-library-undecidability/theories/Synthetic/DecidabilityFacts.v
coq-library-undecidability/theories/Synthetic/SemiDecidabilityFacts.v
coq-library-undecidability/theories/Synthetic/EnumerabilityFacts.v
coq-library-undecidability/theories/Synthetic/ListEnumerabilityFacts.v
coq-library-undecidability/theories/Synthetic/MoreEnumerabilityFacts.v
coq-library-undecidability/theories/Synthetic/ReducibilityFacts.v
coq-library-undecidability/theories/Synthetic/InformativeReducibilityFacts.v
coq-library-undecidability/theories/Synthetic/Infinite.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/focus.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/utils_tac.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/list_focus.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/utils_list.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/utils_nat.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/utils_string.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/utils.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/sorting.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/utils_decidable.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/interval.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/list_bool.v       
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/sums.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/binomial.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/bool_list.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/bool_nat.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/gcd.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/prime.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/power_decomp.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/bounded_quantification.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/php.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/seteq.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/rel_iter.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/crt.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/fin_base.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/fin_dec.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/fin_choice.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/fin_bij.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/fin_upto.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/fin_quotient.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/finite.v
coq-library-undecidability/theories/Shared/Libs/DLW/Utils/quotient.v
coq-library-undecidability/theories/Shared/Libs/DLW/Vec/pos.v
coq-library-undecidability/theories/Shared/Libs/DLW/Vec/vec.v
coq-library-undecidability/theories/Shared/Libs/DLW/Wf/acc_irr.v
coq-library-undecidability/theories/Shared/Libs/DLW/Wf/measure_ind.v
coq-library-undecidability/theories/Shared/Libs/DLW/Wf/wf_chains.v
coq-library-undecidability/theories/Shared/Libs/DLW/Wf/wf_finite.v
coq-library-undecidability/theories/Shared/Libs/DLW/Wf/wf_incl.v
coq-library-undecidability/theories/Shared/Libs/DLW/Code/subcode.v
coq-library-undecidability/theories/Shared/Libs/DLW/Code/sss.v
coq-library-undecidability/theories/Shared/Libs/DLW/Code/compiler.v
coq-library-undecidability/theories/Shared/Libs/DLW/Code/compiler_correction.v
coq-library-undecidability/theories/Shared/Libs/PSL/Base.v
coq-library-undecidability/theories/Shared/Libs/PSL/Tactics/Tactics.v
coq-library-undecidability/theories/Shared/Libs/PSL/Tactics/AutoIndTac.v
coq-library-undecidability/theories/Shared/Libs/PSL/Prelim.v
coq-library-undecidability/theories/Shared/Libs/PSL/EqDec.v
coq-library-undecidability/theories/Shared/Libs/PSL/Numbers.v
coq-library-undecidability/theories/Shared/Libs/PSL/Bijection.v
coq-library-undecidability/theories/Shared/Libs/PSL/Retracts.v
coq-library-undecidability/theories/Shared/Libs/PSL/Inhabited.v
coq-library-undecidability/theories/Shared/Libs/PSL/FCI.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/BaseLists.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/Cardinality.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/Dupfree.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/Filter.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/Position.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/Power.v
coq-library-undecidability/theories/Shared/Libs/PSL/Lists/Removal.v
coq-library-undecidability/theories/Shared/Libs/PSL/Vectors/Fin.v
coq-library-undecidability/theories/Shared/Libs/PSL/Vectors/Vectors.v
coq-library-undecidability/theories/Shared/Libs/PSL/Vectors/FinNotation.v
coq-library-undecidability/theories/Shared/Libs/PSL/Vectors/VectorDupfree.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/BasicDefinitions.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/FinTypes.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/BasicFinTypes.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/CompoundFinTypes.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/FiniteFunction.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/Cardinality.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/DepPairs.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/Arbitrary.v
coq-library-undecidability/theories/Shared/Libs/PSL/FiniteTypes/VectorFin.v


theories/Complexity/Definitions.v
theories/Complexity/EncodableP.v
theories/Complexity/LinTimeDecodable.v
theories/Complexity/Monotonic.v
theories/Complexity/NP.v
theories/Complexity/ONotation.v
theories/Complexity/ONotationIsAppropriate.v
theories/Complexity/PolyTimeComputable.v
theories/Complexity/SpaceBoundsTime.v
theories/Complexity/Subtypes.v
theories/Complexity/UpToCPoly.v

theories/HierarchyTheorem/AbstractTimeHierarchyTheorem.v
theories/HierarchyTheorem/TimeHierarchyTheorem.v

theories/L/ComparisonTimeBoundDerivation.v


theories/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.v
theories/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.v
theories/L/AbstractMachines/AbstractSubstMachine.v
theories/L/AbstractMachines/AbstractHeapMachine.v
theories/L/AbstractMachines/AbstractHeapMachineDef.v
theories/L/AbstractMachines/UnfoldHeap.v
theories/L/AbstractMachines/FunctionalDefinitions.v
theories/L/AbstractMachines/LambdaDepth.v
theories/L/AbstractMachines/UnfoldTailRec.v
theories/L/AbstractMachines/Computable/Shared.v
theories/L/AbstractMachines/Computable/HeapMachine.v
theories/L/AbstractMachines/Computable/SubstMachine.v
theories/L/AbstractMachines/Computable/Unfolding.v
theories/L/AbstractMachines/Computable/Lookup.v
theories/L/AbstractMachines/Computable/UnivDecTime.v
theories/L/AbstractMachines/Computable/LargestVar.v
theories/L/AbstractMachines/Computable/EvalForTime.v
theories/L/AbstractMachines/Computable/EvalForTimeBool.v
theories/L/AbstractMachines/FlatPro/Computable/Compile.v
theories/L/AbstractMachines/FlatPro/Computable/Decompile.v
theories/L/AbstractMachines/FlatPro/SizeAnalysisStep.v
theories/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.v
#L/AbstractMachines/FlatPro/Computable/JumpTarget.v
#L/AbstractMachines/FlatPro/Computable/HeapStep.v
theories/L/AbstractMachines/FlatPro/Computable/LPro.v

theories/L/Datatypes/LBinNums.v
theories/L/Datatypes/LComparison.v
theories/L/Datatypes/LDepPair.v
theories/L/Functions/IterupN.v
theories/L/Functions/BinNums.v
theories/L/Functions/BinNumsAdd.v
theories/L/Functions/BinNumsSub.v
theories/L/Functions/BinNumsCompare.v

theories/L/TM/TMflat.v
theories/L/TM/CompCode.v
theories/L/TM/TMunflatten.v
theories/L/TM/TMflatEnc.v
theories/L/TM/TMflatFun.v
theories/L/TM/TMflatComp.v
theories/L/TM/TapeDecode.v
theories/L/TM/TMflatten.v



theories/Libs/Pigeonhole.v
theories/Libs/UniformHomomorphisms.v
theories/Libs/CookPrelim/PolyBounds.v
theories/Libs/CookPrelim/Tactics.v
theories/Libs/CookPrelim/MorePrelim.v
theories/Libs/CookPrelim/FlatFinTypes.v




theories/NP/Clique/Clique.v
theories/NP/Clique/FlatClique.v
theories/NP/Clique/FlatUGraph.v
theories/NP/Clique/kSAT_to_Clique.v
theories/NP/Clique/kSAT_to_FlatClique.v
theories/NP/Clique/UGraph.v

theories/NP/L/CanEnumTerm_def.v
theories/NP/L/CanEnumTerm.v
theories/NP/L/GenNP_is_hard.v
theories/NP/L/GenNP.v
theories/NP/L/GenNPBool.v
theories/NP/L/LMGenNP.v




theories/NP/SAT/CookLevin.v
theories/NP/SAT/SharedSAT.v
theories/NP/SAT/SAT.v
theories/NP/SAT/SAT_inNP.v
theories/NP/SAT/kSAT.v
theories/NP/SAT/kSAT_to_SAT.v

theories/NP/SAT/FSAT/FSAT.v
theories/NP/SAT/FSAT/FormulaEncoding.v
theories/NP/SAT/FSAT/FSAT_to_SAT.v

theories/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v
theories/NP/SAT/CookLevin/Reductions/PTCC_Preludes.v
theories/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v
theories/NP/SAT/CookLevin/Reductions/TCC_to_CC.v
theories/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v
theories/NP/SAT/CookLevin/Reductions/CC_homomorphisms.v
theories/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.v
theories/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v
theories/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.v
theories/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v

theories/NP/SAT/CookLevin/Subproblems/FlatCC.v
theories/NP/SAT/CookLevin/Subproblems/FlatTCC.v
theories/NP/SAT/CookLevin/Subproblems/BinaryCC.v
theories/NP/SAT/CookLevin/Subproblems/CC.v
theories/NP/SAT/CookLevin/Subproblems/TCC.v
theories/NP/SAT/CookLevin/Subproblems/TM_single.v
theories/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.v




theories/NP/TM/IntermediateProblems.v
theories/NP/TM/L_to_LM.v
theories/NP/TM/LM_to_mTM.v
theories/NP/TM/M_LM2TM.v
theories/NP/TM/M_multi2mono.v
theories/NP/TM/mTM_to_singleTapeTM.v
theories/NP/TM/TMGenNP_fixed_mTM.v
theories/NP/TM/TMGenNP.v






theories/TM/Compound/MoveToSymbol_niceSpec.v
theories/TM/Code/Decode.v
theories/TM/Code/DecodeList.v
theories/TM/Code/DecodeBool.v
theories/TM/Single/EncodeTapesInvariants.v
theories/TM/Single/DecodeTape.v
theories/TM/Single/DecodeTapes.v

# PrettyBounds
theories/TM/PrettyBounds/PrettyBounds.v
theories/TM/PrettyBounds/BaseCode.v
theories/TM/PrettyBounds/UnivBounds.v
theories/TM/PrettyBounds/M2MBounds.v

theories/TM/PrettyBounds/SpaceBounds.v
theories/TM/PrettyBounds/BaseCodeSpace.v
theories/TM/PrettyBounds/UnivSpaceBounds.v

# Multi-Univ Simulation Theorem
theories/TM/Univ/MultiUnivTimeSpaceSimulation.v