blob: c5e195382965f18d4acce31f34a59380355fef4b (
plain)
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
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
|
(* Checks that constructor does not repeat the reduction of the conclusion *)
(* Expected time < 3.00s *)
(* Note: on i7 2.2GZ, time decreases from 85s to 0.1s *)
Inductive T : bool -> Prop :=
| C000 : T true | C001 : T true | C002 : T true | C003 : T true | C004 : T true
| C005 : T true | C006 : T true | C007 : T true | C008 : T true | C009 : T true
| C010 : T true | C011 : T true | C012 : T true | C013 : T true | C014 : T true
| C015 : T true | C016 : T true | C017 : T true | C018 : T true | C019 : T true
| C020 : T true | C021 : T true | C022 : T true | C023 : T true | C024 : T true
| C025 : T true | C026 : T true | C027 : T true | C028 : T true | C029 : T true
| C030 : T true | C031 : T true | C032 : T true | C033 : T true | C034 : T true
| C035 : T true | C036 : T true | C037 : T true | C038 : T true | C039 : T true
| C040 : T true | C041 : T true | C042 : T true | C043 : T true | C044 : T true
| C045 : T true | C046 : T true | C047 : T true | C048 : T true | C049 : T true
| C050 : T true | C051 : T true | C052 : T true | C053 : T true | C054 : T true
| C055 : T true | C056 : T true | C057 : T true | C058 : T true | C059 : T true
| C060 : T true | C061 : T true | C062 : T true | C063 : T true | C064 : T true
| C065 : T true | C066 : T true | C067 : T true | C068 : T true | C069 : T true
| C070 : T true | C071 : T true | C072 : T true | C073 : T true | C074 : T true
| C075 : T true | C076 : T true | C077 : T true | C078 : T true | C079 : T true
| C080 : T true | C081 : T true | C082 : T true | C083 : T true | C084 : T true
| C085 : T true | C086 : T true | C087 : T true | C088 : T true | C089 : T true
| C090 : T true | C091 : T true | C092 : T true | C093 : T true | C094 : T true
| C095 : T true | C096 : T true | C097 : T true | C098 : T true | C099 : T true
| C100 : T true | C101 : T true | C102 : T true | C103 : T true | C104 : T true
| C105 : T true | C106 : T true | C107 : T true | C108 : T true | C109 : T true
| C110 : T true | C111 : T true | C112 : T true | C113 : T true | C114 : T true
| C115 : T true | C116 : T true | C117 : T true | C118 : T true | C119 : T true
| C120 : T true | C121 : T true | C122 : T true | C123 : T true | C124 : T true
| C125 : T true | C126 : T true | C127 : T true | C128 : T true | C129 : T true
| C130 : T true | C131 : T true | C132 : T true | C133 : T true | C134 : T true
| C135 : T true | C136 : T true | C137 : T true | C138 : T true | C139 : T true
| C140 : T true | C141 : T true | C142 : T true | C143 : T true | C144 : T true
| C145 : T true | C146 : T true | C147 : T true | C148 : T true | C149 : T true
| C150 : T true | C151 : T true | C152 : T true | C153 : T true | C154 : T true
| C155 : T true | C156 : T true | C157 : T true | C158 : T true | C159 : T true
| C160 : T true | C161 : T true | C162 : T true | C163 : T true | C164 : T true
| C165 : T true | C166 : T true | C167 : T true | C168 : T true | C169 : T true
| C170 : T true | C171 : T true | C172 : T true | C173 : T true | C174 : T true
| C175 : T true | C176 : T true | C177 : T true | C178 : T true | C179 : T true
| C180 : T true | C181 : T true | C182 : T true | C183 : T true | C184 : T true
| C185 : T true | C186 : T true | C187 : T true | C188 : T true | C189 : T true
| C190 : T true | C191 : T true | C192 : T true | C193 : T true | C194 : T true
| C195 : T true | C196 : T true | C197 : T true | C198 : T true | C199 : T true
| C200 : T true | C201 : T true | C202 : T true | C203 : T true | C204 : T true
| C205 : T true | C206 : T true | C207 : T true | C208 : T true | C209 : T true
| C210 : T true | C211 : T true | C212 : T true | C213 : T true | C214 : T true
| C215 : T true | C216 : T true | C217 : T true | C218 : T true | C219 : T true
| C220 : T true | C221 : T true | C222 : T true | C223 : T true | C224 : T true
| C225 : T true | C226 : T true | C227 : T true | C228 : T true | C229 : T true
| C230 : T true | C231 : T true | C232 : T true | C233 : T true | C234 : T true
| C235 : T true | C236 : T true | C237 : T true | C238 : T true | C239 : T true
| C240 : T true | C241 : T true | C242 : T true | C243 : T true | C244 : T true
| C245 : T true | C246 : T true | C247 : T true | C248 : T true | C249 : T true
| C250 : T true | C251 : T true | C252 : T true | C253 : T true | C254 : T true
| C255 : T true | C256 : T true | C257 : T true | C258 : T true | C259 : T true
| C260 : T true | C261 : T true | C262 : T true | C263 : T true | C264 : T true
| C265 : T true | C266 : T true | C267 : T true | C268 : T true | C269 : T true
| C270 : T true | C271 : T true | C272 : T true | C273 : T true | C274 : T true
| C275 : T true | C276 : T true | C277 : T true | C278 : T true | C279 : T true
| C280 : T true | C281 : T true | C282 : T true | C283 : T true | C284 : T true
| C285 : T true | C286 : T true | C287 : T true | C288 : T true | C289 : T true
| C290 : T true | C291 : T true | C292 : T true | C293 : T true | C294 : T true
| C295 : T true | C296 : T true | C297 : T true | C298 : T true | C299 : T true
| C300 : T true | C301 : T true | C302 : T true | C303 : T true | C304 : T true
| C305 : T true | C306 : T true | C307 : T true | C308 : T true | C309 : T true
| C310 : T true | C311 : T true | C312 : T true | C313 : T true | C314 : T true
| C315 : T true | C316 : T true | C317 : T true | C318 : T true | C319 : T true
| C320 : T true | C321 : T true | C322 : T true | C323 : T true | C324 : T true
| C325 : T true | C326 : T true | C327 : T true | C328 : T true | C329 : T true
| C330 : T true | C331 : T true | C332 : T true | C333 : T true | C334 : T true
| C335 : T true | C336 : T true | C337 : T true | C338 : T true | C339 : T true
| C340 : T true | C341 : T true | C342 : T true | C343 : T true | C344 : T true
| C345 : T true | C346 : T true | C347 : T true | C348 : T true | C349 : T true
| C350 : T true | C351 : T true | C352 : T true | C353 : T true | C354 : T true
| C355 : T true | C356 : T true | C357 : T true | C358 : T true | C359 : T true
| C360 : T true | C361 : T true | C362 : T true | C363 : T true | C364 : T true
| C365 : T true | C366 : T true | C367 : T true | C368 : T true | C369 : T true
| C370 : T true | C371 : T true | C372 : T true | C373 : T true | C374 : T true
| C375 : T true | C376 : T true | C377 : T true | C378 : T true | C379 : T true
| C380 : T true | C381 : T true | C382 : T true | C383 : T true | C384 : T true
| C385 : T true | C386 : T true | C387 : T true | C388 : T true | C389 : T true
| C390 : T true | C391 : T true | C392 : T true | C393 : T true | C394 : T true
| C395 : T true | C396 : T true | C397 : T true | C398 : T true | C399 : T true
| C400 : T true | C401 : T true | C402 : T true | C403 : T true | C404 : T true
| C405 : T true | C406 : T true | C407 : T true | C408 : T true | C409 : T true
| C410 : T true | C411 : T true | C412 : T true | C413 : T true | C414 : T true
| C415 : T true | C416 : T true | C417 : T true | C418 : T true | C419 : T true
| C420 : T true | C421 : T true | C422 : T true | C423 : T true | C424 : T true
| C425 : T true | C426 : T true | C427 : T true | C428 : T true | C429 : T true
| C430 : T true | C431 : T true | C432 : T true | C433 : T true | C434 : T true
| C435 : T true | C436 : T true | C437 : T true | C438 : T true | C439 : T true
| C440 : T true | C441 : T true | C442 : T true | C443 : T true | C444 : T true
| C445 : T true | C446 : T true | C447 : T true | C448 : T true | C449 : T true
| C450 : T true | C451 : T true | C452 : T true | C453 : T true | C454 : T true
| C455 : T true | C456 : T true | C457 : T true | C458 : T true | C459 : T true
| C460 : T true | C461 : T true | C462 : T true | C463 : T true | C464 : T true
| C465 : T true | C466 : T true | C467 : T true | C468 : T true | C469 : T true
| C470 : T true | C471 : T true | C472 : T true | C473 : T true | C474 : T true
| C475 : T true | C476 : T true | C477 : T true | C478 : T true | C479 : T true
| C480 : T true | C481 : T true | C482 : T true | C483 : T true | C484 : T true
| C485 : T true | C486 : T true | C487 : T true | C488 : T true | C489 : T true
| C490 : T true | C491 : T true | C492 : T true | C493 : T true | C494 : T true
| C495 : T true | C496 : T true | C497 : T true | C498 : T true | C499 : T true
| C500 : T true | C501 : T true | C502 : T true | C503 : T true | C504 : T true
| C505 : T true | C506 : T true | C507 : T true | C508 : T true | C509 : T true
| C510 : T true | C511 : T true | C512 : T true | C513 : T true | C514 : T true
| C515 : T true | C516 : T true | C517 : T true | C518 : T true | C519 : T true
| C520 : T true | C521 : T true | C522 : T true | C523 : T true | C524 : T true
| C525 : T true | C526 : T true | C527 : T true | C528 : T true | C529 : T true
| C530 : T true | C531 : T true | C532 : T true | C533 : T true | C534 : T true
| C535 : T true | C536 : T true | C537 : T true | C538 : T true | C539 : T true
| C540 : T true | C541 : T true | C542 : T true | C543 : T true | C544 : T true
| C545 : T true | C546 : T true | C547 : T true | C548 : T true | C549 : T true
| C550 : T true | C551 : T true | C552 : T true | C553 : T true | C554 : T true
| C555 : T true | C556 : T true | C557 : T true | C558 : T true | C559 : T true
| C560 : T true | C561 : T true | C562 : T true | C563 : T true | C564 : T true
| C565 : T true | C566 : T true | C567 : T true | C568 : T true | C569 : T true
| C570 : T true | C571 : T true | C572 : T true | C573 : T true | C574 : T true
| C575 : T true | C576 : T true | C577 : T true | C578 : T true | C579 : T true
| C580 : T true | C581 : T true | C582 : T true | C583 : T true | C584 : T true
| C585 : T true | C586 : T true | C587 : T true | C588 : T true | C589 : T true
| C590 : T true | C591 : T true | C592 : T true | C593 : T true | C594 : T true
| C595 : T true | C596 : T true | C597 : T true | C598 : T true | C599 : T true
| C600 : T true | C601 : T true | C602 : T true | C603 : T true | C604 : T true
| C605 : T true | C606 : T true | C607 : T true | C608 : T true | C609 : T true
| C610 : T true | C611 : T true | C612 : T true | C613 : T true | C614 : T true
| C615 : T true | C616 : T true | C617 : T true | C618 : T true | C619 : T true
| C620 : T true | C621 : T true | C622 : T true | C623 : T true | C624 : T true
| C625 : T true | C626 : T true | C627 : T true | C628 : T true | C629 : T true
| C630 : T true | C631 : T true | C632 : T true | C633 : T true | C634 : T true
| C635 : T true | C636 : T true | C637 : T true | C638 : T true | C639 : T true
| C640 : T true | C641 : T true | C642 : T true | C643 : T true | C644 : T true
| C645 : T true | C646 : T true | C647 : T true | C648 : T true | C649 : T true
| C650 : T true | C651 : T true | C652 : T true | C653 : T true | C654 : T true
| C655 : T true | C656 : T true | C657 : T true | C658 : T true | C659 : T true
| C660 : T true | C661 : T true | C662 : T true | C663 : T true | C664 : T true
| C665 : T true | C666 : T true | C667 : T true | C668 : T true | C669 : T true
| C670 : T true | C671 : T true | C672 : T true | C673 : T true | C674 : T true
| C675 : T true | C676 : T true | C677 : T true | C678 : T true | C679 : T true
| C680 : T true | C681 : T true | C682 : T true | C683 : T true | C684 : T true
| C685 : T true | C686 : T true | C687 : T true | C688 : T true | C689 : T true
| C690 : T true | C691 : T true | C692 : T true | C693 : T true | C694 : T true
| C695 : T true | C696 : T true | C697 : T true | C698 : T true | C699 : T true
| C700 : T true | C701 : T true | C702 : T true | C703 : T true | C704 : T true
| C705 : T true | C706 : T true | C707 : T true | C708 : T true | C709 : T true
| C710 : T true | C711 : T true | C712 : T true | C713 : T true | C714 : T true
| C715 : T true | C716 : T true | C717 : T true | C718 : T true | C719 : T true
| C720 : T true | C721 : T true | C722 : T true | C723 : T true | C724 : T true
| C725 : T true | C726 : T true | C727 : T true | C728 : T true | C729 : T true
| C730 : T true | C731 : T true | C732 : T true | C733 : T true | C734 : T true
| C735 : T true | C736 : T true | C737 : T true | C738 : T true | C739 : T true
| C740 : T true | C741 : T true | C742 : T true | C743 : T true | C744 : T true
| C745 : T true | C746 : T true | C747 : T true | C748 : T true | C749 : T true
| C750 : T true | C751 : T true | C752 : T true | C753 : T true | C754 : T true
| C755 : T true | C756 : T true | C757 : T true | C758 : T true | C759 : T true
| C760 : T true | C761 : T true | C762 : T true | C763 : T true | C764 : T true
| C765 : T true | C766 : T true | C767 : T true | C768 : T true | C769 : T true
| C770 : T true | C771 : T true | C772 : T true | C773 : T true | C774 : T true
| C775 : T true | C776 : T true | C777 : T true | C778 : T true | C779 : T true
| C780 : T true | C781 : T true | C782 : T true | C783 : T true | C784 : T true
| C785 : T true | C786 : T true | C787 : T true | C788 : T true | C789 : T true
| C790 : T true | C791 : T true | C792 : T true | C793 : T true | C794 : T true
| C795 : T true | C796 : T true | C797 : T true | C798 : T true | C799 : T true
| C800 : T true | C801 : T true | C802 : T true | C803 : T true | C804 : T true
| C805 : T true | C806 : T true | C807 : T true | C808 : T true | C809 : T true
| C810 : T true | C811 : T true | C812 : T true | C813 : T true | C814 : T true
| C815 : T true | C816 : T true | C817 : T true | C818 : T true | C819 : T true
| C820 : T true | C821 : T true | C822 : T true | C823 : T true | C824 : T true
| C825 : T true | C826 : T true | C827 : T true | C828 : T true | C829 : T true
| C830 : T true | C831 : T true | C832 : T true | C833 : T true | C834 : T true
| C835 : T true | C836 : T true | C837 : T true | C838 : T true | C839 : T true
| C840 : T true | C841 : T true | C842 : T true | C843 : T true | C844 : T true
| C845 : T true | C846 : T true | C847 : T true | C848 : T true | C849 : T true
| C850 : T true | C851 : T true | C852 : T true | C853 : T true | C854 : T true
| C855 : T true | C856 : T true | C857 : T true | C858 : T true | C859 : T true
| C860 : T true | C861 : T true | C862 : T true | C863 : T true | C864 : T true
| C865 : T true | C866 : T true | C867 : T true | C868 : T true | C869 : T true
| C870 : T true | C871 : T true | C872 : T true | C873 : T true | C874 : T true
| C875 : T true | C876 : T true | C877 : T true | C878 : T true | C879 : T true
| C880 : T true | C881 : T true | C882 : T true | C883 : T true | C884 : T true
| C885 : T true | C886 : T true | C887 : T true | C888 : T true | C889 : T true
| C890 : T true | C891 : T true | C892 : T true | C893 : T true | C894 : T true
| C895 : T true | C896 : T true | C897 : T true | C898 : T true | C899 : T true
| C900 : T true | C901 : T true | C902 : T true | C903 : T true | C904 : T true
| C905 : T true | C906 : T true | C907 : T true | C908 : T true | C909 : T true
| C910 : T true | C911 : T true | C912 : T true | C913 : T true | C914 : T true
| C915 : T true | C916 : T true | C917 : T true | C918 : T true | C919 : T true
| C920 : T true | C921 : T true | C922 : T true | C923 : T true | C924 : T true
| C925 : T true | C926 : T true | C927 : T true | C928 : T true | C929 : T true
| C930 : T true | C931 : T true | C932 : T true | C933 : T true | C934 : T true
| C935 : T true | C936 : T true | C937 : T true | C938 : T true | C939 : T true
| C940 : T true | C941 : T true | C942 : T true | C943 : T true | C944 : T true
| C945 : T true | C946 : T true | C947 : T true | C948 : T true | C949 : T true
| C950 : T true | C951 : T true | C952 : T true | C953 : T true | C954 : T true
| C955 : T true | C956 : T true | C957 : T true | C958 : T true | C959 : T true
| C960 : T true | C961 : T true | C962 : T true | C963 : T true | C964 : T true
| C965 : T true | C966 : T true | C967 : T true | C968 : T true | C969 : T true
| C970 : T true | C971 : T true | C972 : T true | C973 : T true | C974 : T true
| C975 : T true | C976 : T true | C977 : T true | C978 : T true | C979 : T true
| C980 : T true | C981 : T true | C982 : T true | C983 : T true | C984 : T true
| C985 : T true | C986 : T true | C987 : T true | C988 : T true | C989 : T true
| C990 : T true | C991 : T true | C992 : T true | C993 : T true | C994 : T true
| C995 : T true | C996 : T true | C997 : T true | C998 : T true | C999 : T true
| C1000 : T false.
Fixpoint expand (n : nat) : Prop :=
match n with
| O => T false
| S n => expand n
end.
Example Expand : expand 2500.
Time constructor. (* ~0.45 secs *)
|
