d:54 [in ImpParser]
E
eqb:205 [in Logic]eqb:210 [in Logic]
es:137 [in ImpParser]
es:82 [in ImpParser]
es:96 [in ImpParser]
evPO:103 [in IndPrinciples]
evPS:105 [in IndPrinciples]
e':127 [in ImpParser]
e':130 [in ImpParser]
e0:98 [in ImpParser]
e1:103 [in Imp]
e1:59 [in Imp]
e1:63 [in Imp]
e1:67 [in Imp]
e1:74 [in Imp]
e1:80 [in Imp]
e1:86 [in Imp]
e1:95 [in Imp]
e1:99 [in Imp]
e2:100 [in Imp]
e2:104 [in Imp]
e2:60 [in Imp]
e2:64 [in Imp]
e2:68 [in Imp]
e2:75 [in Imp]
e2:81 [in Imp]
e2:87 [in Imp]
e2:96 [in Imp]
e:115 [in ImpParser]
e:118 [in ImpParser]
e:124 [in ImpParser]
e:134 [in ImpParser]
E:14 [in ProofObjects]
e:154 [in ImpParser]
e:165 [in ImpParser]
e:177 [in ImpParser]
e:22 [in Tactics]
e:271 [in Imp]
e:278 [in Imp]
e:281 [in Imp]
e:32 [in Tactics]
e:38 [in Tactics]
e:72 [in ImpParser]
e:79 [in ImpParser]
e:86 [in ImpParser]
e:90 [in ImpParser]
e:93 [in ImpParser]
F
foo:49 [in Basics]f:114 [in Logic]
f:115 [in Poly]
f:119 [in Logic]
f:123 [in Tactics]
f:123 [in Basics]
f:135 [in Poly]
f:143 [in Poly]
f:147 [in Poly]
f:153 [in Poly]
f:158 [in Poly]
f:173 [in Poly]
f:174 [in Logic]
f:178 [in Poly]
f:184 [in Poly]
f:189 [in Poly]
f:195 [in Poly]
f:199 [in Poly]
f:202 [in Poly]
f:205 [in Poly]
f:23 [in Tactics]
f:33 [in Tactics]
f:39 [in Tactics]
f:41 [in IndPrinciples]
f:58 [in IndPrinciples]
f:69 [in Tactics]
f:7 [in Logic]
f:71 [in AltAuto]
f:78 [in AltAuto]
f:95 [in Lists]
G
g:175 [in Logic]g:42 [in IndPrinciples]
g:72 [in AltAuto]
g:79 [in AltAuto]
H
Heq:89 [in ProofObjects]Hm:70 [in IndProp]
Hm:77 [in IndPrinciples]
Hn:69 [in IndProp]
Hn:76 [in IndPrinciples]
HPQ:51 [in ProofObjects]
HPR:52 [in ProofObjects]
HP:42 [in ProofObjects]
HQR:53 [in ProofObjects]
Hrest:67 [in Rel]
Hxy:55 [in Rel]
Hxy:66 [in Rel]
Hyz:56 [in Rel]
H1:192 [in IndProp]
H1:197 [in IndProp]
H1:206 [in IndProp]
H1:78 [in Imp]
H1:84 [in Imp]
H1:90 [in Imp]
h1:94 [in ProofObjects]
H2:193 [in IndProp]
H2:201 [in IndProp]
H2:207 [in IndProp]
H2:79 [in Imp]
H2:85 [in Imp]
H2:91 [in Imp]
h2:95 [in ProofObjects]
H:11 [in ProofObjects]
H:140 [in IndProp]
H:144 [in IndProp]
H:148 [in IndProp]
H:152 [in IndProp]
H:27 [in ProofObjects]
H:299 [in IndProp]
H:300 [in IndProp]
H:4 [in ProofObjects]
H:41 [in IndProp]
H:50 [in Rel]
H:82 [in IndProp]
h:87 [in AltAuto]
H:88 [in IndPrinciples]
H:9 [in ProofObjects]
I
i1:34 [in ImpCEvalFun]i2:35 [in ImpCEvalFun]
i:130 [in Lists]
i:16 [in ImpCEvalFun]
i:174 [in ImpParser]
i:22 [in ImpCEvalFun]
i:33 [in ImpCEvalFun]
i:42 [in ImpCEvalFun]
i:46 [in ImpCEvalFun]
i:66 [in ImpParser]
i:8 [in ImpCEvalFun]
J
j:56 [in Tactics]j:65 [in Tactics]
K
k':57 [in IndProp]k':59 [in IndProp]
k:165 [in Poly]
k:188 [in Logic]
k:190 [in Logic]
L
lf:134 [in Tactics]lst1:21 [in AltAuto]
lst1:27 [in AltAuto]
lst1:30 [in AltAuto]
lst2:22 [in AltAuto]
lst2:28 [in AltAuto]
lst2:31 [in AltAuto]
lst:18 [in AltAuto]
lst:195 [in AltAuto]
lst:207 [in AltAuto]
lst:210 [in AltAuto]
lst:212 [in AltAuto]
lx:92 [in Poly]
ly:93 [in Poly]
l':125 [in Logic]
l':17 [in Tactics]
l1:118 [in Tactics]
l1:159 [in IndProp]
l1:162 [in IndProp]
l1:181 [in Logic]
l1:206 [in Logic]
l1:213 [in Logic]
l1:32 [in Lists]
l1:325 [in IndProp]
l1:341 [in IndProp]
l1:347 [in IndProp]
l1:35 [in IndProp]
l1:46 [in Lists]
l1:49 [in Poly]
l1:68 [in Lists]
l1:69 [in Poly]
l1:72 [in Poly]
l1:75 [in Lists]
l1:79 [in Lists]
l1:82 [in Lists]
l1:86 [in Lists]
l1:88 [in Lists]
l1:99 [in Lists]
l2:100 [in Lists]
l2:119 [in Tactics]
l2:160 [in IndProp]
l2:163 [in IndProp]
l2:182 [in Logic]
l2:207 [in Logic]
l2:214 [in Logic]
l2:326 [in IndProp]
l2:33 [in Lists]
l2:342 [in IndProp]
l2:348 [in IndProp]
l2:36 [in IndProp]
l2:47 [in Lists]
l2:50 [in Poly]
l2:69 [in Lists]
l2:70 [in Poly]
l2:73 [in Poly]
l2:76 [in Lists]
l2:80 [in Lists]
l2:83 [in Lists]
l2:87 [in Lists]
l2:89 [in Lists]
l3:161 [in IndProp]
l3:164 [in IndProp]
l3:37 [in IndProp]
l3:70 [in Lists]
l3:84 [in Lists]
l4:85 [in Lists]
l:101 [in Lists]
l:106 [in Poly]
l:107 [in Logic]
l:109 [in Lists]
l:112 [in Tactics]
l:112 [in Poly]
l:115 [in Logic]
l:117 [in Lists]
l:117 [in Tactics]
l:118 [in Lists]
l:120 [in Logic]
l:120 [in Poly]
l:124 [in Logic]
l:124 [in Poly]
l:125 [in Poly]
l:127 [in Poly]
l:128 [in Poly]
l:129 [in Logic]
l:131 [in Poly]
l:133 [in Tactics]
l:133 [in Logic]
l:136 [in Poly]
l:137 [in Tactics]
l:141 [in Tactics]
l:144 [in Poly]
l:145 [in Tactics]
l:148 [in Tactics]
l:148 [in Poly]
l:15 [in IndPrinciples]
l:158 [in IndProp]
l:159 [in Logic]
l:159 [in Poly]
l:16 [in Tactics]
l:160 [in Logic]
l:161 [in Logic]
l:162 [in Logic]
l:163 [in Logic]
l:164 [in Logic]
l:167 [in Poly]
l:170 [in Poly]
l:174 [in Poly]
l:18 [in IndPrinciples]
l:186 [in Logic]
l:19 [in IndPrinciples]
l:209 [in IndProp]
l:217 [in Logic]
l:22 [in IndPrinciples]
l:221 [in Logic]
l:24 [in Lists]
l:25 [in IndPrinciples]
l:267 [in IndProp]
l:273 [in IndProp]
l:29 [in Lists]
l:294 [in IndProp]
l:308 [in IndProp]
l:311 [in IndProp]
l:315 [in IndProp]
l:324 [in IndProp]
l:333 [in IndProp]
l:335 [in IndProp]
l:337 [in IndProp]
l:340 [in IndProp]
l:37 [in Lists]
l:39 [in Lists]
l:4 [in Poly]
l:41 [in Lists]
l:43 [in Lists]
l:45 [in Lists]
l:47 [in Poly]
l:54 [in Poly]
l:55 [in Tactics]
l:57 [in IndPrinciples]
l:58 [in Poly]
l:63 [in Poly]
l:64 [in Tactics]
l:65 [in Poly]
l:66 [in Lists]
l:67 [in Lists]
l:71 [in Lists]
l:74 [in Lists]
l:75 [in Poly]
l:77 [in Lists]
l:78 [in Lists]
l:81 [in Lists]
l:9 [in Poly]
l:91 [in Lists]
l:97 [in Tactics]
l:99 [in Poly]
M
m':76 [in Maps]m':81 [in Maps]
m:100 [in Tactics]
m:100 [in Logic]
m:100 [in IndProp]
m:102 [in Tactics]
m:102 [in IndProp]
m:102 [in AltAuto]
m:103 [in Logic]
m:105 [in Tactics]
m:105 [in AltAuto]
m:106 [in Tactics]
m:107 [in Tactics]
m:107 [in IndProp]
m:108 [in AltAuto]
m:109 [in IndProp]
m:11 [in Induction]
m:113 [in IndProp]
m:116 [in IndProp]
m:119 [in IndProp]
m:12 [in Maps]
m:120 [in Basics]
m:122 [in IndProp]
m:125 [in IndProp]
m:126 [in Tactics]
m:127 [in IndProp]
m:128 [in Tactics]
m:129 [in IndProp]
m:131 [in IndProp]
m:132 [in Lists]
m:132 [in Basics]
m:133 [in IndProp]
m:134 [in Basics]
m:134 [in AltAuto]
m:136 [in AltAuto]
m:137 [in IndProp]
m:139 [in AltAuto]
m:14 [in Logic]
m:141 [in IndProp]
m:145 [in IndProp]
m:145 [in AltAuto]
m:147 [in Logic]
m:149 [in IndProp]
m:15 [in Tactics]
m:153 [in IndProp]
m:155 [in AltAuto]
m:16 [in Lists]
m:16 [in Logic]
m:16 [in IndProp]
m:16 [in AltAuto]
m:162 [in AltAuto]
m:167 [in Logic]
m:18 [in Logic]
m:196 [in Logic]
m:2 [in Tactics]
m:2 [in Logic]
m:20 [in Logic]
m:20 [in Induction]
m:20 [in Maps]
m:214 [in AltAuto]
m:217 [in AltAuto]
m:218 [in Poly]
m:22 [in Logic]
m:22 [in Induction]
m:220 [in Poly]
m:220 [in AltAuto]
m:222 [in Poly]
m:222 [in AltAuto]
m:227 [in Logic]
m:23 [in Rel]
m:24 [in Poly]
m:24 [in Maps]
m:25 [in Rel]
m:26 [in Tactics]
m:26 [in Induction]
m:272 [in IndProp]
m:275 [in IndProp]
m:285 [in IndProp]
m:29 [in Maps]
m:292 [in IndProp]
m:3 [in Maps]
m:30 [in Induction]
m:306 [in IndProp]
m:33 [in Logic]
m:33 [in Induction]
m:33 [in AltAuto]
m:34 [in Auto]
m:34 [in Maps]
m:36 [in Rel]
m:36 [in Auto]
m:36 [in Induction]
m:37 [in Maps]
m:38 [in Logic]
m:38 [in Induction]
m:380 [in IndProp]
m:39 [in Imp]
m:39 [in Auto]
m:394 [in IndProp]
m:4 [in Tactics]
m:41 [in Tactics]
m:41 [in Induction]
m:45 [in Tactics]
m:45 [in Maps]
m:47 [in Tactics]
m:47 [in Imp]
m:49 [in Tactics]
m:5 [in Maps]
m:51 [in Imp]
m:51 [in Induction]
m:51 [in Maps]
m:53 [in Imp]
m:53 [in IndProp]
m:53 [in AltAuto]
m:54 [in Induction]
m:55 [in Maps]
m:57 [in Induction]
m:57 [in AltAuto]
m:58 [in Rel]
m:58 [in Tactics]
m:59 [in Basics]
m:60 [in Maps]
m:63 [in Basics]
m:63 [in Induction]
m:63 [in IndPrinciples]
m:64 [in IndProp]
m:64 [in AltAuto]
m:65 [in Induction]
m:65 [in Maps]
m:66 [in Poly]
m:66 [in IndPrinciples]
m:67 [in Basics]
m:67 [in AltAuto]
m:68 [in IndPrinciples]
m:68 [in IndProp]
m:69 [in Maps]
m:7 [in Induction]
m:73 [in Tactics]
m:73 [in IndProp]
m:75 [in Tactics]
m:75 [in IndPrinciples]
m:75 [in IndProp]
m:75 [in Maps]
m:77 [in Tactics]
m:77 [in Logic]
m:78 [in Basics]
m:8 [in Tactics]
m:80 [in Tactics]
m:80 [in Maps]
m:81 [in IndProp]
m:82 [in Logic]
m:83 [in IndPrinciples]
m:83 [in AltAuto]
m:84 [in Tactics]
m:84 [in Basics]
m:84 [in IndProp]
m:86 [in Tactics]
m:87 [in Logic]
m:87 [in IndPrinciples]
m:88 [in Tactics]
m:88 [in IndProp]
m:89 [in Basics]
m:9 [in Induction]
m:90 [in Tactics]
m:92 [in Tactics]
m:92 [in IndPrinciples]
m:92 [in IndProp]
m:93 [in IndProp]
m:94 [in Tactics]
m:96 [in Basics]
m:97 [in IndPrinciples]
m:98 [in Basics]
m:98 [in IndProp]
N
nb:42 [in Basics]ns:166 [in Logic]
n':111 [in Logic]
n':48 [in IndProp]
n0:58 [in IndProp]
n0:60 [in IndProp]
n0:94 [in IndPrinciples]
n0:98 [in IndPrinciples]
n1:101 [in Imp]
n1:105 [in Imp]
n1:105 [in IndProp]
n1:123 [in IndProp]
n1:131 [in Imp]
n1:135 [in Imp]
n1:139 [in Imp]
n1:143 [in Imp]
n1:161 [in Imp]
n1:165 [in Imp]
n1:169 [in Imp]
n1:192 [in Logic]
n1:3 [in Lists]
n1:61 [in Imp]
n1:65 [in Imp]
n1:69 [in Imp]
n1:76 [in Imp]
n1:82 [in Imp]
n1:85 [in ProofObjects]
n1:87 [in ProofObjects]
n1:88 [in Imp]
n1:91 [in ProofObjects]
n1:97 [in Lists]
n1:97 [in Imp]
n2:102 [in Imp]
n2:106 [in Imp]
n2:106 [in IndProp]
n2:124 [in IndProp]
n2:132 [in Imp]
n2:136 [in Imp]
n2:140 [in Imp]
n2:144 [in Imp]
n2:162 [in Imp]
n2:166 [in Imp]
n2:170 [in Imp]
n2:193 [in Logic]
n2:4 [in Lists]
n2:62 [in Imp]
n2:66 [in Imp]
n2:70 [in Imp]
n2:77 [in Imp]
n2:83 [in Imp]
n2:86 [in ProofObjects]
n2:88 [in ProofObjects]
n2:89 [in Imp]
n2:92 [in ProofObjects]
n2:98 [in Lists]
n2:98 [in Imp]
n3:145 [in Imp]
n:1 [in Tactics]
n:1 [in Logic]
n:1 [in Induction]
n:1 [in IndProp]
n:10 [in ProofObjects]
n:10 [in Induction]
n:10 [in IndProp]
n:10 [in AltAuto]
n:100 [in IndPrinciples]
n:101 [in IndPrinciples]
n:101 [in IndProp]
n:101 [in AltAuto]
n:102 [in Lists]
n:102 [in Logic]
n:103 [in Basics]
n:104 [in Basics]
n:104 [in IndPrinciples]
n:104 [in AltAuto]
n:106 [in IndPrinciples]
n:107 [in Poly]
n:107 [in AltAuto]
n:108 [in Lists]
n:108 [in Tactics]
n:108 [in Imp]
n:108 [in IndProp]
n:109 [in Tactics]
n:109 [in IndPrinciples]
n:11 [in AltAuto]
n:110 [in Lists]
n:110 [in Imp]
n:110 [in Logic]
n:111 [in IndPrinciples]
n:112 [in IndPrinciples]
n:112 [in IndProp]
n:115 [in Basics]
n:115 [in IndProp]
n:116 [in Poly]
n:117 [in ProofObjects]
n:117 [in Imp]
n:117 [in IndPrinciples]
n:118 [in Basics]
n:118 [in IndProp]
n:119 [in Basics]
n:12 [in ProofObjects]
n:12 [in Tactics]
n:12 [in AltAuto]
n:120 [in Tactics]
n:120 [in IndPrinciples]
n:121 [in Tactics]
n:121 [in IndProp]
n:122 [in Lists]
n:122 [in Tactics]
n:125 [in Tactics]
n:126 [in Poly]
n:126 [in IndProp]
n:127 [in Tactics]
n:128 [in Imp]
n:128 [in IndProp]
n:13 [in ProofObjects]
n:13 [in Tactics]
n:13 [in Logic]
n:13 [in Induction]
n:130 [in Basics]
n:130 [in IndProp]
n:131 [in Basics]
n:132 [in IndProp]
n:133 [in AltAuto]
n:135 [in AltAuto]
n:138 [in IndProp]
n:138 [in AltAuto]
n:139 [in Logic]
n:14 [in Tactics]
n:14 [in IndPrinciples]
n:14 [in IndProp]
n:140 [in Poly]
n:142 [in Logic]
n:142 [in IndProp]
n:144 [in AltAuto]
n:145 [in Logic]
n:146 [in Logic]
n:146 [in IndProp]
n:148 [in Imp]
n:15 [in ProofObjects]
n:15 [in Lists]
n:15 [in Logic]
n:15 [in IndProp]
n:15 [in AltAuto]
n:150 [in Poly]
n:150 [in IndProp]
n:154 [in IndProp]
n:157 [in Imp]
n:158 [in Imp]
n:16 [in ProofObjects]
n:16 [in Induction]
n:165 [in Logic]
n:167 [in IndProp]
n:168 [in Poly]
n:168 [in IndProp]
n:17 [in Logic]
n:17 [in Induction]
n:17 [in IndPrinciples]
n:171 [in IndProp]
n:172 [in IndProp]
n:173 [in Imp]
n:175 [in AltAuto]
n:176 [in AltAuto]
n:18 [in Induction]
n:180 [in AltAuto]
n:189 [in Logic]
n:19 [in Logic]
n:19 [in Induction]
n:191 [in Logic]
n:194 [in Logic]
n:195 [in Logic]
n:196 [in AltAuto]
n:2 [in ImpParser]
n:2 [in Induction]
n:2 [in IndPrinciples]
n:2 [in Maps]
n:21 [in Logic]
n:21 [in Induction]
n:213 [in AltAuto]
n:216 [in Poly]
n:216 [in AltAuto]
n:217 [in Poly]
n:219 [in Poly]
n:219 [in AltAuto]
n:22 [in Rel]
n:221 [in Poly]
n:221 [in AltAuto]
n:223 [in Imp]
n:226 [in Logic]
n:23 [in Lists]
n:23 [in IndPrinciples]
n:24 [in Rel]
n:25 [in Lists]
n:25 [in Tactics]
n:25 [in Induction]
n:253 [in Imp]
n:26 [in Rel]
n:26 [in IndPrinciples]
n:265 [in Imp]
n:266 [in IndProp]
n:27 [in IndPrinciples]
n:271 [in IndProp]
n:29 [in Induction]
n:293 [in IndProp]
n:3 [in ProofObjects]
n:3 [in Tactics]
n:3 [in Imp]
n:3 [in Logic]
n:3 [in Induction]
n:3 [in IndPrinciples]
n:305 [in IndProp]
n:307 [in IndProp]
n:310 [in IndProp]
n:314 [in IndProp]
n:32 [in Logic]
n:32 [in Induction]
n:32 [in AltAuto]
n:327 [in IndProp]
n:328 [in IndProp]
n:33 [in Auto]
n:35 [in Rel]
n:35 [in Imp]
n:35 [in Auto]
n:35 [in Induction]
n:36 [in Imp]
n:36 [in Logic]
n:37 [in Logic]
n:38 [in Auto]
n:39 [in Induction]
n:4 [in Logic]
n:4 [in ImpParser]
n:4 [in Induction]
n:4 [in IndPrinciples]
n:4 [in IndProp]
n:4 [in Maps]
n:40 [in Tactics]
n:40 [in Imp]
n:40 [in Induction]
n:40 [in IndProp]
n:42 [in IndProp]
n:43 [in Induction]
n:44 [in Tactics]
n:44 [in Induction]
n:45 [in IndPrinciples]
n:45 [in IndProp]
n:46 [in Tactics]
n:46 [in Basics]
n:46 [in Induction]
n:46 [in IndProp]
n:47 [in Induction]
n:47 [in IndProp]
n:48 [in Tactics]
n:48 [in Imp]
n:49 [in IndProp]
n:5 [in ProofObjects]
n:5 [in Induction]
n:5 [in IndPrinciples]
n:5 [in IndProp]
n:50 [in Basics]
n:50 [in Induction]
n:50 [in IndProp]
n:51 [in IndProp]
n:52 [in Imp]
n:52 [in Basics]
n:52 [in IndProp]
n:52 [in AltAuto]
n:53 [in ImpParser]
n:53 [in Induction]
n:54 [in Imp]
n:54 [in Basics]
n:55 [in Logic]
n:55 [in IndProp]
n:56 [in Induction]
n:56 [in IndProp]
n:56 [in AltAuto]
n:57 [in Rel]
n:57 [in Tactics]
n:57 [in Basics]
n:57 [in Logic]
n:58 [in Imp]
n:58 [in Basics]
n:59 [in Tactics]
n:59 [in IndPrinciples]
n:6 [in ProofObjects]
n:6 [in ImpParser]
n:6 [in Induction]
n:60 [in IndPrinciples]
n:60 [in AltAuto]
n:61 [in Induction]
n:61 [in IndPrinciples]
n:61 [in IndProp]
n:61 [in AltAuto]
n:62 [in Basics]
n:62 [in Induction]
n:62 [in IndPrinciples]
n:62 [in IndProp]
n:62 [in AltAuto]
n:63 [in IndProp]
n:63 [in AltAuto]
n:65 [in IndPrinciples]
n:65 [in AltAuto]
n:66 [in ProofObjects]
n:66 [in Tactics]
n:66 [in Basics]
n:66 [in AltAuto]
n:67 [in ProofObjects]
n:67 [in Poly]
n:67 [in IndPrinciples]
n:67 [in IndProp]
n:68 [in ProofObjects]
n:68 [in Induction]
n:69 [in ImpParser]
n:7 [in ProofObjects]
n:7 [in Tactics]
n:70 [in Induction]
n:70 [in IndPrinciples]
n:71 [in IndPrinciples]
n:71 [in IndProp]
n:72 [in Tactics]
n:72 [in Induction]
n:72 [in IndProp]
n:73 [in Imp]
n:74 [in Tactics]
n:74 [in IndPrinciples]
n:74 [in IndProp]
n:75 [in Basics]
n:76 [in Tactics]
n:76 [in Logic]
n:77 [in Basics]
n:78 [in IndPrinciples]
n:79 [in Tactics]
n:79 [in IndProp]
n:8 [in ProofObjects]
n:8 [in ImpParser]
n:8 [in Induction]
n:8 [in AltAuto]
n:80 [in IndProp]
n:81 [in Logic]
n:81 [in IndPrinciples]
n:82 [in IndPrinciples]
n:82 [in AltAuto]
n:83 [in Tactics]
n:83 [in Basics]
n:83 [in IndProp]
n:84 [in Auto]
n:84 [in IndPrinciples]
n:85 [in Tactics]
n:85 [in Logic]
n:86 [in Logic]
n:87 [in Tactics]
n:87 [in IndProp]
n:88 [in Basics]
n:89 [in Tactics]
n:9 [in Rel]
n:9 [in IndProp]
n:90 [in Basics]
n:90 [in IndPrinciples]
n:91 [in Tactics]
n:91 [in Basics]
n:91 [in IndPrinciples]
n:91 [in IndProp]
n:92 [in Basics]
n:93 [in Lists]
n:93 [in Tactics]
n:93 [in Basics]
n:93 [in IndPrinciples]
n:94 [in Imp]
n:94 [in Basics]
n:94 [in IndProp]
n:95 [in Tactics]
n:95 [in Basics]
n:95 [in IndPrinciples]
n:96 [in Lists]
n:96 [in IndProp]
n:97 [in Basics]
n:97 [in IndProp]
n:98 [in Tactics]
n:99 [in Tactics]
n:99 [in Logic]
n:99 [in IndProp]
O
o:103 [in AltAuto]o:115 [in Lists]
o:134 [in IndProp]
o:139 [in IndProp]
o:143 [in IndProp]
o:146 [in Lists]
o:147 [in IndProp]
o:151 [in IndProp]
o:155 [in IndProp]
o:27 [in Tactics]
o:42 [in Tactics]
o:49 [in Imp]
o:5 [in Tactics]
o:50 [in Tactics]
o:54 [in IndProp]
o:54 [in AltAuto]
o:58 [in AltAuto]
o:84 [in AltAuto]
o:88 [in Logic]
o:95 [in IndProp]
o:99 [in Basics]
P
pat:110 [in ImpParser]pat:113 [in ImpParser]
pat:116 [in ImpParser]
pat:119 [in ImpParser]
pat:122 [in ImpParser]
pat:125 [in ImpParser]
pat:128 [in ImpParser]
pat:131 [in ImpParser]
pat:135 [in ImpParser]
pat:138 [in ImpParser]
pat:152 [in ImpParser]
pat:155 [in ImpParser]
pat:158 [in ImpParser]
pat:161 [in ImpParser]
pat:163 [in ImpParser]
pat:166 [in ImpParser]
pat:169 [in ImpParser]
pat:172 [in ImpParser]
pat:175 [in ImpParser]
pat:178 [in ImpParser]
pat:182 [in ImpParser]
pat:185 [in ImpParser]
pat:67 [in ImpParser]
pat:70 [in ImpParser]
pat:73 [in ImpParser]
pat:76 [in ImpParser]
pat:80 [in ImpParser]
pat:83 [in ImpParser]
pat:87 [in ImpParser]
pat:91 [in ImpParser]
pat:94 [in ImpParser]
pat:97 [in ImpParser]
Peven:136 [in Logic]
Peven:138 [in Logic]
Peven:141 [in Logic]
Peven:144 [in Logic]
pf1:142 [in ProofObjects]
pf2:143 [in ProofObjects]
Podd:135 [in Logic]
Podd:137 [in Logic]
Podd:140 [in Logic]
Podd:143 [in Logic]
power:72 [in Basics]
prog:269 [in Imp]
PSS:116 [in IndPrinciples]
P0:114 [in IndPrinciples]
P1:115 [in IndPrinciples]
p1:274 [in Imp]
p2:275 [in Imp]
P:1 [in IndPrinciples]
p:100 [in Basics]
P:101 [in ProofObjects]
p:102 [in Basics]
P:102 [in IndPrinciples]
P:105 [in ProofObjects]
p:106 [in AltAuto]
P:109 [in ProofObjects]
P:109 [in AltAuto]
p:11 [in Lists]
p:11 [in Tactics]
P:11 [in Auto]
P:110 [in ProofObjects]
P:110 [in IndPrinciples]
p:110 [in IndProp]
P:112 [in ProofObjects]
P:112 [in AltAuto]
P:113 [in IndPrinciples]
p:114 [in IndProp]
P:115 [in AltAuto]
p:117 [in IndProp]
P:118 [in AltAuto]
P:119 [in ProofObjects]
p:12 [in Induction]
p:120 [in IndProp]
P:122 [in ProofObjects]
P:124 [in AltAuto]
P:125 [in ProofObjects]
P:126 [in ProofObjects]
P:127 [in Auto]
P:128 [in ProofObjects]
P:128 [in Logic]
p:129 [in Tactics]
p:13 [in Lists]
P:130 [in ProofObjects]
P:130 [in AltAuto]
P:132 [in Logic]
P:133 [in ProofObjects]
P:133 [in Auto]
P:136 [in ProofObjects]
p:137 [in AltAuto]
P:138 [in ProofObjects]
P:138 [in Auto]
P:140 [in ProofObjects]
p:140 [in ImpParser]
p:140 [in AltAuto]
P:141 [in ProofObjects]
P:143 [in Auto]
P:148 [in Auto]
P:16 [in IndPrinciples]
P:17 [in ProofObjects]
p:17 [in Lists]
P:17 [in Auto]
p:17 [in AltAuto]
p:18 [in Lists]
p:185 [in Poly]
p:19 [in Lists]
p:196 [in Poly]
p:197 [in Logic]
P:198 [in AltAuto]
P:199 [in AltAuto]
p:20 [in Lists]
P:200 [in AltAuto]
P:202 [in AltAuto]
P:205 [in AltAuto]
P:21 [in ProofObjects]
p:215 [in AltAuto]
p:218 [in AltAuto]
P:223 [in Logic]
P:223 [in AltAuto]
P:224 [in Logic]
P:224 [in AltAuto]
P:226 [in AltAuto]
P:228 [in Logic]
P:229 [in AltAuto]
P:23 [in ProofObjects]
P:23 [in Auto]
P:23 [in Logic]
p:23 [in Induction]
P:230 [in Logic]
P:233 [in Logic]
P:233 [in AltAuto]
P:235 [in Logic]
P:235 [in AltAuto]
P:236 [in Logic]
P:237 [in AltAuto]
P:238 [in Logic]
P:238 [in AltAuto]
P:24 [in IndPrinciples]
P:240 [in AltAuto]
P:241 [in AltAuto]
P:25 [in ProofObjects]
P:25 [in Logic]
P:26 [in Auto]
P:27 [in Logic]
p:27 [in Induction]
P:29 [in ProofObjects]
p:29 [in Basics]
P:29 [in Logic]
P:296 [in IndProp]
P:301 [in IndProp]
P:303 [in IndProp]
P:31 [in ProofObjects]
p:31 [in Induction]
p:33 [in ImpParser]
P:34 [in ProofObjects]
P:34 [in Imp]
p:34 [in Induction]
P:34 [in IndPrinciples]
p:34 [in AltAuto]
P:35 [in IndPrinciples]
P:350 [in IndProp]
P:351 [in IndProp]
P:36 [in IndPrinciples]
p:37 [in Rel]
p:37 [in Auto]
p:37 [in Induction]
P:37 [in IndPrinciples]
P:38 [in ProofObjects]
P:39 [in Logic]
P:40 [in ProofObjects]
p:40 [in Auto]
p:40 [in ImpParser]
P:41 [in Logic]
P:42 [in Logic]
p:42 [in Induction]
P:43 [in ProofObjects]
p:43 [in Tactics]
P:43 [in Logic]
P:43 [in IndPrinciples]
p:44 [in ImpParser]
P:45 [in ProofObjects]
P:45 [in Logic]
P:47 [in Logic]
P:48 [in ProofObjects]
P:48 [in Logic]
P:48 [in AltAuto]
P:49 [in AltAuto]
p:5 [in Lists]
P:5 [in Auto]
p:50 [in Imp]
P:50 [in Logic]
P:50 [in AltAuto]
P:51 [in Logic]
P:51 [in AltAuto]
p:52 [in Induction]
P:55 [in ProofObjects]
p:55 [in Imp]
p:55 [in Induction]
p:55 [in AltAuto]
P:58 [in ProofObjects]
P:58 [in Logic]
p:58 [in Induction]
p:59 [in AltAuto]
p:6 [in Tactics]
P:60 [in Logic]
P:61 [in ProofObjects]
P:63 [in Logic]
p:64 [in IndPrinciples]
P:66 [in Logic]
P:69 [in Logic]
P:69 [in IndPrinciples]
p:7 [in Lists]
P:70 [in Logic]
P:71 [in ProofObjects]
P:73 [in Logic]
P:76 [in ProofObjects]
p:76 [in IndProp]
P:78 [in Logic]
P:8 [in Auto]
P:8 [in IndPrinciples]
p:81 [in Tactics]
p:83 [in Logic]
p:84 [in Poly]
p:85 [in AltAuto]
p:88 [in Poly]
P:89 [in IndPrinciples]
P:89 [in AltAuto]
p:9 [in Lists]
P:9 [in AltAuto]
P:90 [in Logic]
P:90 [in AltAuto]
P:92 [in AltAuto]
P:94 [in Logic]
P:95 [in AltAuto]
P:96 [in IndPrinciples]
P:99 [in IndPrinciples]
P:99 [in AltAuto]
Q
Q:100 [in AltAuto]q:101 [in Basics]
Q:110 [in AltAuto]
Q:111 [in ProofObjects]
q:111 [in IndProp]
Q:113 [in ProofObjects]
Q:113 [in AltAuto]
Q:116 [in AltAuto]
Q:119 [in AltAuto]
Q:12 [in Auto]
Q:120 [in ProofObjects]
Q:123 [in ProofObjects]
Q:125 [in AltAuto]
Q:127 [in ProofObjects]
Q:128 [in Auto]
Q:129 [in ProofObjects]
Q:131 [in ProofObjects]
Q:131 [in AltAuto]
Q:134 [in ProofObjects]
Q:134 [in Auto]
Q:137 [in ProofObjects]
Q:139 [in ProofObjects]
Q:139 [in Auto]
Q:144 [in Auto]
Q:149 [in Auto]
Q:18 [in ProofObjects]
Q:18 [in Auto]
Q:201 [in AltAuto]
Q:203 [in AltAuto]
Q:206 [in AltAuto]
Q:22 [in ProofObjects]
Q:225 [in AltAuto]
Q:227 [in AltAuto]
Q:230 [in AltAuto]
Q:234 [in Logic]
Q:234 [in AltAuto]
Q:236 [in AltAuto]
Q:237 [in Logic]
Q:239 [in Logic]
Q:239 [in AltAuto]
Q:24 [in ProofObjects]
Q:24 [in Auto]
Q:24 [in Logic]
q:24 [in Induction]
Q:242 [in AltAuto]
Q:26 [in ProofObjects]
Q:26 [in Logic]
Q:27 [in Auto]
Q:28 [in Logic]
q:28 [in Induction]
Q:30 [in ProofObjects]
Q:30 [in Logic]
Q:32 [in ProofObjects]
Q:35 [in ProofObjects]
Q:39 [in ProofObjects]
Q:40 [in Logic]
Q:41 [in ProofObjects]
Q:44 [in ProofObjects]
Q:44 [in Logic]
Q:46 [in ProofObjects]
Q:46 [in Logic]
Q:49 [in ProofObjects]
Q:49 [in Logic]
Q:52 [in Logic]
Q:56 [in ProofObjects]
Q:59 [in ProofObjects]
Q:59 [in Logic]
Q:6 [in Auto]
Q:61 [in Logic]
Q:64 [in Logic]
Q:67 [in Logic]
Q:71 [in Logic]
Q:74 [in Logic]
Q:79 [in Logic]
q:82 [in Tactics]
q:9 [in Tactics]
Q:9 [in Auto]
Q:91 [in AltAuto]
Q:95 [in Logic]
Q:96 [in AltAuto]
R
rest''':162 [in ImpParser]rest'':159 [in ImpParser]
rest'':170 [in ImpParser]
rest':120 [in ImpParser]
rest':126 [in ImpParser]
rest':129 [in ImpParser]
rest':136 [in ImpParser]
rest':156 [in ImpParser]
rest':167 [in ImpParser]
rest':176 [in ImpParser]
rest':183 [in ImpParser]
rest':74 [in ImpParser]
rest':81 [in ImpParser]
rest':89 [in ImpParser]
rest':92 [in ImpParser]
rest':95 [in ImpParser]
rest:108 [in ImpParser]
rest:111 [in ImpParser]
rest:114 [in ImpParser]
rest:117 [in ImpParser]
rest:123 [in ImpParser]
rest:133 [in ImpParser]
rest:150 [in ImpParser]
rest:153 [in ImpParser]
rest:164 [in ImpParser]
rest:173 [in ImpParser]
rest:180 [in ImpParser]
rest:65 [in ImpParser]
rest:68 [in ImpParser]
rest:71 [in ImpParser]
rest:78 [in ImpParser]
rest:85 [in ImpParser]
re':247 [in IndProp]
re':386 [in IndProp]
re0:362 [in IndProp]
re0:368 [in IndProp]
re0:373 [in IndProp]
re1:189 [in IndProp]
re1:195 [in IndProp]
re1:198 [in IndProp]
re1:219 [in IndProp]
re1:363 [in IndProp]
re1:369 [in IndProp]
re1:374 [in IndProp]
re2:191 [in IndProp]
re2:196 [in IndProp]
re2:200 [in IndProp]
re2:220 [in IndProp]
re:147 [in AltAuto]
re:150 [in AltAuto]
re:157 [in AltAuto]
re:2 [in AltAuto]
re:202 [in IndProp]
re:205 [in IndProp]
re:214 [in IndProp]
re:223 [in IndProp]
re:226 [in IndProp]
re:231 [in IndProp]
re:234 [in IndProp]
re:237 [in IndProp]
re:24 [in AltAuto]
re:242 [in IndProp]
re:246 [in IndProp]
re:251 [in IndProp]
re:254 [in IndProp]
re:258 [in IndProp]
re:262 [in IndProp]
re:264 [in IndProp]
re:278 [in IndProp]
re:280 [in IndProp]
re:287 [in IndProp]
re:36 [in AltAuto]
re:377 [in IndProp]
re:381 [in IndProp]
re:382 [in IndProp]
re:384 [in IndProp]
re:39 [in AltAuto]
re:390 [in IndProp]
re:392 [in IndProp]
re:396 [in IndProp]
re:398 [in IndProp]
re:43 [in AltAuto]
re:46 [in AltAuto]
re:6 [in AltAuto]
r1:179 [in IndProp]
r1:181 [in IndProp]
r2:180 [in IndProp]
r2:182 [in IndProp]
r:10 [in Tactics]
R:10 [in Auto]
R:111 [in AltAuto]
R:114 [in AltAuto]
R:117 [in AltAuto]
R:120 [in AltAuto]
R:121 [in ProofObjects]
R:124 [in ProofObjects]
R:126 [in AltAuto]
R:13 [in Auto]
R:132 [in ProofObjects]
R:132 [in AltAuto]
R:135 [in ProofObjects]
R:15 [in Rel]
R:18 [in Rel]
R:18 [in IndProp]
r:183 [in IndProp]
R:19 [in Auto]
R:204 [in AltAuto]
R:228 [in AltAuto]
R:25 [in Auto]
R:28 [in Rel]
R:28 [in Auto]
R:3 [in Rel]
R:31 [in Logic]
R:32 [in Rel]
R:33 [in ProofObjects]
R:39 [in Rel]
R:41 [in Rel]
R:43 [in Rel]
R:45 [in Rel]
R:47 [in ProofObjects]
R:50 [in ProofObjects]
R:57 [in ProofObjects]
R:60 [in Rel]
R:65 [in Logic]
R:68 [in Logic]
R:69 [in Rel]
R:7 [in Auto]
R:72 [in Logic]
R:73 [in Rel]
R:75 [in Logic]
R:78 [in Rel]
R:80 [in Logic]
S
ss:222 [in IndProp]ss:255 [in IndProp]
stack:268 [in Imp]
stack:276 [in Imp]
stack:279 [in Imp]
steps:101 [in ImpParser]
steps:103 [in ImpParser]
steps:143 [in ImpParser]
steps:145 [in ImpParser]
steps:35 [in ImpParser]
steps:41 [in ImpParser]
steps:55 [in ImpParser]
steps:57 [in ImpParser]
steps:59 [in ImpParser]
str:186 [in ImpParser]
st'':106 [in Auto]
st'':115 [in Auto]
st'':229 [in Imp]
st'':245 [in Imp]
st'':315 [in Imp]
st'':324 [in Imp]
st'':90 [in Auto]
st':105 [in Auto]
st':110 [in Auto]
st':114 [in Auto]
st':12 [in ImpCEvalFun]
st':13 [in ImpCEvalFun]
st':217 [in Imp]
st':228 [in Imp]
st':231 [in Imp]
st':236 [in Imp]
st':244 [in Imp]
st':254 [in Imp]
st':256 [in Imp]
st':26 [in ImpCEvalFun]
st':27 [in ImpCEvalFun]
st':300 [in Imp]
st':305 [in Imp]
st':310 [in Imp]
st':314 [in Imp]
st':319 [in Imp]
st':32 [in ImpCEvalFun]
st':323 [in Imp]
st':37 [in ImpCEvalFun]
st':41 [in ImpCEvalFun]
st':45 [in ImpCEvalFun]
st':5 [in ImpCEvalFun]
st':89 [in Auto]
st':92 [in Auto]
st':97 [in Auto]
st1:120 [in Auto]
st1:124 [in Auto]
st1:250 [in Imp]
st1:3 [in Auto]
st1:327 [in Imp]
st1:46 [in Auto]
st1:49 [in ImpCEvalFun]
st1:50 [in Auto]
st1:54 [in Auto]
st1:58 [in Auto]
st1:64 [in Auto]
st2:121 [in Auto]
st2:125 [in Auto]
st2:251 [in Imp]
st2:328 [in Imp]
st2:4 [in Auto]
st2:47 [in Auto]
st2:50 [in ImpCEvalFun]
st2:51 [in Auto]
st2:55 [in Auto]
st2:59 [in Auto]
st2:65 [in Auto]
st:1 [in ImpCEvalFun]
st:102 [in Auto]
st:104 [in Auto]
st:109 [in Auto]
st:113 [in Auto]
st:119 [in Auto]
st:123 [in Auto]
st:14 [in ImpCEvalFun]
st:194 [in Imp]
st:198 [in Imp]
st:2 [in Auto]
st:20 [in ImpCEvalFun]
st:213 [in Imp]
st:220 [in Imp]
st:221 [in Imp]
st:227 [in Imp]
st:230 [in Imp]
st:235 [in Imp]
st:241 [in Imp]
st:243 [in Imp]
st:249 [in Imp]
st:252 [in Imp]
st:255 [in Imp]
st:267 [in Imp]
st:273 [in Imp]
st:277 [in Imp]
st:28 [in ImpCEvalFun]
st:280 [in Imp]
st:297 [in Imp]
st:299 [in Imp]
st:304 [in Imp]
st:309 [in Imp]
st:31 [in ImpCEvalFun]
st:313 [in Imp]
st:318 [in Imp]
st:322 [in Imp]
st:326 [in Imp]
st:36 [in ImpCEvalFun]
st:40 [in ImpCEvalFun]
st:44 [in ImpCEvalFun]
st:45 [in Auto]
st:48 [in ImpCEvalFun]
st:49 [in Auto]
st:53 [in Auto]
st:57 [in Auto]
st:6 [in ImpCEvalFun]
st:63 [in Auto]
st:81 [in Auto]
st:82 [in Auto]
st:88 [in Auto]
st:91 [in Auto]
st:96 [in Auto]
succ:208 [in Poly]
succ:211 [in Poly]
succ:214 [in Poly]
s':126 [in Auto]
s':256 [in IndProp]
s0:364 [in IndProp]
s0:370 [in IndProp]
s0:378 [in IndProp]
s1:152 [in AltAuto]
s1:159 [in AltAuto]
s1:188 [in IndProp]
s1:194 [in IndProp]
s1:203 [in IndProp]
s1:240 [in IndProp]
s1:244 [in IndProp]
s1:249 [in IndProp]
s1:276 [in IndProp]
s1:282 [in IndProp]
s1:289 [in IndProp]
s1:329 [in Imp]
s1:365 [in IndProp]
s1:371 [in IndProp]
s1:379 [in IndProp]
s1:63 [in Lists]
s2:153 [in AltAuto]
s2:160 [in AltAuto]
s2:190 [in IndProp]
s2:199 [in IndProp]
s2:204 [in IndProp]
s2:241 [in IndProp]
s2:245 [in IndProp]
s2:250 [in IndProp]
s2:277 [in IndProp]
s2:283 [in IndProp]
s2:290 [in IndProp]
s2:330 [in Imp]
s2:64 [in Lists]
s3:154 [in AltAuto]
s3:161 [in AltAuto]
s3:284 [in IndProp]
s3:291 [in IndProp]
s:12 [in ImpParser]
S:121 [in AltAuto]
S:127 [in AltAuto]
S:14 [in Auto]
s:141 [in ImpParser]
s:148 [in AltAuto]
s:151 [in AltAuto]
s:158 [in AltAuto]
S:20 [in Auto]
s:213 [in IndProp]
s:216 [in IndProp]
s:218 [in IndProp]
s:224 [in IndProp]
s:230 [in IndProp]
s:238 [in IndProp]
s:25 [in ImpParser]
s:25 [in AltAuto]
s:253 [in IndProp]
s:281 [in IndProp]
s:288 [in IndProp]
S:29 [in Auto]
s:30 [in ImpParser]
s:301 [in Imp]
s:306 [in Imp]
s:352 [in IndProp]
s:353 [in IndProp]
s:355 [in IndProp]
s:358 [in IndProp]
s:360 [in IndProp]
s:361 [in IndProp]
s:367 [in IndProp]
s:37 [in AltAuto]
s:372 [in IndProp]
s:376 [in IndProp]
s:387 [in IndProp]
s:395 [in IndProp]
s:397 [in IndProp]
s:44 [in AltAuto]
s:47 [in AltAuto]
s:50 [in Lists]
s:53 [in Lists]
s:55 [in Lists]
s:58 [in Lists]
s:61 [in Lists]
s:7 [in AltAuto]
s:92 [in Lists]
s:94 [in Lists]
T
term:99 [in ImpParser]test:119 [in Poly]
test:130 [in Poly]
test:131 [in Tactics]
test:136 [in Tactics]
test:140 [in Tactics]
test:144 [in Tactics]
test:147 [in Tactics]
test:216 [in Logic]
test:220 [in Logic]
test:323 [in IndProp]
tk:21 [in ImpParser]
tokens:187 [in ImpParser]
t1:32 [in IndPrinciples]
t1:52 [in IndPrinciples]
t1:96 [in ProofObjects]
t2:33 [in IndPrinciples]
t2:53 [in IndPrinciples]
t2:97 [in ProofObjects]
T:1 [in AltAuto]
T:122 [in AltAuto]
t:125 [in IndPrinciples]
T:127 [in Logic]
T:128 [in AltAuto]
t:129 [in IndPrinciples]
T:131 [in Logic]
t:131 [in IndPrinciples]
t:142 [in ImpParser]
T:146 [in AltAuto]
T:149 [in AltAuto]
T:15 [in Auto]
T:156 [in AltAuto]
T:175 [in IndProp]
t:178 [in IndProp]
T:184 [in IndProp]
T:208 [in IndProp]
T:21 [in Auto]
T:212 [in IndProp]
T:215 [in IndProp]
T:217 [in IndProp]
T:221 [in IndProp]
T:225 [in IndProp]
T:229 [in IndProp]
T:23 [in AltAuto]
T:233 [in IndProp]
T:236 [in IndProp]
T:239 [in IndProp]
T:243 [in IndProp]
T:248 [in IndProp]
T:252 [in IndProp]
T:257 [in IndProp]
T:261 [in IndProp]
T:263 [in IndProp]
T:265 [in IndProp]
T:270 [in IndProp]
T:274 [in IndProp]
T:279 [in IndProp]
T:286 [in IndProp]
T:30 [in Auto]
T:31 [in ImpParser]
T:32 [in ImpParser]
T:35 [in AltAuto]
T:38 [in AltAuto]
T:39 [in ImpParser]
T:42 [in ImpParser]
T:42 [in AltAuto]
t:43 [in ImpParser]
T:45 [in AltAuto]
t:46 [in IndPrinciples]
t:47 [in ImpParser]
t:47 [in IndPrinciples]
T:5 [in AltAuto]
t:88 [in AltAuto]
t:9 [in IndPrinciples]
U
u:109 [in ImpParser]u:112 [in ImpParser]
u:121 [in ImpParser]
U:123 [in AltAuto]
U:129 [in AltAuto]
u:151 [in ImpParser]
U:16 [in Auto]
u:171 [in ImpParser]
U:22 [in Auto]
U:31 [in Auto]
u:75 [in ImpParser]
V
value:135 [in Lists]vx:83 [in Maps]
v1:31 [in Maps]
v1:38 [in Maps]
v1:62 [in Maps]
v1:72 [in Maps]
v2:32 [in Maps]
v2:39 [in Maps]
v2:63 [in Maps]
v2:73 [in Maps]
v:10 [in Maps]
v:131 [in Lists]
v:14 [in Maps]
v:142 [in Lists]
v:18 [in Maps]
v:22 [in Maps]
v:27 [in Maps]
v:47 [in Maps]
v:49 [in Lists]
v:52 [in Lists]
v:53 [in Maps]
v:54 [in Lists]
v:57 [in Lists]
v:58 [in Maps]
v:60 [in Lists]
v:67 [in Maps]
v:78 [in Maps]
W
W:32 [in Auto]X
xo:154 [in Poly]xs:102 [in ImpParser]
xs:104 [in ImpParser]
xs:144 [in ImpParser]
xs:146 [in ImpParser]
xs:15 [in ImpParser]
xs:18 [in ImpParser]
xs:36 [in ImpParser]
xs:45 [in ImpParser]
xs:48 [in ImpParser]
xs:49 [in ImpParser]
xs:51 [in ImpParser]
xs:56 [in ImpParser]
xs:58 [in ImpParser]
xs:60 [in ImpParser]
xs:88 [in ImpParser]
x':15 [in Maps]
x1:123 [in Lists]
x1:25 [in Maps]
x1:40 [in Maps]
x1:56 [in Maps]
x1:70 [in Maps]
x2:124 [in Lists]
x2:26 [in Maps]
x2:41 [in Maps]
x2:57 [in Maps]
x2:71 [in Maps]
X:1 [in Rel]
x:1 [in Maps]
X:10 [in Poly]
x:101 [in Tactics]
x:101 [in Logic]
X:101 [in Poly]
X:102 [in ProofObjects]
x:103 [in ProofObjects]
x:103 [in Tactics]
x:104 [in Logic]
x:104 [in Poly]
X:105 [in Poly]
X:106 [in ProofObjects]
x:106 [in Logic]
x:107 [in ProofObjects]
X:11 [in Poly]
X:110 [in Tactics]
X:111 [in Poly]
X:113 [in Poly]
X:114 [in Poly]
X:115 [in Tactics]
X:116 [in ProofObjects]
x:116 [in Logic]
X:117 [in Poly]
X:118 [in Poly]
X:12 [in Poly]
X:121 [in IndPrinciples]
x:122 [in Logic]
X:123 [in Poly]
x:124 [in Basics]
X:124 [in IndPrinciples]
x:127 [in Lists]
X:128 [in IndPrinciples]
x:129 [in Auto]
X:129 [in Poly]
x:13 [in Poly]
x:13 [in Maps]
X:130 [in Tactics]
X:130 [in IndPrinciples]
x:131 [in Auto]
x:132 [in Tactics]
x:132 [in Poly]
X:133 [in Poly]
x:134 [in Lists]
x:134 [in Logic]
X:135 [in Tactics]
x:136 [in Lists]
x:136 [in Auto]
X:139 [in Tactics]
X:139 [in ImpParser]
x:139 [in Poly]
X:14 [in Rel]
x:141 [in Lists]
x:141 [in Auto]
X:141 [in Poly]
x:141 [in AltAuto]
x:142 [in AltAuto]
X:143 [in Tactics]
x:143 [in AltAuto]
x:144 [in Lists]
X:145 [in Poly]
X:146 [in Tactics]
x:146 [in Auto]
x:148 [in Logic]
x:149 [in Lists]
x:151 [in Auto]
x:151 [in Logic]
X:151 [in Poly]
x:154 [in Logic]
X:156 [in Poly]
x:158 [in Logic]
X:163 [in Poly]
x:164 [in Poly]
X:166 [in Poly]
x:168 [in Logic]
x:169 [in Logic]
X:169 [in Poly]
X:17 [in Rel]
X:17 [in IndProp]
x:17 [in Maps]
x:170 [in Logic]
x:171 [in Logic]
X:171 [in Poly]
X:172 [in Logic]
x:174 [in Imp]
X:175 [in Poly]
x:176 [in Logic]
x:178 [in Logic]
x:179 [in Logic]
x:179 [in Poly]
X:180 [in Logic]
X:181 [in Poly]
X:185 [in Logic]
X:186 [in Poly]
X:187 [in Logic]
x:187 [in IndProp]
x:19 [in Poly]
x:190 [in Poly]
X:192 [in Poly]
X:194 [in AltAuto]
X:197 [in Poly]
X:198 [in Poly]
X:2 [in Rel]
x:200 [in Poly]
X:201 [in Poly]
x:202 [in Logic]
x:203 [in Poly]
x:204 [in Imp]
X:204 [in Poly]
x:206 [in Poly]
X:207 [in Poly]
X:209 [in AltAuto]
X:21 [in Poly]
x:21 [in IndProp]
x:21 [in Maps]
X:210 [in Poly]
X:211 [in AltAuto]
X:213 [in Poly]
X:215 [in Logic]
X:219 [in Logic]
x:222 [in Logic]
x:224 [in Imp]
X:229 [in Logic]
x:23 [in IndProp]
x:231 [in Logic]
x:232 [in Logic]
x:232 [in IndProp]
X:24 [in Tactics]
x:25 [in Poly]
X:26 [in ImpParser]
X:26 [in Poly]
X:26 [in IndProp]
X:26 [in AltAuto]
x:266 [in Imp]
X:27 [in Rel]
x:27 [in Poly]
x:284 [in Imp]
x:29 [in ImpParser]
X:29 [in AltAuto]
x:295 [in IndProp]
x:30 [in Maps]
x:309 [in IndProp]
X:31 [in Rel]
X:31 [in Poly]
X:316 [in IndProp]
X:319 [in IndProp]
X:32 [in Poly]
X:322 [in IndProp]
X:329 [in IndProp]
X:33 [in Poly]
X:332 [in IndProp]
X:334 [in IndProp]
X:336 [in IndProp]
X:338 [in IndProp]
x:339 [in IndProp]
x:34 [in Poly]
X:343 [in IndProp]
X:346 [in IndProp]
x:349 [in IndProp]
x:35 [in Maps]
X:38 [in Rel]
X:38 [in Poly]
x:39 [in Poly]
x:4 [in Rel]
X:40 [in Rel]
x:41 [in Auto]
X:42 [in Rel]
x:42 [in Auto]
x:43 [in Auto]
X:43 [in Poly]
x:46 [in Poly]
x:46 [in Maps]
x:48 [in Rel]
X:48 [in Poly]
X:48 [in IndPrinciples]
x:49 [in Maps]
X:5 [in Poly]
x:51 [in Rel]
X:51 [in Tactics]
x:51 [in IndPrinciples]
x:52 [in Rel]
x:52 [in Tactics]
x:52 [in Maps]
X:53 [in Poly]
X:54 [in IndPrinciples]
X:57 [in Poly]
x:6 [in Maps]
X:60 [in Tactics]
x:60 [in Auto]
x:61 [in Rel]
x:61 [in Tactics]
x:61 [in Auto]
X:61 [in Poly]
x:61 [in Maps]
X:62 [in Poly]
x:64 [in ProofObjects]
x:65 [in ProofObjects]
x:66 [in Maps]
X:68 [in Rel]
x:68 [in Auto]
X:68 [in Poly]
x:70 [in Rel]
x:70 [in Tactics]
X:71 [in Poly]
X:72 [in Rel]
x:73 [in AltAuto]
x:74 [in Rel]
X:74 [in Poly]
X:76 [in Poly]
X:77 [in ProofObjects]
X:77 [in Rel]
x:77 [in Maps]
x:79 [in Rel]
x:8 [in Logic]
x:8 [in Poly]
x:80 [in ProofObjects]
x:80 [in Poly]
x:80 [in AltAuto]
X:81 [in ProofObjects]
x:82 [in ProofObjects]
X:82 [in Poly]
x:82 [in Maps]
X:83 [in ProofObjects]
x:84 [in ProofObjects]
x:84 [in Logic]
x:85 [in Auto]
X:86 [in Poly]
X:86 [in AltAuto]
X:89 [in Logic]
X:90 [in Poly]
x:91 [in Logic]
x:92 [in Logic]
X:93 [in ProofObjects]
X:93 [in Logic]
x:93 [in AltAuto]
X:96 [in Tactics]
x:96 [in Logic]
x:97 [in Logic]
X:97 [in Poly]
x:97 [in AltAuto]
X:98 [in ProofObjects]
x:98 [in Logic]
x:99 [in ProofObjects]
Y
y1:5 [in Rel]y2:6 [in Rel]
y:100 [in ProofObjects]
y:104 [in ProofObjects]
y:108 [in ProofObjects]
Y:111 [in Tactics]
Y:116 [in Tactics]
y:121 [in Logic]
y:130 [in Auto]
y:132 [in Auto]
Y:134 [in Poly]
y:135 [in Auto]
y:137 [in Auto]
y:140 [in Auto]
y:142 [in Auto]
Y:142 [in Poly]
y:145 [in Lists]
y:145 [in Auto]
Y:146 [in Poly]
y:147 [in Auto]
y:149 [in Logic]
y:150 [in Lists]
y:150 [in Auto]
y:152 [in Auto]
y:152 [in Logic]
Y:152 [in Poly]
y:155 [in Logic]
Y:157 [in Poly]
Y:172 [in Poly]
Y:173 [in Logic]
Y:176 [in Poly]
y:180 [in Poly]
Y:182 [in Poly]
Y:187 [in Poly]
y:191 [in Poly]
Y:193 [in Poly]
y:20 [in Poly]
y:203 [in Logic]
y:22 [in IndProp]
y:24 [in IndProp]
y:49 [in Rel]
y:53 [in Rel]
y:53 [in Tactics]
y:62 [in Tactics]
y:64 [in Rel]
y:7 [in Maps]
y:71 [in Rel]
y:71 [in Tactics]
y:74 [in AltAuto]
y:75 [in Rel]
Y:77 [in Poly]
y:80 [in Rel]
y:81 [in Poly]
y:81 [in AltAuto]
Y:83 [in Poly]
Y:87 [in Poly]
y:9 [in Logic]
Y:91 [in Poly]
y:94 [in AltAuto]
Y:98 [in Poly]
y:98 [in AltAuto]
Z
zero:209 [in Poly]zero:212 [in Poly]
zero:215 [in Poly]
z:150 [in Logic]
z:153 [in Logic]
z:156 [in Logic]
Z:177 [in Poly]
Z:183 [in Poly]
Z:188 [in Poly]
Z:194 [in Poly]
z:25 [in IndProp]
z:54 [in Rel]
z:54 [in Tactics]
z:63 [in Tactics]
z:65 [in Rel]
z:76 [in Rel]
Module Index
A
aevalR_extended [in Imp]aevalR_division [in Imp]
AExp [in Imp]
AExp.aevalR_first_try.HypothesisNames [in Imp]
AExp.aevalR_first_try [in Imp]
B
bin1 [in IndProp]bin2 [in IndProp]
bin3 [in IndProp]
BreakImp [in Imp]
E
EqualityPlayground [in ProofObjects]Exercises [in Poly]
Exercises.Church [in Poly]
I
IffPlayground [in Logic]L
LePlayground [in IndProp]M
MumbleGrumble [in Poly]N
NatList [in Lists]NatPlayground [in Basics]
NatPlayground2 [in Basics]
NotPlayground [in Logic]
O
OptionPlayground [in Poly]P
PartialMap [in Lists]Playground [in Basics]
Playground [in IndProp]
Props [in ProofObjects]
Props.And [in ProofObjects]
Props.Ex [in ProofObjects]
Props.Or [in ProofObjects]
Pumping [in IndProp]
R
R [in IndProp]Repeat [in Auto]
T
TuplePlayground [in Basics]Library Index
A
AltAutoAuto
B
BasicsBib
E
ExtractionI
ImpImpCEvalFun
ImpParser
IndPrinciples
IndProp
Induction
L
ListsLogic
M
MapsP
PolyPostscript
Preface
ProofObjects
R
RelT
TacticsLemma Index
A
add_comm3_take3 [in Logic]add_comm3_take2 [in Logic]
add_comm3 [in Logic]
add_shuffle3' [in Induction]
add_shuffle3 [in Induction]
add_assoc'' [in Induction]
add_assoc' [in Induction]
add_assoc [in Induction]
add_comm [in Induction]
add_0_r [in Induction]
add_0_r_secondtry [in Induction]
add_0_r_firsttry [in Induction]
add_comm'' [in IndPrinciples]
add_comm' [in IndPrinciples]
add_assoc' [in IndPrinciples]
add_le_cases [in IndProp]
add_assoc''' [in AltAuto]
add_assoc'' [in AltAuto]
add_assoc_from_induction [in AltAuto]
add_assoc' [in AltAuto]
add_assoc [in AltAuto]
AExp.aeval_iff_aevalR' [in Imp]
AExp.aeval_iff_aevalR [in Imp]
AExp.beval_iff_bevalR [in Imp]
AExp.foo [in Imp]
AExp.foo' [in Imp]
AExp.invert_example1 [in Imp]
AExp.In10 [in Imp]
AExp.In10' [in Imp]
AExp.optimize_0plus_b_sound [in Imp]
AExp.optimize_0plus_sound'' [in Imp]
AExp.optimize_0plus_sound' [in Imp]
AExp.optimize_0plus_sound [in Imp]
AExp.repeat_loop [in Imp]
AExp.silly1 [in Imp]
AExp.silly2 [in Imp]
All_In [in Logic]
all3_spec [in Induction]
andb_eq_orb [in Basics]
andb_commutative'' [in Basics]
andb_true_elim2 [in Basics]
andb_commutative' [in Basics]
andb_commutative [in Basics]
andb_true_iff [in Logic]
andb_false_r [in Induction]
andb_true_elim2' [in AltAuto]
andb_true_elim2 [in AltAuto]
andb_commutative' [in AltAuto]
andb_commutative [in AltAuto]
andb_eq_orb [in AltAuto]
andb3_exchange [in Basics]
andb3_exchange' [in AltAuto]
andb3_exchange [in AltAuto]
and_assoc [in Logic]
and_commut [in Logic]
and_example3 [in Logic]
and_example2'' [in Logic]
and_example2' [in Logic]
and_example2 [in Logic]
and_intro [in Logic]
apply_iff_example2 [in Logic]
apply_iff_example1 [in Logic]
apply_empty [in Maps]
app_length [in Poly]
app_assoc [in Poly]
app_nil_r [in Poly]
app_ne [in IndProp]
app_exists [in IndProp]
app_nil_r'' [in AltAuto]
app_nil_r' [in AltAuto]
app_nil_r [in AltAuto]
app_length' [in AltAuto]
app_length [in AltAuto]
B
bin_nat_bin [in Induction]bin_nat_bin_fails [in Induction]
bin_nat_bin_fails [in Induction]
bin_to_nat_pres_incr [in Induction]
booltree_ind_type_correct [in IndPrinciples]
bool_fn_applied_thrice [in Tactics]
BreakImp.break_ignore [in Imp]
BreakImp.ceval_deterministic [in Imp]
BreakImp.seq_stops_on_break [in Imp]
BreakImp.seq_continue [in Imp]
BreakImp.while_break_true [in Imp]
BreakImp.while_stops_on_break [in Imp]
BreakImp.while_continue [in Imp]
C
ceval_deterministic [in Imp]ceval_deterministic'''' [in Auto]
ceval_deterministic''' [in Auto]
ceval_deterministic'' [in Auto]
ceval_deterministic'_alt [in Auto]
ceval_deterministic' [in Auto]
ceval_deterministic [in Auto]
ceval_deterministic' [in ImpCEvalFun]
ceval_and_ceval_step_coincide [in ImpCEvalFun]
ceval__ceval_step [in ImpCEvalFun]
ceval_step_more [in ImpCEvalFun]
ceval_step__ceval [in ImpCEvalFun]
char_eps_suffix [in IndProp]
char_nomatch_char [in IndProp]
combine_split [in Tactics]
combine_odd_even_elim_even [in Logic]
combine_odd_even_elim_odd [in Logic]
combine_odd_even_intro [in Logic]
contradiction_implies_anything [in Logic]
contrapositive [in Logic]
contras [in AltAuto]
contras' [in AltAuto]
D
derive_corr [in IndProp]de_morgan_not_or [in Logic]
discriminate_ex2 [in Tactics]
discriminate_ex1 [in Tactics]
disc_example [in Logic]
dist_exists_or [in Logic]
dist_not_exists [in Logic]
double_injective_take2 [in Tactics]
double_injective_take2_FAILED [in Tactics]
double_injective [in Tactics]
double_injective_FAILED [in Tactics]
double_neg [in Logic]
double_incr_bin [in Induction]
double_incr [in Induction]
double_plus [in Induction]
E
empty_relation_partial_function [in Rel]empty_nomatch_ne [in IndProp]
empty_matches_eps [in IndProp]
empty_is_empty [in IndProp]
empty_relation_is_empty [in IndProp]
eqbP [in IndProp]
eqbP_practice [in IndProp]
eqb_id_refl [in Lists]
eqb_trans [in Tactics]
eqb_sym [in Tactics]
eqb_true [in Tactics]
eqb_0_l [in Tactics]
eqb_list_true_iff [in Logic]
eqb_neq [in Logic]
eqb_eq [in Logic]
eqb_refl [in Induction]
EqualityPlayground.equality__leibniz_equality [in ProofObjects]
EqualityPlayground.eq_add' [in ProofObjects]
EqualityPlayground.four [in ProofObjects]
EqualityPlayground.leibniz_equality__equality [in ProofObjects]
eq_implies_succ_equal' [in Tactics]
eq_implies_succ_equal [in Tactics]
eq_example3 [in AltAuto]
eq_example2 [in AltAuto]
eq_example1' [in AltAuto]
eq_example1 [in AltAuto]
even_bool_prop [in Logic]
even_double_conv [in Logic]
even_double [in Logic]
even_S [in Induction]
even_ev [in IndPrinciples]
even_ev [in IndPrinciples]
evSS_ev' [in IndProp]
evSS_ev [in IndProp]
ev_plus4 [in ProofObjects]
ev_8 [in ProofObjects]
ev_4'' [in ProofObjects]
ev_4' [in ProofObjects]
ev_4 [in ProofObjects]
ev_ev' [in IndPrinciples]
ev_plus_plus [in IndProp]
ev_ev__ev [in IndProp]
ev_sum [in IndProp]
ev_Even_iff [in IndProp]
ev_Even [in IndProp]
ev_Even_firsttry [in IndProp]
ev_inversion [in IndProp]
ev_double [in IndProp]
ev_plus4 [in IndProp]
ev_4' [in IndProp]
ev_4 [in IndProp]
ev'_ev [in IndProp]
ev100 [in AltAuto]
ev5_nonsense [in IndProp]
excluded_middle_irrefutable [in Logic]
execute_app [in Imp]
Exercises.curry_uncurry [in Poly]
Exercises.fold_length_correct [in Poly]
Exercises.uncurry_curry [in Poly]
existsb_existsb' [in Tactics]
exists_example_2 [in Logic]
ex_falso_quodlibet [in Logic]
F
factor_is_O [in Logic]false_assumed' [in AltAuto]
false_assumed [in AltAuto]
filter_exercise [in Tactics]
filter_not_empty_In' [in IndProp]
filter_not_empty_In [in IndProp]
forallb_true_iff [in Logic]
four_is_Even [in Logic]
f_equal [in Tactics]
H
hyp_name [in AltAuto]I
identity_fn_applied_twice [in Basics]iff_trans [in Logic]
iff_refl [in Logic]
iff_sym [in Logic]
iff_reflect [in IndProp]
includedin_update [in Maps]
injection_ex1 [in Tactics]
intuition_simplify2' [in AltAuto]
intuition_simplify2 [in AltAuto]
intuition_simplify1 [in AltAuto]
intuition_succeed2 [in AltAuto]
intuition_succeed1 [in AltAuto]
inversion_ex2 [in IndProp]
inversion_ex1 [in IndProp]
in_not_nil_42_take5 [in Logic]
in_not_nil_42_take4 [in Logic]
in_not_nil_42_take3 [in Logic]
in_not_nil_42_take2 [in Logic]
in_not_nil_42 [in Logic]
in_not_nil [in Logic]
In_app_iff [in Logic]
In_map_iff [in Logic]
In_map [in Logic]
in_split [in IndProp]
in_re_match [in IndProp]
In10 [in AltAuto]
In10' [in AltAuto]
L
leb_plus_exists [in Logic]leb_refl [in Induction]
leb_true_trans [in IndProp]
leb_iff [in IndProp]
leb_correct [in IndProp]
leb_complete [in IndProp]
le_order [in Rel]
le_step [in Rel]
le_antisymmetric [in Rel]
le_not_symmetric [in Rel]
le_Sn_n [in Rel]
le_S_n [in Rel]
le_Sn_le [in Rel]
le_trans [in Rel]
le_reflexive [in Rel]
le_not_a_partial_function [in Rel]
le_antisym [in Auto]
le_plus_trans [in IndProp]
le_plus_l [in IndProp]
le_trans [in IndProp]
le_antisym [in AltAuto]
lia_fail2 [in AltAuto]
lia_fail1 [in AltAuto]
lia_succeed2 [in AltAuto]
lia_succeed1 [in AltAuto]
loop_never_stops [in Imp]
lt_trans'' [in Rel]
lt_trans' [in Rel]
lt_trans [in Rel]
lt_ge_cases [in IndProp]
M
many_eq' [in AltAuto]many_eq [in AltAuto]
map_rev [in Poly]
match_eps_refl [in IndProp]
match_ex5 [in AltAuto]
match_ex5 [in AltAuto]
match_ex4 [in AltAuto]
match_ex3' [in AltAuto]
match_ex3 [in AltAuto]
match_ex2''' [in AltAuto]
match_ex2'' [in AltAuto]
match_ex2' [in AltAuto]
match_ex2 [in AltAuto]
match_ex1 [in AltAuto]
merge_filter [in IndProp]
minus_n_n [in Induction]
MStar' [in IndProp]
MStar'' [in IndProp]
MStar1 [in IndProp]
mult_n_1 [in Basics]
mult_n_0_m_0 [in Basics]
mult_0_l [in Basics]
mult_is_O [in Logic]
mult_assoc [in Induction]
mult_plus_distr_r [in Induction]
mult_1_l [in Induction]
mult_0_plus' [in Induction]
mult_comm [in AltAuto]
mul_eq_0_ternary [in Logic]
mul_eq_0 [in Logic]
mul_comm [in Induction]
mul_0_r [in Induction]
mul_0_r'' [in IndPrinciples]
mul_0_r' [in IndPrinciples]
MUnion' [in IndProp]
N
nand_not_and' [in AltAuto]nand_not' [in AltAuto]
nand_comm' [in AltAuto]
nand_not [in AltAuto]
nand_comm [in AltAuto]
nand_not_and [in AltAuto]
NatList.app_assoc4 [in Lists]
NatList.app_nil_r [in Lists]
NatList.app_length [in Lists]
NatList.app_assoc [in Lists]
NatList.count_member_nonzero [in Lists]
NatList.eqblist_refl [in Lists]
NatList.fst_swap_is_snd [in Lists]
NatList.involution_injective [in Lists]
NatList.leb_n_Sn [in Lists]
NatList.nil_app [in Lists]
NatList.nonzeros_app [in Lists]
NatList.option_elim_hd [in Lists]
NatList.remove_does_not_increase_count [in Lists]
NatList.rev_injective [in Lists]
NatList.rev_involutive [in Lists]
NatList.rev_app_distr [in Lists]
NatList.rev_length [in Lists]
NatList.rev_length_firsttry [in Lists]
NatList.snd_fst_is_swap [in Lists]
NatList.surjective_pairing [in Lists]
NatList.surjective_pairing_stuck [in Lists]
NatList.surjective_pairing' [in Lists]
NatList.tl_length_pred [in Lists]
nat_bin_nat [in Induction]
negb_involutive [in Basics]
negb_involutive' [in AltAuto]
negb_involutive [in AltAuto]
next_nat_closure_is_le [in Rel]
next_nat_partial_function [in Rel]
nonzeros_app [in AltAuto]
not_exists_dist [in Logic]
not_true_iff_false [in Logic]
not_true_is_false' [in Logic]
not_true_is_false [in Logic]
not_both_true_and_false [in Logic]
not_False [in Logic]
not_implies_our_not [in Logic]
not_equiv_false [in IndProp]
no_whiles_eqv [in Imp]
no_hyp_name [in AltAuto]
nth_error_after_last [in Tactics]
null_matches_none [in IndProp]
n_lt_m__n_le_m [in IndProp]
n_le_m__Sn_le_Sm [in IndProp]
O
one_not_even' [in IndProp]one_not_even [in IndProp]
orb_true_iff [in Logic]
or_assoc [in Logic]
or_distributes_over_and [in Logic]
or_commut [in Logic]
or_intro_l [in Logic]
or_distributes_over_and_from_logic [in AltAuto]
O_le_n [in IndProp]
P
palindrome_converse [in IndProp]pal_rev [in IndProp]
pal_app_rev [in IndProp]
PartialMap.update_neq [in Lists]
PartialMap.update_eq [in Lists]
pe_implies_pi [in ProofObjects]
pe_implies_true_eq [in ProofObjects]
pe_implies_or_eq [in ProofObjects]
pigeonhole_principle [in IndProp]
Playground.test_le3 [in IndProp]
Playground.test_le2 [in IndProp]
Playground.test_le1 [in IndProp]
plus_n_n_injective [in Tactics]
plus_1_neq_0' [in Basics]
plus_1_neq_0 [in Basics]
plus_1_neq_0_firsttry [in Basics]
plus_id_exercise [in Basics]
plus_id_example [in Basics]
plus_1_l [in Basics]
plus_O_n'' [in Basics]
plus_O_n' [in Basics]
plus_O_n [in Basics]
plus_eqb_example [in Logic]
plus_exists_leb [in Logic]
plus_claim_is_true [in Logic]
plus_2_2_is_4 [in Logic]
plus_leb_compat_l [in Induction]
plus_rearrange [in Induction]
plus_rearrange_firsttry [in Induction]
plus_n_Sm [in Induction]
plus_one_r' [in IndPrinciples]
plus_lt [in IndProp]
plus_le_compat_r [in IndProp]
plus_le_compat_l [in IndProp]
plus_le [in IndProp]
plus_n_Sm' [in AltAuto]
plus_n_Sm [in AltAuto]
plus_1_neq_0' [in AltAuto]
plus_1_neq_0 [in AltAuto]
plus_id_exercise_from_basics [in AltAuto]
plus2_spec [in Imp]
proj1 [in Logic]
proj2 [in Logic]
Props.And.and_comm [in ProofObjects]
Props.And.proj1' [in ProofObjects]
Props.Or.inj_l' [in ProofObjects]
Props.Or.or_elim' [in ProofObjects]
provable_equiv_true [in IndProp]
pumping [in AltAuto]
Pumping.napp_star [in IndProp]
Pumping.napp_plus [in IndProp]
Pumping.pumping [in IndProp]
Pumping.pumping_constant_0_false [in IndProp]
Pumping.pumping_constant_ge_1 [in IndProp]
Pumping.weak_pumping [in IndProp]
pup_to_2_ceval [in Imp]
R
reflect_involution [in IndPrinciples]reflect_involution [in IndPrinciples]
reflect_iff [in IndProp]
regex_match_correct [in IndProp]
Repeat.ceval_deterministic' [in Auto]
Repeat.ceval_deterministic [in Auto]
restricted_excluded_middle_eq [in Logic]
restricted_excluded_middle [in Logic]
rev_exercise1 [in Tactics]
rev_involutive [in Poly]
rev_app_distr [in Poly]
re_not_empty_correct [in IndProp]
re_opt_match'' [in AltAuto]
re_opt_match' [in AltAuto]
re_opt_match [in AltAuto]
re_opt_e_match'' [in AltAuto]
re_opt_e_match' [in AltAuto]
re_opt_e_match [in AltAuto]
rsc_trans [in Rel]
rsc_R [in Rel]
rtc_rsc_coincide [in Rel]
R.R_equiv_fR [in IndProp]
S
sillyfun_false [in Tactics]sillyfun1_odd [in Tactics]
sillyfun1_odd_FAILED [in Tactics]
silly_fact_2' [in Tactics]
silly_fact_2 [in Tactics]
silly_fact_2_FAILED [in Tactics]
silly_fact_1 [in Tactics]
silly_ex [in Tactics]
silly1 [in Tactics]
silly1 [in Auto]
silly1 [in AltAuto]
silly2 [in Tactics]
silly2 [in Auto]
silly2 [in AltAuto]
silly2a [in Tactics]
silly2_eauto [in Auto]
silly2_eassumption [in Auto]
silly2_fixed [in Auto]
silly3 [in Tactics]
silly4 [in Tactics]
simple_semi'' [in AltAuto]
simple_semi' [in AltAuto]
simple_semi [in AltAuto]
Sn_le_Sm__n_le_m [in IndProp]
split_combine [in Tactics]
square_mult [in Tactics]
SSSSev__even [in IndProp]
star_ne [in IndProp]
star_app [in IndProp]
star_app [in IndProp]
star_app [in IndProp]
subseq_trans [in IndProp]
subseq_app [in IndProp]
subseq_refl [in IndProp]
succ_inj [in Logic]
S_inj [in Tactics]
S_injective' [in Tactics]
S_injective [in Tactics]
s_compile_correct [in Imp]
s_compile_correct_aux [in Imp]
S_neqb_0 [in Induction]
S_injective_from_tactics [in AltAuto]
T
total_relation_not_partial_function [in Rel]total_relation_is_total [in IndProp]
Toy_correct [in IndPrinciples]
trans_eq [in Tactics]
True_is_true [in Logic]
tr_rev_correct [in Logic]
t_update_permute [in Maps]
t_update_same [in Maps]
t_update_shadow [in Maps]
t_update_neq [in Maps]
t_update_eq [in Maps]
t_apply_empty [in Maps]
U
union_disj [in IndProp]update_permute [in Maps]
update_same [in Maps]
update_shadow [in Maps]
update_neq [in Maps]
update_eq [in Maps]
W
weak_pumping [in AltAuto]Z
zero_nbeq_plus_1 [in Basics]zero_not_one [in Logic]
zero_or_succ [in Logic]
zero_neqb_S [in Induction]
Constructor Index
A
aevalR_extended.E_AMult [in Imp]aevalR_extended.E_AMinus [in Imp]
aevalR_extended.E_APlus [in Imp]
aevalR_extended.E_ANum [in Imp]
aevalR_extended.E_Any [in Imp]
aevalR_extended.AMult [in Imp]
aevalR_extended.AMinus [in Imp]
aevalR_extended.APlus [in Imp]
aevalR_extended.ANum [in Imp]
aevalR_extended.AAny [in Imp]
aevalR_division.E_ADiv [in Imp]
aevalR_division.E_AMult [in Imp]
aevalR_division.E_AMinus [in Imp]
aevalR_division.E_APlus [in Imp]
aevalR_division.E_ANum [in Imp]
aevalR_division.ADiv [in Imp]
aevalR_division.AMult [in Imp]
aevalR_division.AMinus [in Imp]
aevalR_division.APlus [in Imp]
aevalR_division.ANum [in Imp]
AExp.aevalR_first_try.HypothesisNames.E_AMult [in Imp]
AExp.aevalR_first_try.HypothesisNames.E_AMinus [in Imp]
AExp.aevalR_first_try.HypothesisNames.E_APlus [in Imp]
AExp.aevalR_first_try.HypothesisNames.E_ANum [in Imp]
AExp.aevalR_first_try.E_AMult [in Imp]
AExp.aevalR_first_try.E_AMinus [in Imp]
AExp.aevalR_first_try.E_APlus [in Imp]
AExp.aevalR_first_try.E_ANum [in Imp]
AExp.AMinus [in Imp]
AExp.AMult [in Imp]
AExp.ANum [in Imp]
AExp.APlus [in Imp]
AExp.BAnd [in Imp]
AExp.BEq [in Imp]
AExp.BFalse [in Imp]
AExp.BGt [in Imp]
AExp.BLe [in Imp]
AExp.BNeq [in Imp]
AExp.BNot [in Imp]
AExp.BTrue [in Imp]
AExp.E_AMult [in Imp]
AExp.E_AMinus [in Imp]
AExp.E_APlus [in Imp]
AExp.E_ANum [in Imp]
AId [in Imp]
alpha [in ImpParser]
AMinus [in Imp]
AMult [in Imp]
ANum [in Imp]
APlus [in Imp]
App [in IndProp]
B
BAnd [in Imp]Baz1 [in Lists]
Baz2 [in Lists]
BEq [in Imp]
BFalse [in Imp]
BGt [in Imp]
bin1.B0 [in IndProp]
bin1.B1 [in IndProp]
bin1.Z [in IndProp]
bin2.B0 [in IndProp]
bin2.B1 [in IndProp]
bin2.Z [in IndProp]
bin3.B0 [in IndProp]
bin3.B1 [in IndProp]
bin3.Z [in IndProp]
black [in Basics]
BLe [in Imp]
blue [in Basics]
blue [in IndPrinciples]
BNeq [in Imp]
BNot [in Imp]
bool_cons [in Poly]
bool_nil [in Poly]
BreakImp.CAsgn [in Imp]
BreakImp.CBreak [in Imp]
BreakImp.CIf [in Imp]
BreakImp.CSeq [in Imp]
BreakImp.CSkip [in Imp]
BreakImp.CWhile [in Imp]
BreakImp.E_Skip [in Imp]
BreakImp.SBreak [in Imp]
BreakImp.SContinue [in Imp]
BTrue [in Imp]
bt_branch [in IndPrinciples]
bt_leaf [in IndPrinciples]
bt_empty [in IndPrinciples]
B0 [in Basics]
B0 [in Induction]
B1 [in Basics]
B1 [in Induction]
C
CAsgn [in Imp]Char [in IndProp]
CIf [in Imp]
cons [in Poly]
cons' [in Poly]
CSeq [in Imp]
CSkip [in Imp]
CWhile [in Imp]
C1 [in IndPrinciples]
C2 [in IndPrinciples]
D
day [in IndPrinciples]digit [in ImpParser]
E
EmptySet [in IndProp]EmptyStr [in IndProp]
EqualityPlayground.eq_refl [in ProofObjects]
ev_SS [in ProofObjects]
ev_0 [in ProofObjects]
ev_SS [in IndProp]
ev_0 [in IndProp]
ev'_sum [in IndPrinciples]
ev'_2 [in IndPrinciples]
ev'_0 [in IndPrinciples]
ev'_sum [in IndProp]
ev'_2 [in IndProp]
ev'_0 [in IndProp]
E_WhileTrue [in Imp]
E_WhileFalse [in Imp]
E_IfFalse [in Imp]
E_IfTrue [in Imp]
E_Seq [in Imp]
E_Asgn [in Imp]
E_Skip [in Imp]
F
false [in Basics]friday [in Basics]
G
green [in Basics]green [in IndPrinciples]
I
Id [in Lists]L
leaf [in IndPrinciples]LePlayground.le_S [in IndProp]
LePlayground.le_n [in IndProp]
le1_S [in IndPrinciples]
le1_n [in IndPrinciples]
le2_S [in IndPrinciples]
le2_n [in IndPrinciples]
M
MApp [in IndProp]MChar [in IndProp]
MEmpty [in IndProp]
monday [in Basics]
MStarApp [in IndProp]
MStar0 [in IndProp]
MumbleGrumble.a [in Poly]
MumbleGrumble.b [in Poly]
MumbleGrumble.c [in Poly]
MumbleGrumble.d [in Poly]
MumbleGrumble.e [in Poly]
MUnionL [in IndProp]
MUnionR [in IndProp]
N
NatList.cons [in Lists]NatList.nil [in Lists]
NatList.None [in Lists]
NatList.pair [in Lists]
NatList.Some [in Lists]
NatPlayground.O [in Basics]
NatPlayground.S [in Basics]
NatPlayground.stop [in Basics]
NatPlayground.tick [in Basics]
ncons [in IndPrinciples]
night [in IndPrinciples]
nil [in Poly]
nil' [in Poly]
nn [in Rel]
nnil [in IndPrinciples]
nnil' [in IndPrinciples]
node [in IndPrinciples]
NoneE [in ImpParser]
nsnoc [in IndPrinciples]
O
OptionPlayground.None [in Poly]OptionPlayground.Some [in Poly]
other [in ImpParser]
P
pair [in Poly]PartialMap.empty [in Lists]
PartialMap.record [in Lists]
perm3_trans [in IndProp]
perm3_swap23 [in IndProp]
perm3_swap12 [in IndProp]
Playground.le_S [in IndProp]
Playground.le_n [in IndProp]
primary [in Basics]
Props.And.conj [in ProofObjects]
Props.Ex.ex_intro [in ProofObjects]
Props.I [in ProofObjects]
Props.Or.or_intror [in ProofObjects]
Props.Or.or_introl [in ProofObjects]
R
red [in Basics]red [in IndPrinciples]
ReflectF [in IndProp]
ReflectT [in IndProp]
Repeat.CAsgn [in Auto]
Repeat.CIf [in Auto]
Repeat.CRepeat [in Auto]
Repeat.CSeq [in Auto]
Repeat.CSkip [in Auto]
Repeat.CWhile [in Auto]
Repeat.E_RepeatLoop [in Auto]
Repeat.E_RepeatEnd [in Auto]
Repeat.E_WhileTrue [in Auto]
Repeat.E_WhileFalse [in Auto]
Repeat.E_IfFalse [in Auto]
Repeat.E_IfTrue [in Auto]
Repeat.E_Seq [in Auto]
Repeat.E_Asgn [in Auto]
Repeat.E_Skip [in Auto]
rt_trans [in Rel]
rt_refl [in Rel]
rt_step [in Rel]
rt1n_trans [in Rel]
rt1n_refl [in Rel]
R.c1 [in IndProp]
R.c2 [in IndProp]
R.c3 [in IndProp]
R.c4 [in IndProp]
R.c5 [in IndProp]
S
saturday [in Basics]SLoad [in Imp]
SMinus [in Imp]
SMult [in Imp]
SomeE [in ImpParser]
SPlus [in Imp]
SPush [in Imp]
Star [in IndProp]
stroke [in AltAuto]
sunday [in Basics]
T
term_more [in IndProp]term_done [in IndProp]
thursday [in Basics]
true [in Basics]
tuesday [in Basics]
TuplePlayground.bits [in Basics]
TuplePlayground.B0 [in Basics]
TuplePlayground.B1 [in Basics]
t_branch [in IndPrinciples]
t_leaf [in IndPrinciples]
t_trans [in IndProp]
t_step [in IndProp]
U
Union [in IndProp]W
wednesday [in Basics]white [in Basics]
white [in ImpParser]
wrong_ev_SS [in IndProp]
wrong_ev_0 [in IndProp]
Z
Z [in Basics]Z [in Induction]
Axiom Index
C
collatz [in IndProp]F
functional_extensionality [in Logic]Inductive Index
A
aevalR_extended.aevalR [in Imp]aevalR_extended.aexp [in Imp]
aevalR_division.aevalR [in Imp]
aevalR_division.aexp [in Imp]
aexp [in Imp]
AExp.aevalR [in Imp]
AExp.aevalR_first_try.HypothesisNames.aevalR [in Imp]
AExp.aevalR_first_try.aevalR [in Imp]
AExp.aexp [in Imp]
AExp.bevalR [in Imp]
AExp.bexp [in Imp]
B
baz [in Lists]bexp [in Imp]
bin [in Basics]
bin [in Induction]
bin1.bin [in IndProp]
bin2.bin [in IndProp]
bin3.bin [in IndProp]
bool [in Basics]
boollist [in Poly]
booltree [in IndPrinciples]
BreakImp.ceval [in Imp]
BreakImp.com [in Imp]
BreakImp.result [in Imp]
C
ceval [in Imp]chartype [in ImpParser]
clos_refl_trans_1n [in Rel]
clos_refl_trans [in Rel]
clos_trans [in IndProp]
color [in Basics]
com [in Imp]
D
day [in Basics]E
empty_relation [in Rel]empty_relation [in IndProp]
EqualityPlayground.eq [in ProofObjects]
ev [in ProofObjects]
ev [in IndProp]
ev' [in IndPrinciples]
ev' [in IndProp]
exp_match [in IndProp]
F
foo' [in IndPrinciples]I
id [in Lists]L
LePlayground.le [in IndProp]le1 [in IndPrinciples]
le2 [in IndPrinciples]
list [in Poly]
list' [in Poly]
M
merge [in IndProp]MumbleGrumble.grumble [in Poly]
MumbleGrumble.mumble [in Poly]
N
nand [in AltAuto]natlist [in IndPrinciples]
natlist' [in IndPrinciples]
NatList.natlist [in Lists]
NatList.natoption [in Lists]
NatList.natprod [in Lists]
NatPlayground.nat [in Basics]
NatPlayground.nat' [in Basics]
next_nat [in Rel]
nostutter [in IndProp]
no_whilesR [in Imp]
O
optionE [in ImpParser]OptionPlayground.option [in Poly]
P
pal [in IndProp]PartialMap.partial_map [in Lists]
Perm3 [in IndProp]
Playground.le [in IndProp]
prod [in Poly]
Props.And.and [in ProofObjects]
Props.Ex.ex [in ProofObjects]
Props.False [in ProofObjects]
Props.Or.or [in ProofObjects]
Props.True [in ProofObjects]
R
reaches_1 [in IndProp]reflect [in IndProp]
reg_exp [in IndProp]
repeats [in IndProp]
Repeat.ceval [in Auto]
Repeat.com [in Auto]
rgb [in Basics]
rgb [in IndPrinciples]
R.R [in IndProp]
S
sinstr [in Imp]subseq [in IndProp]
T
time [in IndPrinciples]total_relation [in Rel]
total_relation [in IndProp]
Toy [in IndPrinciples]
tree [in IndPrinciples]
TuplePlayground.bit [in Basics]
TuplePlayground.nybble [in Basics]
t_tree [in IndPrinciples]
W
wrong_ev [in IndProp]Definition Index
A
add1 [in ProofObjects]aeval [in Imp]
AExp.add_assoc__lia [in Imp]
AExp.add_comm__lia [in Imp]
AExp.aeval [in Imp]
AExp.beval [in Imp]
AExp.manual_grade_for_beval_rules [in Imp]
AExp.optimize_0plus_b [in Imp]
AExp.optimize_0plus [in Imp]
AExp.silly_presburger_example [in Imp]
AExp.test_optimize_0plus [in Imp]
AExp.test_aeval1 [in Imp]
aexp1 [in Imp]
aexp2 [in Imp]
All [in Logic]
andb [in Basics]
andb' [in Basics]
andb3 [in Basics]
and_assoc [in ProofObjects]
and_exercise [in Logic]
and_example' [in Logic]
and_example [in Logic]
antisymmetric [in Rel]
app [in Poly]
auto_example_7' [in Auto]
auto_example_7 [in Auto]
auto_example_6' [in Auto]
auto_example_6 [in Auto]
auto_example_5' [in Auto]
auto_example_5 [in Auto]
auto_example_4 [in Auto]
auto_example_3 [in Auto]
auto_example_2 [in Auto]
auto_example_1' [in Auto]
auto_example_1 [in Auto]
auto_example_8 [in AltAuto]
auto_example_7' [in AltAuto]
auto_example_7 [in AltAuto]
auto_example_6' [in AltAuto]
auto_example_6 [in AltAuto]
auto_example_5 [in AltAuto]
auto_example_4 [in AltAuto]
auto_example_3 [in AltAuto]
auto_example_2 [in AltAuto]
auto_example_1' [in AltAuto]
auto_example_1 [in AltAuto]
B
b [in Basics]bar [in Tactics]
base_case [in IndPrinciples]
better_t_tree_ind [in IndPrinciples]
better_t_tree_ind_type [in IndPrinciples]
beval [in Imp]
bexp1 [in Imp]
bignumber [in ImpParser]
bin_to_nat [in Basics]
bin_to_nat [in Induction]
booltree_ind_type [in IndPrinciples]
booltree_property_type [in IndPrinciples]
branch_case [in IndPrinciples]
build_proof [in IndPrinciples]
C
c [in IndProp]ceval_example2 [in Imp]
ceval_example1 [in Imp]
ceval_fun_no_while [in Imp]
ceval_example1 [in Auto]
ceval_step [in ImpCEvalFun]
ceval_step3 [in ImpCEvalFun]
ceval_step2 [in ImpCEvalFun]
ceval_step1 [in ImpCEvalFun]
ceval'_example1 [in Auto]
classifyChar [in ImpParser]
combine [in Poly]
combine_odd_even [in Logic]
constfun [in Poly]
constfun_example2 [in Poly]
constfun_example1 [in Poly]
constructor_example [in AltAuto]
contradiction_implies_anything [in ProofObjects]
count [in IndProp]
countoddmembers' [in Poly]
curry [in ProofObjects]
D
d [in IndProp]derive [in IndProp]
derives [in IndProp]
de_morgan_not_or [in ProofObjects]
de_morgan_not_and_not [in Logic]
discriminate_ex3 [in Tactics]
disc_fn [in Logic]
div2 [in IndProp]
doit3times [in Poly]
double [in Induction]
double_neg [in ProofObjects]
double_negation_elimination [in Logic]
double_bin_zero [in Induction]
double_bin [in Induction]
dup_first_two_elts [in AltAuto]
E
eauto_example [in Auto]eg1 [in ImpParser]
eg2 [in ImpParser]
empty [in Maps]
empty_st [in Imp]
eqb [in Basics]
eqb_id [in Lists]
eqb_list [in Logic]
EqualityPlayground.equality__leibniz_equality_term [in ProofObjects]
EqualityPlayground.eq_cons [in ProofObjects]
EqualityPlayground.eq_add [in ProofObjects]
EqualityPlayground.four' [in ProofObjects]
EqualityPlayground.singleton [in ProofObjects]
equivalence [in Rel]
even [in Basics]
Even [in Logic]
even_1000'' [in Logic]
even_1000' [in Logic]
even_1000 [in Logic]
even_42_prop [in Logic]
even_42_bool [in Logic]
ev_plus2'' [in ProofObjects]
ev_plus2' [in ProofObjects]
ev_plus2 [in ProofObjects]
ev_plus4'' [in ProofObjects]
ev_plus4' [in ProofObjects]
ev_8' [in ProofObjects]
ev_4''' [in ProofObjects]
examplemap [in Maps]
examplemap' [in Maps]
examplepmap [in Maps]
example_bexp [in Imp]
example_aexp [in Imp]
example_test_ceval [in ImpCEvalFun]
example_empty [in Maps]
excluded_middle [in Logic]
Exercises.Church.cnat [in Poly]
Exercises.Church.exp [in Poly]
Exercises.Church.exp_3 [in Poly]
Exercises.Church.exp_2 [in Poly]
Exercises.Church.exp_1 [in Poly]
Exercises.Church.mult [in Poly]
Exercises.Church.mult_3 [in Poly]
Exercises.Church.mult_2 [in Poly]
Exercises.Church.mult_1 [in Poly]
Exercises.Church.one [in Poly]
Exercises.Church.one_church_peano [in Poly]
Exercises.Church.one' [in Poly]
Exercises.Church.plus [in Poly]
Exercises.Church.plus_3 [in Poly]
Exercises.Church.plus_2 [in Poly]
Exercises.Church.plus_1 [in Poly]
Exercises.Church.scc [in Poly]
Exercises.Church.scc_3 [in Poly]
Exercises.Church.scc_2 [in Poly]
Exercises.Church.scc_1 [in Poly]
Exercises.Church.three [in Poly]
Exercises.Church.two [in Poly]
Exercises.Church.two_church_peano [in Poly]
Exercises.Church.two' [in Poly]
Exercises.Church.zero [in Poly]
Exercises.Church.zero_church_peano [in Poly]
Exercises.Church.zero' [in Poly]
Exercises.fold_map [in Poly]
Exercises.fold_length [in Poly]
Exercises.manual_grade_for_informal_proof [in Poly]
Exercises.manual_grade_for_fold_map [in Poly]
Exercises.prod_uncurry [in Poly]
Exercises.prod_curry [in Poly]
Exercises.test_map1' [in Poly]
Exercises.test_fold_length1 [in Poly]
existsb [in Tactics]
existsb' [in Tactics]
exp [in Basics]
expect [in ImpParser]
F
f [in IndProp]factorial [in Basics]
fact_in_coq [in Imp]
falso [in ProofObjects]
filter [in Poly]
filter_even_gt7 [in Poly]
firstExpect [in ImpParser]
flat_map [in Poly]
fold [in Poly]
fold_example3 [in Poly]
fold_example2 [in Poly]
fold_example1 [in Poly]
foo [in Tactics]
forallb [in Tactics]
forallb [in Logic]
fst [in Poly]
ftrue [in Poly]
function_equality_ex2 [in Logic]
function_equality_ex2 [in Logic]
function_equality_ex1 [in Logic]
H
hd_error [in Poly]I
IffPlayground.iff [in Logic]implies_to_or [in Logic]
imp1 [in AltAuto]
imp2 [in AltAuto]
imp3 [in AltAuto]
In [in Logic]
includedin [in Maps]
incr [in Basics]
incr [in Induction]
infinite_loop [in ProofObjects]
injection_ex3 [in Tactics]
injective [in Logic]
In_example_2 [in Logic]
In_example_1 [in Logic]
isAlpha [in ImpParser]
isDigit [in ImpParser]
isLowerAlpha [in ImpParser]
isred [in Basics]
isWhite [in ImpParser]
is_fortytwo [in Auto]
is_even_prime [in Logic]
is_three [in Logic]
is_der [in IndProp]
is_fortytwo [in AltAuto]
L
leaf_case [in IndPrinciples]leb [in Basics]
lemma_application_ex [in Logic]
length [in Poly]
length_is_1 [in Poly]
list_of_string [in ImpParser]
list123 [in Poly]
list123' [in Poly]
list123'' [in Poly]
list123''' [in Poly]
loop [in Imp]
ltb [in Basics]
M
manual_grade_for_split_combine [in Tactics]manual_grade_for_informal_proof [in Tactics]
manual_grade_for_no_whiles_terminating [in Imp]
manual_grade_for_XtimesYinZ_spec [in Imp]
manual_grade_for_negation_fn_applied_twice [in Basics]
manual_grade_for_informal_not_PNP [in Logic]
manual_grade_for_double_neg_inf [in Logic]
manual_grade_for_eqb_refl_informal [in Induction]
manual_grade_for_add_comm_informal [in Induction]
manual_grade_for_ceval_step__ceval_inf [in ImpCEvalFun]
manual_grade_for_check_repeats [in IndProp]
manual_grade_for_NoDup_disjoint_etc [in IndProp]
manual_grade_for_nostutter [in IndProp]
manual_grade_for_nand_intuition [in AltAuto]
manual_grade_for_pumping_redux_strong [in AltAuto]
manual_grade_for_pumping_redux [in AltAuto]
manual_grade_for_re_opt_match'' [in AltAuto]
manual_grade_for_re_opt [in AltAuto]
many [in ImpParser]
many_helper [in ImpParser]
map [in Poly]
matches_regex [in IndProp]
match_eps [in IndProp]
minustwo [in Basics]
monochrome [in Basics]
mynil [in Poly]
mynil [in Poly]
mynil' [in Poly]
N
nandb [in Basics]NatList.add [in Lists]
NatList.alternate [in Lists]
NatList.app [in Lists]
NatList.bag [in Lists]
NatList.count [in Lists]
NatList.countoddmembers [in Lists]
NatList.eqblist [in Lists]
NatList.fst [in Lists]
NatList.fst' [in Lists]
NatList.hd [in Lists]
NatList.hd_error [in Lists]
NatList.included [in Lists]
NatList.length [in Lists]
NatList.manual_grade_for_add_inc_count [in Lists]
NatList.member [in Lists]
NatList.mylist [in Lists]
NatList.mylist1 [in Lists]
NatList.mylist2 [in Lists]
NatList.mylist3 [in Lists]
NatList.nonzeros [in Lists]
NatList.nth_error [in Lists]
NatList.nth_bad [in Lists]
NatList.oddmembers [in Lists]
NatList.option_elim [in Lists]
NatList.remove_all [in Lists]
NatList.remove_one [in Lists]
NatList.repeat [in Lists]
NatList.rev [in Lists]
NatList.snd [in Lists]
NatList.snd' [in Lists]
NatList.sum [in Lists]
NatList.swap_pair [in Lists]
NatList.test_hd_error3 [in Lists]
NatList.test_hd_error2 [in Lists]
NatList.test_hd_error1 [in Lists]
NatList.test_nth_error3 [in Lists]
NatList.test_nth_error2 [in Lists]
NatList.test_nth_error1 [in Lists]
NatList.test_eqblist3 [in Lists]
NatList.test_eqblist2 [in Lists]
NatList.test_eqblist1 [in Lists]
NatList.test_rev2 [in Lists]
NatList.test_rev1 [in Lists]
NatList.test_included2 [in Lists]
NatList.test_included1 [in Lists]
NatList.test_remove_all4 [in Lists]
NatList.test_remove_all3 [in Lists]
NatList.test_remove_all2 [in Lists]
NatList.test_remove_all1 [in Lists]
NatList.test_remove_one4 [in Lists]
NatList.test_remove_one3 [in Lists]
NatList.test_remove_one2 [in Lists]
NatList.test_remove_one1 [in Lists]
NatList.test_member2 [in Lists]
NatList.test_member1 [in Lists]
NatList.test_add2 [in Lists]
NatList.test_add1 [in Lists]
NatList.test_sum1 [in Lists]
NatList.test_count2 [in Lists]
NatList.test_count1 [in Lists]
NatList.test_alternate4 [in Lists]
NatList.test_alternate3 [in Lists]
NatList.test_alternate2 [in Lists]
NatList.test_alternate1 [in Lists]
NatList.test_countoddmembers3 [in Lists]
NatList.test_countoddmembers2 [in Lists]
NatList.test_countoddmembers1 [in Lists]
NatList.test_oddmembers [in Lists]
NatList.test_nonzeros [in Lists]
NatList.test_tl [in Lists]
NatList.test_hd2 [in Lists]
NatList.test_hd1 [in Lists]
NatList.test_app3 [in Lists]
NatList.test_app2 [in Lists]
NatList.test_app1 [in Lists]
NatList.tl [in Lists]
NatPlayground.pred [in Basics]
NatPlayground2.minus [in Basics]
NatPlayground2.mult [in Basics]
NatPlayground2.plus [in Basics]
NatPlayground2.test_mult1 [in Basics]
nat_to_bin [in Induction]
nat_ind2 [in IndPrinciples]
nat_ind_tidy [in IndPrinciples]
negb [in Basics]
negb' [in Basics]
next_weekday [in Basics]
nonzeros [in AltAuto]
normalize [in Induction]
NotPlayground.not [in Logic]
not_even_1001' [in Logic]
not_even_1001 [in Logic]
no_whiles [in Imp]
nth_error [in Poly]
O
odd [in Basics]option_map [in Poly]
orb [in Basics]
orb' [in Basics]
order [in Rel]
or_distributes_over_and [in ProofObjects]
or_bogus [in ProofObjects]
P
parse [in ImpParser]parseAExp [in ImpParser]
parseAtomicExp [in ImpParser]
parseBExp [in ImpParser]
parseConjunctionExp [in ImpParser]
parseIdentifier [in ImpParser]
parseNumber [in ImpParser]
parsePrimaryExp [in ImpParser]
parseProductExp [in ImpParser]
parser [in ImpParser]
parseSequencedCommand [in ImpParser]
parseSimpleCommand [in ImpParser]
parseSumExp [in ImpParser]
PartialMap.find [in Lists]
PartialMap.update [in Lists]
partial_function [in Rel]
partial_map [in Maps]
partition [in Poly]
peirce [in Logic]
Playground.b [in Basics]
Playground.lt [in IndProp]
plus_claim [in Logic]
plus' [in Basics]
plus2 [in Imp]
plus3 [in Poly]
preorder [in Rel]
proof_irrelevance [in ProofObjects]
propositional_extensionality [in ProofObjects]
Props.and_comm' [in ProofObjects]
Props.and_comm'_aux [in ProofObjects]
Props.conj_fact [in ProofObjects]
Props.contra [in ProofObjects]
Props.ex_falso_quodlibet' [in ProofObjects]
Props.ex_ev_Sn [in ProofObjects]
Props.false_implies_zero_eq_one [in ProofObjects]
Props.or_commut' [in ProofObjects]
Props.Or.inj_l [in ProofObjects]
Props.Or.or_elim [in ProofObjects]
Props.p_implies_true [in ProofObjects]
Props.some_nat_is_even [in ProofObjects]
Pumping.napp [in IndProp]
Pumping.pumping_constant [in IndProp]
pup_to_n [in Imp]
pup_to_n_1 [in ImpCEvalFun]
pup_to_n [in ImpCEvalFun]
P_m0r' [in IndPrinciples]
P_m0r [in IndPrinciples]
R
reaches_1_in [in IndProp]redundant_match [in AltAuto]
reflect [in IndPrinciples]
reflexive [in Rel]
refl_matches_eps [in IndProp]
regex_match [in IndProp]
reg_exp_ex4 [in IndProp]
reg_exp_of_list [in IndProp]
reg_exp_ex3 [in IndProp]
reg_exp_ex2 [in IndProp]
reg_exp_ex1 [in IndProp]
relation [in Rel]
repeat [in Poly]
repeat' [in Poly]
repeat'' [in Poly]
repeat''' [in Poly]
rev [in Poly]
rev_append [in Logic]
re_not_empty [in IndProp]
re_chars [in IndProp]
re_opt [in AltAuto]
re_opt_e [in AltAuto]
R.fR [in IndProp]
R.manual_grade_for_R_provability [in IndProp]
S
sat_ex2 [in AltAuto]sat_ex1 [in AltAuto]
sillyfun [in Tactics]
sillyfun1 [in Tactics]
snd [in Poly]
split [in Tactics]
split [in Poly]
split_combine_statement [in Tactics]
square [in Tactics]
state [in Imp]
string [in IndProp]
string_of_list [in ImpParser]
subtract_3_from_5_slowly [in Imp]
subtract_slowly [in Imp]
subtract_slowly_body [in Imp]
symmetric [in Rel]
s_compile1 [in Imp]
s_compile [in Imp]
s_execute2 [in Imp]
s_execute1 [in Imp]
s_execute [in Imp]
T
testParsing [in ImpParser]test_existsb_4 [in Tactics]
test_existsb_3 [in Tactics]
test_existsb_2 [in Tactics]
test_existsb_1 [in Tactics]
test_forallb_4 [in Tactics]
test_forallb_3 [in Tactics]
test_forallb_2 [in Tactics]
test_forallb_1 [in Tactics]
test_bin_incr6 [in Basics]
test_bin_incr5 [in Basics]
test_bin_incr4 [in Basics]
test_bin_incr3 [in Basics]
test_bin_incr2 [in Basics]
test_bin_incr1 [in Basics]
test_ltb3 [in Basics]
test_ltb2 [in Basics]
test_ltb1 [in Basics]
test_leb3' [in Basics]
test_leb3 [in Basics]
test_leb2 [in Basics]
test_leb1 [in Basics]
test_factorial2 [in Basics]
test_factorial1 [in Basics]
test_odd2 [in Basics]
test_odd1 [in Basics]
test_andb34 [in Basics]
test_andb33 [in Basics]
test_andb32 [in Basics]
test_andb31 [in Basics]
test_nandb4 [in Basics]
test_nandb3 [in Basics]
test_nandb2 [in Basics]
test_nandb1 [in Basics]
test_orb5 [in Basics]
test_orb4 [in Basics]
test_orb3 [in Basics]
test_orb2 [in Basics]
test_orb1 [in Basics]
test_next_weekday [in Basics]
test_plus3'' [in Poly]
test_plus3' [in Poly]
test_plus3 [in Poly]
test_flat_map1 [in Poly]
test_map3 [in Poly]
test_map2 [in Poly]
test_map1 [in Poly]
test_partition2 [in Poly]
test_partition1 [in Poly]
test_filter_even_gt7_2 [in Poly]
test_filter_even_gt7_1 [in Poly]
test_filter2' [in Poly]
test_anon_fun' [in Poly]
test_countoddmembers'3 [in Poly]
test_countoddmembers'2 [in Poly]
test_countoddmembers'1 [in Poly]
test_filter2 [in Poly]
test_filter1 [in Poly]
test_doit3times' [in Poly]
test_doit3times [in Poly]
test_hd_error2 [in Poly]
test_hd_error1 [in Poly]
test_nth_error3 [in Poly]
test_nth_error2 [in Poly]
test_nth_error1 [in Poly]
test_split [in Poly]
test_length1 [in Poly]
test_rev2 [in Poly]
test_rev1 [in Poly]
test_repeat2 [in Poly]
test_repeat1 [in Poly]
test_ceval [in ImpCEvalFun]
test_der7 [in IndProp]
test_der6 [in IndProp]
test_der5 [in IndProp]
test_der4 [in IndProp]
test_der3 [in IndProp]
test_der2 [in IndProp]
test_der1 [in IndProp]
test_der0 [in IndProp]
test_nostutter_4 [in IndProp]
test_nostutter_3 [in IndProp]
test_nostutter_2 [in IndProp]
test_nostutter_1 [in IndProp]
token [in ImpParser]
tokenize [in ImpParser]
tokenize_ex1 [in ImpParser]
tokenize_helper [in ImpParser]
total_map [in Maps]
transitive [in Rel]
trans_eq_exercise [in Tactics]
trans_eq_example'' [in Tactics]
trans_eq_example' [in Tactics]
trans_eq_example [in Tactics]
trans_example2 [in AltAuto]
trans_example1' [in AltAuto]
trans_example1 [in AltAuto]
tr_rev [in Logic]
TuplePlayground.all_zero [in Basics]
t_update [in Maps]
t_empty [in Maps]
U
uncurry [in ProofObjects]update [in Maps]
update_example4 [in Maps]
update_example3 [in Maps]
update_example2 [in Maps]
update_example1 [in Maps]
W
W [in Imp]X
X [in Imp]XtimesYinZ [in Imp]
Y
Y [in Imp]Z
Z [in Imp]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3897 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (84 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2373 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (31 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (489 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (243 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (93 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (562 entries) |
This page has been generated by coqdoc


The following projects seen below are the fourth projects from each project stack and are all unique and built starting with no CSS. Just HTML content was provided and styles had to be created to position everything correctly and make everything look nice. You can see the full webpage that I created by clicking on the project caption.
Lorem ipsum dolor sit amet, consectetur adipisicing elit. Voluptatem necessitatibus explicabo saepe rerum accusantium assumenda similique incidunt vel fugit tenetur obcaecati, nesciunt commodi? Error architecto necessitatibus sit maiores fugiat. Officia?


Last modified on {{ .Lastmod.Format "02-01-2006" }}.
© {{ now.Year }} {{ .Site.Title }} curated by Edwin Wenink


Stop Number 2 for You!
You can control all the details for your tour stop. Any valid HTML will work inside of Joyride.
Get the details right by styling Joyride with a custom stylesheet!
It works as a modal too!


Virtual assistant for pregnancy and early childhood.
Webby Awards 2019 winner.
We are proud to announce that Chat Crecer won a Webby Award in Social Media Health category.
“I like it because I can talk to her when I feel lonely.”
Rosana (user)
“I see the mothers very excited about the chat, and the information is very useful.”
Magdalena (psychologist)
“It helped me discover hospitals in my neighborhood that I did not know about.”
Belén (user)
It has been shown that proper prenatal controls (5 or more during pregnancy) and timely (first control within the first 13 weeks of gestation) reduce maternal and infant mortality.
In Argentina more than 30% of women do not comply with prenatal check-ups and almost 1 in 10 have their first contact with the health system at the time of birth.
Chat Crecer is a virtual assistant (bot) based on Facebook Messenger that works outside the health system, identifying and recruiting pregnant women where they are. The bot is designed to accompany women during their pregnancy and the baby's first year with personalized information and reminders of attendance to pre and post natal check-ups.
Simple access and easily scalable (does not require geographic adaptation or additional cost) it’s bridge accessibility to health services for a population that is away from it.
The reduction in three quarters of the ratio of maternal mortality (RMM) in 2015 was the 5th of the Millennium Development Goals. Argentina assumed this commitment, in order to fulfill it, the RMM of 2015 should have reached 1.3 x 10,000 live births. However, the ratio for that year was 3 times higher than desired.
Infant mortality rate in Argentina is also higher than expected, reaching 9.7 per 1,000 live births during 2016. 70% of these cases of infant mortality are preventable.
One of the most successful strategies to reduce morbidity and mortality of pregnant women and their babies is to have at least 5 prenatal check-ups, being the first within 13 weeks of gestation.
Increase the number of prenatal check-ups in women who use it.
Reduce the absence to check-ups by tackling pregnancy fears and myths.
Empower women with information about respected labor and standard practices.
Promote breastfeeding.
Provide personalized official information about pregnancy, baby's first year and health care.
Simplify the access to social benefits linked to pregnancy.
| Facebook Messenger | Launched | |
| 2019 | ||
| Web | 2019 |
The first stage of implementation is Pilar, Province of Buenos Aires, that has 4,000 deliveries per year and an infant mortality rate of 11 per 1,000 live births. We are enrolling a population of pregnant women to see the evolution and adoption of the bot.
Field implementation is in charge of a team of 10 university students who act as digital literacy teachers who find pregnant women in the waiting rooms of primary care, in school canteens or social events. Obstetricians during controls promote the use of the bot. At the same time, usability tests and analysis of the platform are carried out (topics consulted, questions asked) that allow to implement improvements in the content and the performance of the tool.
Since July 11, 2018 and until now, 3427 pregnant women and 1160 mothers of babies under the age of 1 were contacted. Of these, 1640 are using the platform.
In the following weeks, together with the epidemiological team of the Ministry of Health of Argentina, we will evaluate in a sample of 800 women the sanitary impact of the tool, by measuring the prevalence of women with proper prenatal control. If the result obtained from the first stage of implementation shows an positive impact will continue to the stage of expansion, deploying the bot nationwide.
We designed a non-randomized intervention study with two comparison strategies.
One is historical controls reported in a health management system (perinatal information system) employed by the public health services.
The other type of comparison is simultaneous among women who are or are not users of the bot. For this comparison, there is a local database of maternity where the number of controls and characteristics of the birth is recorded, to which will be added, for the purpose of this study, the question of the mother's discharge if she used or not used the virtual assistant.
The variables to be compared include, among others
At the same time we are conducting interviews to measure the satisfaction of our users with the chat. We have interviewed 288 users so far and our chat has a 77.78 Net Promoter Score (NPS).
In the undersecretary of digital government we are a multidisciplinary team of developers, designers and researchers. We work developing the virtual assistant accompanied by the ministry of health, and we are carrying out the pilot test in Pilar thanks to the direction of digital inclusion.
National Director of Maternity and Early Childhood
Ana QuirogaMaternity and Early Childhood Coordinator
Gastón PerazzoUX Researcher
María Alejandra BoymortoFunctional analyst
Fernanda SalmerónUX Researcher
Diana SaimoviciDesigner and UX Researcher
Ailín AccintiDirector of Citizen Services
Pablo RoccellaUX Coordinator
Head of Project & Health Advisor
Dolores BullóProject Manager
Daniel AbadieUndersecretary of Digital Government
Ludmila BovaProject Manager
Ivana SchellerDirector of the Maternal Hospital "Comodoro Meisner"
Hebe DominguezObstetric
Johanna Alberini BlancoResearcher
Secretary of Modernization
Adolfo RubinsteinSecretary of Health
Débora HerreraDirector of Digital Products
Felipe FerrariDigital Literacy Tutor
Felipe González ÁlzagaDigital Literacy Tutor
Fidel FranceseDigital Literacy Tutor
Jéssica GonzálezDigital Literacy Tutor
Digital Literacy Tutor
Santiago Da RochaDigital Literacy Tutor
Santiago Lenzi PraDigital Literacy Tutor
Sofía García PiniDigital Literacy Tutor
Sofía SuárezDigital Literacy Tutor
Carla SamaniegoDigital Literacy Tutor
Susana RodriguezResearcher


http://
.herokuapp.com
Wait for a while ....
ganesh
kumar
Don't let your heroku app sleep. Wake it up every 30 minutes
by
GaNeShKuMaRm
☺


Detects Phishing URL
The first phishing lawsuit was filed in 2004 against a Californian teenager who created the imitation of the website “America Online”. With this fake website, he was able to gain sensitive information from users and access the credit card details to withdraw money from their accounts. Other than email and website phishing, there’s also 'vishing' (voice phishing), 'smishing' (SMS Phishing) and several other phishing techniques cybercriminals are constantly coming up with.
HOW: We have used XGBoost model trained on 30 features of a URL which predicts with an accuracy of 0.976. We are also using various modules to extract those 30 features from a single URL.


Welcome to Pizza Planet
Build your Out of This World Pizza
Select Pizza Size
Medium
Large
XL
Select Your First Topping
Onion
Mushroom
Black Olive
Green Bell Pepper
Jalapeno
Submit
Pizza Size
Topping 1:
Topping 2:
Topping 3:
Topping 4:
Topping 5:
Pizza Cost:


7.3 Living longer than you expect
We’ve heard this so many times - “life expectancy is increasing”. “Singapore has one of the highest life expectancies in the world.” But what does the term “life expectancy” mean?
A typical article (such as this one written by a physician) will use estimates of life expectancy to say, for instance, “Singaporean residents can expect to live up to 83.2 years67”. This reading of life expectancy is quite common.
The obvious question here is - Who can expect to live up to 83.2 years? My grandma? Me? My child? Do all Singaporeans now expect to live to the same age68?
The figure most often cited in the media is life expectancy at birth. A more precise way to interpret the life expectancy in 2017 is “Singaporean residents who are born in 2017 can expect to live to 83.2”. This other news article in the Straits Times rightly refers to the life expectancy estimate as “expected lifespan at birth”.
But this still does not fully capture how life expectancy is calculated. To do this, we need to go back to our understanding of age, period, and cohort measures. Life expectancy, as it is reported yearly, is a period measure.
Without going into full detail (interested readers can refer to resources such as this), I will explain briefly how this is calculated. A typical life table from the Department of Statistics (taken from this report) looks like Figure 7.7 (it shows just the top part, the entire table is a few pages long).
Age-specific mortality rates (not pictured, but often referred to as \(m_x\)) for a specific year are obtained from the national mortality database and turned into69 the probability of dying in a specific age-interval (\(q_x\), pictured).
You start with a hypothetical base population, usually 100,000, and you put them through the mortality rates of each age until there are no more survivors (\(l_x\)). In other words, the probability of dying at an age-interval becomes certain (\(q_x = 1\)) at some point (usually 100+) since no one is immortal.
From there, you calculate a number of other things (e.g., \(d_x\), \(L_x\), \(T_x\), using simple math formulas). These numbers then help you derive the life expectancy (basically, \(e_x = \frac{T_x}{l_X}\)).
You may not yet fully understand what is happening here, but just note one key thing - the key quantities here that affect everything else in the whole process are the age-specific mortality rates (\(m_x\)). And these age-specific mortality rates used in calculating life expectancy are a period measure, which capture what is happening that particular year.
To understand what this means for how we interpret life expectancy, we return to our previous interpretation - that “Singaporean residents who are born in 2017 can expect to live to 83.2”.
Let’s now make it more precise and say that “Singaporean residents who are born in 2017 and who are exposed to mortality rates of 2017 throughout their lives can expect to live to 83.2”.
This sounds highly awkward, I know. You would have to imagine some kind of time machine allowing you to stay stuck in 2017, continuing to experience its mortality rates even as you grow older. But it is in fact how the measure is calculated. Life expectancy, as often cited in the media, is a period measure that is constructed by stitching together the experiences of multiple cohorts (often called a synthetic cohort).
A more intuitive measure of life expectancy is called cohort life expectancy. Cohort life expectancy follows every person who was born in a certain year (e.g., 1965), and is calculated using the observed/projected rates of all persons in that cohort. With cohort life expectancy, we can truly say that “Singaporean residents born in year XXXX live XX.X years on average”. So why don’t we do this? The answer is simple - to obtain observed rates, we need to observe these deaths for each cohort! We would therefore need to wait for all (or most70) of each cohort to pass away before we can calculate such numbers.
Period life expectancy is therefore practical to use as a measure of how well our health system is doing from year to year, but we must acknowledge its limitations. In order to examine how volatile period rates of life expectancy can be, we can simply look at older rates of life expectancy.
But first, a small excursus - if you look back at Figure 7.7, one thing you will realize is that there are life expectancy estimates for each age. Therefore, life expectancy at age 40 is not the same as life expectancy at birth, and they do not usually add up (i.e., Life expectancy at 40 \(\neq\) Life expectancy at birth - 40). Knowing this, we can now do a little thought experiment with life expectancy estimates.
Let us now look at life expectancy at birth in the year 1965. Using the Department of Statistics Table Builder (go here) to retrieve the data, it seems life expectancy at birth for Singapore residents back in 1965 was 64.5. Using the common way of interpreting these data, we might say, “we can expect those born in 1965 to live up to 64.5 years old.”
Fast forward to 2017, and those born in 1965 are now 52 years old. If those numbers in 1965 are correct, it follows that we might expect life expectancy at 52 to be \(64.5 - 52 = 12.3\) years. Let’s go back to the Complete Life Tables we were looking at before to see how long more those born in 1965 can expect to live (Figure 7.8).
Wait. We see now that those who aged 52 in 2017 can in fact expect to live 32.5 more years. That means they are expected to live up to \(52 + 32.5 = 84.5\) years old! That seems way different from the 64.5 years projected by mortality statistics in 1965. Why is this so? This is because period life expectancy does not account for future improvements in mortality driven by better healthcare, hygiene, health behaviors etc. Period life expectancy is therefore often an underestimate of the true cohort life expectancy71. The discrepancy we see between the 1965 life table and the 2017 life table is likely due to great improvements in mortality rates since independence.
Having studied how life expectancy ‘works’, let us conclude by evaluating this paragraph from an article on the Dollars and Sense website, aimed at helping Singaporeans plan their retirement:
The next step of the retirement planning equation is to understand how long we can expect to spend in retirement. The longer we spend in retirement, the more we need to sustain ourselves.
How Long Do We Spend In Retirement? The simplest way to derive this figure is to use the average life expectancy of Singaporeans – which stands at 83.1 years today. This figure is only going to go up as the latest report from the World Health Organisation (WHO) revealed that people here can expect to live up to 85.4 years by 2040.
What this tells us is that if we retire at the moment we are able to receive our CPF LIFE payouts – at 65 – and live to the average life expectancy in Singapore – to 83.1 – we will have close to 18 years of retirement.
What are the misinterpretations of life expectancy present here? First, the writer talks about average life expectancy as if it applies to everyone. As we discussed, however, the number he uses likely reflects the life expectancy at birth. Is he speaking to newborns and asking them to plan for retirement? A better approach would be to go to the Complete Life Tables published by the Department of Statistics and refer to life expectancy at 50 (or some other reference age that his target audience can identify with). Second, he is correct that life expectancy will probably continue to rise, but the 18 years (obtained supposedly using \(83.1 - 65 \approx 18\)) is likely an underestimate of how long “retirement” will be (apart from the error already made in the first point). Plan harder, people.
The figure for the year 2017.↩
If this is true, then if life expectancy increases faster than one year annually, does this mean we can all expect to be immortal? You can see how ludicrous this sounds.↩
Some assumptions need to be made here about a quantity called \(a_x\), which captures when most deaths in a certain age-interval happen within the time period, but usually this calculation is straightforward.↩
Using a mixture of observed and projected rates is possible.↩
Unless mortality rates spike due to events such as wars, famines etc.↩


I could easily drag this report into pages and pages full of details about what I saw and how I felt, but I will try to keep this reasonably short.
To begin, my work is very intense at times. During release phases, I have often had to work 85-100 hour weeks in order to meet deadlines. As I'm sure many could guess, amphetamine abuse [dextroamphetamine] to achieve these superhuman hours was common. At the time of this experience, I had been up for what I estimate to be approximately 4 days. However, I will say that my knowledge of the event is very spotty... much of what I will say in the following paragraphs is pieced together from the information I have received from others.
This experience occurred while I was out of town visiting a friend at his apartment. The timeline of what happened is very mismatched in my head, but I will point out that the most noticeable negative symptoms that I recall were basically mini schizophrenic episodes, something I'd describe as being in two places at once, or more accurately flipping between two or more realities involuntarily, which, from what I'm told, resulted in me saying some very strange stuff to my friends at inappropriate times.
In all my research I will say that I believe the substance at fault is MDMA. I know I took a much higher dose than I ever have before, although I do not remember this. What I have decided is that I was taking it and then forgetting I took it, taking more, forgetting I took it, taking it... ad infinitum. It was very common at this point for me to completely lose track of short-term memory. At some point I took a sleeping pill, Zopiclone, which is chemically similar to Ambien (Zolpidem). I would say this did nothing but worsen the situation if anything.
This was nothing, however, compared to what was about to happen. I was pretty much worthless, at least from a judgment standpoint, at this time. I should have gone to sleep, I'm sure.
 Thousands of them, around every corner, on every surface -- every object morphed into some sort of malicious insect. This was something I managed to endure for several hours before really freaking out. I knew it wasn't real, but it was so visually terrifying that it was hard to keep my cool. The turning point was upon doing a whippet (nitrous oxide)... like I said, my judgement was gone. I had felt my sanity slipping and for some reason I thought nitrous would help -- who knows why.
I recall watching the spiders on the bed nearby as I inhaled the gas -- and as soon as I felt the whippet, I watched them begin to multiply and spawn and grow larger and move faster. I ripped the balloon out of my mouth and started smacking the bed with it, I'm told: it was at this point was when my sense of reality started to slip.
On a side note, I have had other hallucinogenic experiences -- I think anyone who has knows the dream-like quality of trips... it's distinct, and as far as memories go, it is one clear way to distinguish drug-induced experiences from reality. The noteworthy element of this experience was its *utter lack* of the dreamlike feeling. There was literally no deviation from reality that could provide any sort of indication that what I was seeing was not real. It looked real, it felt real, and my mind regards it as real, despite the fact that I know it wasn't. I believe the obvious conclusion, since none of the substances I ingested are known to induce such acute hallucinations, is that this was a psychotic episode, more specifically a case of amphetamine psychosis. This type of psychosis is often described as short-term paranoid schizophrenia, which basically describes my experience perfectly.
Anyway, it was clear from this point forward that the frightening nature of my surroundings was directly correlated with how frightened I was. It got progressively worse as I got more and more terrified -- at a certain point I would actually say I went into shock, for I had come to terms with watching spiders grow out of my skin as something I could not do anything about, and was 'beyond fear' if that makes any sense. I had not become desensitized, but the opposite, activating the body's natural defense mechanisms, which turned off my sensation of acute terror.
The experience became progressively more and more intense. I know there are several occasions that my mind has suppressed. I have learned of these from those who were following me around the apartment as I sprayed clear coat paint all over the place (thinking I was killing bugs with bug spray) and yelled nonsensical things to the tune of 'why me' and 'when is it going to stop', etc. I recall that I started to see ghost-like figures, stationary, watching me, some menacing, some not.
The general theme of the experience was basically as such: No matter what I did or where I hid -- there was something terrifying right there with me, and these things became increasingly awful. There was no safety, not even in my girlfriend's arms, who I apparently pushed forcefully into a wall because I saw a bug with wings on her back. I have literally no memory of this at all, but she was scared to be around me after that, from what she told me.
This is not to say that there wasn't an element of fascination to all of this. No drug could ever rival this sort of trip -- if one could harness the contents of my subconscious and make them into a movie, they'd have an instant blockbuster. I saw horrors that make Aliens seem like a movie for children.
Eventually, I was taken to the hospital. It had been approximately eight hours of pure terror. I no longer could make the distinction between reality and psychosis-induced visuals. I spent minutes on end trying to convince the doctor there was a worm growing out of my leg. Oddly enough, I calmed down in the hospital and the visions started to disappear. Upon regaining a bit of my sanity, I realized that I thought these things were real, but I couldn't figure out how I had convinced myself of this. It was a very peculiar feeling.
Sleep was all I needed, I guess. I slept for 3 hours in the hospital bed, and upon waking up the visuals were basically gone.
This experience will never leave me, however. It's been 6 months and I still harbor paranoid fears of insects and spiders. Additionally, I acquired a mild case of HPPD (Hallucinogen Persisting Perception Disorder), often seeing floaters or after-images burnt into my vision -- and on the rare occasions that I stay awake all night, this worsens: objects begin to creep around in my peripheral vision, walls have 'crawling' surfaces, etc. From what I understand, this may be with me my whole life -- but it really isn't bad enough to inhibit my ability to live -- just enough to never let me forget. I'll probably never touch E again... no euphoria could ever be worth this kind of living nightmare.
Experience Reports are the writings and opinions of the individual authors who submit them.
Some of the activities described are dangerous and/or illegal and none are recommended by Erowid.