Logiweb(TM)

Logiweb dictionary of check

Up Help

0 0 check
1 0 alpha
2 0 beta
3 0 gamma
4 0 delta
5 0 epsilon
6 0 varepsilon
7 0 zeta
8 0 eta
9 0 theta
10 0 vartheta
11 0 iota
12 0 kappa
13 0 lambda
14 0 mu
15 0 nu
16 0 xi
17 0 pi
18 0 varpi
19 0 rho
20 0 varrho
21 0 sigma
22 0 varsigma
23 0 tau
24 0 upsilon
25 0 phi
26 0 chi
27 0 psi
28 0 omega
29 0 Gamma
30 0 Delta
31 0 Theta
32 0 Lambda
33 0 Xi
34 0 Pi
35 0 Sigma
36 0 Upsilon
37 0 Phi
38 0 Psi
39 0 Omega
40 0 cla
41 0 clb
42 0 clc
43 0 cld
44 0 cle
45 0 clf
46 0 clg
47 0 clh
48 0 cli
49 0 clj
50 0 clk
51 0 cll
52 0 clm
53 0 cln
54 0 clo
55 0 clp
56 0 clq
57 0 clr
58 0 cls
59 0 clt
60 0 clu
61 0 clv
62 0 clw
63 0 clx
64 0 cly
65 0 clz
66 0 statement
67 0 proof
68 0 meta
69 0 math
70 0 tactic
71 0 unitac
72 0 locate
73 2 statement define " as " end define
74 2 proof define " as " end define
75 2 meta define " as " end define
76 2 math define " as " end define
77 2 tactic define " as " end define
78 2 unitac define " as " end define
79 2 locate define " as " end define
80 1 ensure math " end math
81 0 #a
82 0 #b
83 0 #c
84 0 #d
85 0 #e
86 0 #f
87 0 #g
88 0 #h
89 0 #i
90 0 #j
91 0 #k
92 0 #l
93 0 #m
94 0 #n
95 0 #o
96 0 #p
97 0 #q
98 0 #r
99 0 #s
100 0 #t
101 0 #u
102 0 #v
103 0 #w
104 0 #x
105 0 #y
106 0 #z
107 1 tacfresh ( " )
108 2 unifresh ( " , " )
109 0 L00
110 0 L01
111 0 L02
112 0 L03
113 0 L04
114 0 L05
115 0 L06
116 0 L07
117 0 L08
118 0 L09
119 0 L10
120 0 L11
121 0 L12
122 0 L13
123 0 L14
124 0 L15
125 0 L16
126 0 L17
127 0 L18
128 0 L19
129 0 L20
130 0 L21
131 0 L22
132 0 L23
133 0 L24
134 0 L25
135 0 L26
136 0 L27
137 0 L28
138 0 L29
139 0 L30
140 0 L31
141 0 L32
142 0 L33
143 0 L34
144 0 L35
145 0 L36
146 0 L37
147 0 L38
148 0 L39
149 0 L40
150 0 L41
151 0 L42
152 0 L43
153 0 L44
154 0 L45
155 0 L46
156 0 L47
157 0 L48
158 0 L49
159 0 L50
160 0 L51
161 0 L52
162 0 L53
163 0 L54
164 0 L55
165 0 L56
166 0 L57
167 0 L58
168 0 L59
169 0 L60
170 0 L61
171 0 L62
172 0 L63
173 0 L64
174 0 L65
175 0 L66
176 0 L67
177 0 L68
178 0 L69
179 0 L70
180 0 L71
181 0 L72
182 0 L73
183 0 L74
184 0 L75
185 0 L76
186 0 L77
187 0 L78
188 0 L79
189 0 L80
190 0 L81
191 0 L82
192 0 L83
193 0 L84
194 0 L85
195 0 L86
196 0 L87
197 0 L88
198 0 L89
199 0 L90
200 0 L91
201 0 L92
202 0 L93
203 0 L94
204 0 L95
205 0 L96
206 0 L97
207 0 L98
208 0 L99
209 0 False
210 0 p.A1
211 0 p.A2
212 0 p.A3
213 0 p.MP
214 0 p.Prop
215 0 p.IProp
216 2 distinctvar ( " , " )
217 3 metaavoid1 ( " , " , " )
218 3 metaavoid1* ( " , " , " )
219 4 objectavoid1 ( " , " , " , " )
220 4 objectavoid1* ( " , " , " , " )
221 4 metafree ( " , " , " , " )
222 4 metafree* ( " , " , " , " )
223 4 objectfree ( " , " , " , " )
224 4 objectfree* ( " , " , " , " )
225 2 remove ( " , " )
226 3 metaavoid2* ( " , " , " )
227 3 metasubst ( " , " , " )
228 3 metasubst* ( " , " , " )
229 3 metasubstc ( " , " , " )
230 4 metasubstc1 ( " , " , " , " )
231 4 metasubstc1* ( " , " , " , " )
232 4 metasubstc2 ( " , " , " , " )
233 4 metasubstc2* ( " , " , " , " )
234 4 metasubstc3 ( " , " , " , " )
235 1 expand-All ( " )
236 3 expand-All1 ( " , " , " )
237 2 make-string ( " , " )
238 0 end diagnose
239 3 Locate ( " , " , " )
240 5 Locate1 ( " , " , " , " , " )
241 2 error ( " , " )
242 3 mismatch ( " , " , " )
243 3 mismatch* ( " , " , " )
244 2 eval-Init ( " , " )
245 3 eval-Ponens ( " , " , " )
246 3 eval-Probans ( " , " , " )
247 3 eval-Verify ( " , " , " )
248 3 eval-Curry ( " , " , " )
249 3 eval-Uncurry ( " , " , " )
250 3 eval-Deref ( " , " , " )
251 3 eval-at ( " , " , " )
252 5 eval-at1 ( " , " , " , " , " )
253 4 eval-infer ( " , " , " , " )
254 4 eval-endorse ( " , " , " , " )
255 4 eval-ie ( " , " , " , " )
256 4 eval-all ( " , " , " , " )
257 3 eval-cut ( " , " , " )
258 2 seqeval ( " , " )
259 0 Repeat
260 0 prepare proof indentation
261 2 claiming ( " , " )
262 0 proofcheck
263 1 proofcheck1 ( " )
264 1 proofcheck2 ( " )
265 2 seqeval* ( " , " )
266 2 premisecheck* ( " , " )
267 2 checked ( " , " )
268 2 premisecheck ( " , " )
269 4 circularitycheck1 ( " , " , " , " )
270 4 circularitycheck2 ( " , " , " , " )
271 4 circularitycheck2* ( " , " , " , " )
272 0 lemma1
273 0 lemma2
274 0 lemma2a
275 0 lemma2b
276 0 lemma2c
277 0 lemma2d
278 0 lemma2e
279 0 lemma2f
280 0 lemma3
281 0 lemma4a
282 0 lemma4b
283 0 lemma4c
284 0 lemma4d
285 0 lemma4e
286 0 lemma4f
287 0 lemma4g
288 2 int2string ( " , " )
289 2 int2string1 ( " , " )
290 2 val2term ( " , " )
291 2 card2term ( " , " )
292 3 univar ( " , " , " )
293 2 pterm ( " , " )
294 4 pterm1 ( " , " , " , " )
295 3 pterm2 ( " , " , " )
296 3 pterm2* ( " , " , " )
297 3 inst ( " , " , " )
298 3 inst* ( " , " , " )
299 3 occur ( " , " , " )
300 3 occur* ( " , " , " )
301 3 unify ( " , " , " )
302 3 unify* ( " , " , " )
303 3 unify2 ( " , " , " )
304 3 taceval ( " , " , " )
305 3 taceval1 ( " , " , " )
306 0 tacstate0
307 0 unitac0
308 3 tactic-push ( " , " , " )
309 2 tactic-pop ( " , " )
310 1 tactic-Init ( " )
311 1 tactic-Ponens ( " )
312 1 tactic-Probans ( " )
313 1 tactic-Verify ( " )
314 1 tactic-Curry ( " )
315 1 tactic-Uncurry ( " )
316 1 tactic-Deref ( " )
317 1 tactic-at ( " )
318 4 tactic-at1 ( " , " , " , " )
319 5 tactic-at2 ( " , " , " , " , " )
320 1 tactic-infer ( " )
321 1 tactic-endorse ( " )
322 1 tactic-ie ( " )
323 1 tactic-all ( " )
324 1 tactic-cut ( " )
325 3 tactic-cut1 ( " , " , " )
326 0 hook-arg
327 0 hook-res
328 0 hook-idx
329 0 hook-uni
330 0 hook-pre
331 0 hook-cond
332 0 hook-parm
333 0 hook-unitac
334 0 hook-rule
335 0 hook-lemma
336 0 hook-conclude
337 1 unitac ( " )
338 3 unitac1 ( " , " , " )
339 3 unieval ( " , " , " )
340 1 unitac-Init ( " )
341 1 unitac-Conclude ( " )
342 1 unitac-conclude ( " )
343 1 unitac-conclude-std ( " )
344 1 unitac-Ponens ( " )
345 1 unitac-ponens ( " )
346 1 unitac-Probans ( " )
347 1 unitac-probans ( " )
348 1 unitac-Verify ( " )
349 1 unitac-verify ( " )
350 1 unitac-Curry ( " )
351 1 unitac-Uncurry ( " )
352 1 unitac-Deref ( " )
353 1 unitac-idest ( " )
354 1 unitac-At ( " )
355 1 unitac-at ( " )
356 1 unitac-Infer ( " )
357 1 unitac-infer ( " )
358 1 unitac-Endorse ( " )
359 1 unitac-endorse ( " )
360 1 unitac-All ( " )
361 1 unitac-all ( " )
362 1 unitac-cut ( " )
363 3 unitac-adapt ( " , " , " )
364 1 unitac-rule ( " )
365 1 unitac-rule-std ( " )
366 3 unitac-theo ( " , " , " )
367 3 unitac-rule0 ( " , " , " )
368 3 unitac-rule-plus ( " , " , " )
369 4 unitac-rule-stmt ( " , " , " , " )
370 3 unitac-rule1 ( " , " , " )
371 3 unitac-rule2 ( " , " , " )
372 3 unitac-search ( " , " , " )
373 5 unitac-search1 ( " , " , " , " , " )
374 2 unitac-rule3 ( " , " )
375 2 unitac-rule4 ( " , " )
376 4 unitac-rule5 ( " , " , " , " )
377 3 unitac-stack ( " , " , " )
378 1 unitac-lemma ( " )
379 1 unitac-lemma-std ( " )
380 1 unitac-Rule ( " )
381 2 seqcnt ( " , " )
382 1 tactic-conclude-cut ( " )
383 1 tactic-premise-line ( " )
384 1 tactic-condition-line ( " )
385 1 tactic-block ( " )
386 0 System S
387 0 S.S1
388 0 S.S5
389 0 S.reflexivity
390 1 "#
391 2 " plist ( " )
392 3 " def ( " , " )
393 3 " lhs ( " , " )
394 3 " rhs ( " , " )
395 2 " metadef ( " )
396 2 " metavar ( " )
397 2 " stmt-rhs ( " )
398 2 " proof-rhs ( " )
399 2 " tactic-rhs ( " )
400 2 " unitac-rhs ( " )
401 2 " locate-rhs ( " )
402 2 " mathdef ( " )
403 2 " valuedef ( " )
404 2 " objectvar ( " )
405 2 " objectlambda ( " )
406 2 " objectquote ( " )
407 2 " objectterm ( " )
408 2 " objectterm* ( " )
409 2 " metaterm ( " )
410 2 " metaterm* ( " )
411 3 " metaavoid ( " ) "
412 3 " metaavoid* ( " ) "
413 3 " objectavoid ( " ) "
414 3 " objectavoid* ( " ) "
415 2 " set+ "
416 2 " set- "
417 2 " set-- "
418 2 " union "
419 2 " member "
420 2 " subset "
421 2 " set= "
422 2 " sequent= "
423 1 p.not "
424 2 " p.imply "
425 1 metadeclare "
426 1 " Init
427 1 " Ponens
428 1 " Probans
429 1 " Verify
430 1 " Curry
431 1 " Uncurry
432 1 " Deref
433 1 " At
434 1 " Infer
435 1 " Endorse
436 1 " All
437 1 " Conclude
438 1 " Rule
439 2 " at "
440 2 " ponens "
441 2 " probans "
442 2 " verify "
443 2 " p.mp "
444 2 " infer "
445 2 " endorse "
446 2 " id est "
447 2 All " : "
448 2 " oplus "
449 2 " conclude "
450 4 line " : " >> " ; "
451 4 Line " : " >> " ; "
452 3 line " : " >> " ;
453 3 line " : " >> " qed
454 3 line " : Premise >> " ; "
455 3 Line " : Premise >> " ; "
456 3 line " : Condition >> " ; "
457 3 Line " : Condition >> " ; "
458 3 line " : Arbitrary >> " ; "
459 4 line " : Local >> " = " ; "
460 4 line " : Block >> Begin ; " line " : Block >> End ; "
461 4 Line " : Block >> Begin ; " line " : Block >> End ; "
462 2 " ;; "
463 2 " proves "
464 2 axiom " : " end axiom
465 2 rule " : " end rule
466 2 theory " : " end theory
467 2 lemma " : " end lemma
468 3 " lemma " : " end lemma
469 2 proof of " : "
470 3 " proof of " : "
471 2 dbug ( " ) "
472 2 dbug* ( " ) "
473 2 glue ( " ) "
474 2 diag ( " ) "
475 2 disp ( " ) "
476 2 form ( " ) "
477 2 glue' ( " ) "
478 2 dbug' ( " ) "
479 2 diag' ( " ) "
480 2 disp' ( " ) "
481 2 form' ( " ) "
482 3 LocateProofLine ( " , " ) "

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:11:58.175987 = MJD-54293.TAI:20:12:31.175987 = LGT-4690987951175987e-6