-
Notifications
You must be signed in to change notification settings - Fork 3
/
_CoqProject
164 lines (127 loc) · 5.05 KB
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
-Q theories Complexity
-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/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/SubtermProperty.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/PSLCompat.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/M2MBounds.v
theories/TM/PrettyBounds/SpaceBounds.v
theories/TM/PrettyBounds/SizeBounds.v
theories/TM/PrettyBounds/BaseCodeSpace.v
theories/TM/PrettyBounds/UnfoldClosBounds.v