-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"


theories/L/Complexity/CookLevin.v

theories/L/Complexity/bench.v


theories/L/Complexity/Problems/Cook/SingleTMGenNP.v
theories/L/Complexity/UpToCPoly.v
theories/L/Complexity/CookPrelim/PolyBounds.v
theories/L/Complexity/CookPrelim/Tactics.v
theories/L/Complexity/CookPrelim/MorePrelim.v
theories/L/Complexity/CookPrelim/FlatFinTypes.v

theories/L/Complexity/Problems/SharedSAT.v
theories/L/Complexity/Problems/SAT.v
theories/L/Complexity/Problems/kSAT.v
theories/L/Complexity/Reductions/kSAT_to_SAT.v

theories/L/Complexity/Problems/UGraph.v
theories/L/Complexity/Problems/Clique.v
theories/L/Complexity/Problems/FlatUGraph.v
theories/L/Complexity/Problems/FlatClique.v
theories/L/Complexity/Reductions/Pigeonhole.v
theories/L/Complexity/Reductions/kSAT_to_Clique.v
theories/L/Complexity/Reductions/kSAT_to_FlatClique.v



theories/L/Complexity/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v
theories/L/Complexity/Reductions/Cook/TM_single.v
theories/L/Complexity/Problems/Cook/CC.v
theories/L/Complexity/Problems/Cook/TCC.v
theories/L/Complexity/Reductions/Cook/PTCC_Preludes.v
theories/L/Complexity/Problems/Cook/FlatCC.v
theories/L/Complexity/Problems/Cook/FlatTCC.v
theories/L/Complexity/Problems/Cook/BinaryCC.v
theories/L/Complexity/Reductions/Cook/FlatSingleTMGenNP_to_FlatTCC.v
theories/L/Complexity/Reductions/Cook/TCC_to_CC.v
theories/L/Complexity/Reductions/Cook/FlatTCC_to_FlatCC.v

theories/L/Complexity/Reductions/Cook/UniformHomomorphisms.v
theories/L/Complexity/Reductions/Cook/CC_homomorphisms.v
theories/L/Complexity/Reductions/Cook/CC_to_BinaryCC.v
theories/L/Complexity/Reductions/Cook/FlatCC_to_BinaryCC.v


theories/L/Complexity/Problems/FSAT.v
theories/L/Complexity/Reductions/Cook/FormulaEncoding.v
theories/L/Complexity/Reductions/Cook/BinaryCC_to_FSAT.v
theories/L/Complexity/Reductions/FSAT_to_SAT.v

theories/L/AbstractMachines/TM_LHeapInterpreter/SizeAnalysis.v
theories/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.v
theories/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.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



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/L/Complexity/SpaceBoundsTime.v
theories/L/Complexity/Synthetic.v
theories/L/Complexity/PolyTimeComputable.v
theories/L/Complexity/AbstractTimeHierarchyTheorem.v
theories/L/Complexity/TimeHierarchyTheorem.v
theories/L/Complexity/Monotonic.v
theories/L/Complexity/ONotation.v
theories/L/Complexity/ONotationIsAppropriate.v
theories/L/Complexity/RegisteredP.v
theories/L/Complexity/LinTimeDecodable.v
theories/L/Complexity/NP.v
theories/L/Complexity/Problems/GenNP/CanEnumTerm_def.v
theories/L/Complexity/Problems/GenNP/CanEnumTerm.v
theories/L/Complexity/Problems/GenNP/GenNPBool.v
theories/L/Complexity/Problems/GenNP/GenNP.v
theories/L/Complexity/Problems/GenNP/GenNP_is_hard.v
theories/L/Complexity/Problems/GenNP/TMGenNP_fixed_mTM.v
theories/L/Complexity/Problems/GenNP/TMGenNP.v
theories/L/Complexity/Reductions/TMGenNP/L_to_LM.v
theories/L/Complexity/Reductions/TMGenNP/LM_to_mTM.v
theories/L/Complexity/Reductions/TMGenNP/mTM_to_singleTapeTM.v
theories/L/Complexity/Reductions/TMGenNP/M_multi2mono.v
theories/L/Complexity/Reductions/TMGenNP/M_LM2TM.v
theories/L/Complexity/Reductions/TMGenNP/IntermediateProblems.v
theories/L/Complexity/Reductions/TMGenNP/LMGenNP.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/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
#L/AbstractMachines/FlatPro/Computable/JumpTarget.v
#L/AbstractMachines/FlatPro/Computable/HeapStep.v
theories/L/AbstractMachines/FlatPro/Computable/LPro.v

theories/L/Complexity/Reductions/Cook/SingleTMGenNP_to_TCC.v