Logiweb dictionary of ijcar base

Up Help

0	0	ijcar base
1	2	proclaim * as * end proclaim
2	1	unicode start of text * end unicode text
3	0	unicode end of text
4	2	* then *
5	3	* begin * end *
6	2	preassociative * greater than *
7	2	postassociative * greater than *
8	2	priority * equal *
9	1	priority * end priority
10	1	unicode newline *
11	0	x
12	1	text * end text
13	2	text * plus *
14	2	text * plus indent *
15	1	bracket * end bracket
16	1	big bracket * end bracket
17	1	math * end math
18	1	flush left * end left
19	0	var x
20	0	var y
21	0	var z
22	3	define * of * as * end define
23	0	pyk
24	0	tex
25	0	tex name
26	0	priority
27	0	true
28	3	if * then * else * end if
29	3	introduce * of * as * end introduce
30	0	value
31	0	claim
32	1	unicode space *
33	1	unicode exclamation mark *
34	1	unicode quotation mark *
35	1	unicode number sign *
36	1	unicode dollar sign *
37	1	unicode percent *
38	1	unicode ampersand *
39	1	unicode apostrophe *
40	1	unicode left parenthesis *
41	1	unicode right parenthesis *
42	1	unicode asterisk *
43	1	unicode plus sign *
44	1	unicode comma *
45	1	unicode hyphen *
46	1	unicode period *
47	1	unicode slash *
48	1	unicode zero *
49	1	unicode one *
50	1	unicode two *
51	1	unicode three *
52	1	unicode four *
53	1	unicode five *
54	1	unicode six *
55	1	unicode seven *
56	1	unicode eight *
57	1	unicode nine *
58	1	unicode colon *
59	1	unicode semicolon *
60	1	unicode less than *
61	1	unicode equal sign *
62	1	unicode greater than *
63	1	unicode question mark *
64	1	unicode commercial at *
65	1	unicode capital a *
66	1	unicode capital b *
67	1	unicode capital c *
68	1	unicode capital d *
69	1	unicode capital e *
70	1	unicode capital f *
71	1	unicode capital g *
72	1	unicode capital h *
73	1	unicode capital i *
74	1	unicode capital j *
75	1	unicode capital k *
76	1	unicode capital l *
77	1	unicode capital m *
78	1	unicode capital n *
79	1	unicode capital o *
80	1	unicode capital p *
81	1	unicode capital q *
82	1	unicode capital r *
83	1	unicode capital s *
84	1	unicode capital t *
85	1	unicode capital u *
86	1	unicode capital v *
87	1	unicode capital w *
88	1	unicode capital x *
89	1	unicode capital y *
90	1	unicode capital z *
91	1	unicode left bracket *
92	1	unicode backslash *
93	1	unicode right bracket *
94	1	unicode circumflex *
95	1	unicode underscore *
96	1	unicode grave accent *
97	1	unicode small a *
98	1	unicode small b *
99	1	unicode small c *
100	1	unicode small d *
101	1	unicode small e *
102	1	unicode small f *
103	1	unicode small g *
104	1	unicode small h *
105	1	unicode small i *
106	1	unicode small j *
107	1	unicode small k *
108	1	unicode small l *
109	1	unicode small m *
110	1	unicode small n *
111	1	unicode small o *
112	1	unicode small p *
113	1	unicode small q *
114	1	unicode small r *
115	1	unicode small s *
116	1	unicode small t *
117	1	unicode small u *
118	1	unicode small v *
119	1	unicode small w *
120	1	unicode small x *
121	1	unicode small y *
122	1	unicode small z *
123	1	unicode left brace *
124	1	unicode vertical line *
125	1	unicode right brace *
126	1	unicode tilde *
127	0	bottom
128	1	function f of * end function
129	1	identity * end identity
130	0	false
131	0	untagged zero
132	0	untagged one
133	0	untagged two
134	0	untagged three
135	0	untagged four
136	0	untagged five
137	0	untagged six
138	0	untagged seven
139	0	untagged eight
140	0	untagged nine
141	0	zero
142	0	one
143	0	two
144	0	three
145	0	four
146	0	five
147	0	six
148	0	seven
149	0	eight
150	0	nine
151	0	var a
152	0	var b
153	0	var c
154	0	var d
155	0	var e
156	0	var f
157	0	var g
158	0	var h
159	0	var i
160	0	var j
161	0	var k
162	0	var l
163	0	var m
164	0	var n
165	0	var o
166	0	var p
167	0	var q
168	0	var r
169	0	var s
170	0	var t
171	0	var u
172	0	var v
173	0	var w
174	1	tagged parenthesis * end tagged
175	3	tagged if * then * else * end if
176	2	array * is * end array
177	0	left
178	0	center
179	0	right
180	0	empty
181	3	substitute * set * to * end substitute
182	1	map tag * end tag
183	1	raw map untag * end untag
184	1	map untag * end untag
185	1	normalizing untag * end untag
186	2	apply * to * end apply
187	2	apply one * to * end apply
188	1	identifier * end identifier
189	2	identifier one * plus id * end identifier
190	2	array plus * and * end plus
191	3	array remove * array * level * end remove
192	4	array put * value * array * level * end put
193	5	array add * value * index * value * level * end add
194	2	bit * of * end bit
195	2	bit one * of * end bit
196	0	example rack
197	0	vector hook
198	0	bibliography hook
199	0	dictionary hook
200	0	body hook
201	0	codex hook
202	0	expansion hook
203	0	code hook
204	0	cache hook
205	0	diagnose hook
206	0	pyk aspect
207	0	tex aspect
208	0	texname aspect
209	0	value aspect
210	0	message aspect
211	0	macro aspect
212	0	definition aspect
213	0	unpack aspect
214	0	claim aspect
215	0	priority aspect
216	0	lambda identifier
217	0	apply identifier
218	0	true identifier
219	0	if identifier
220	0	quote identifier
221	0	proclaim identifier
222	0	define identifier
223	0	introduce identifier
224	0	hide identifier
225	0	pre identifier
226	0	post identifier
227	3	eval * stack * cache * end eval
228	5	eval two * ref * id * stack * cache * end eval
229	4	eval three * function * stack * cache * end eval
230	4	eval four * arguments * stack * cache * end eval
231	3	lookup * stack * default * end lookup
232	4	abstract * term * stack * cache * end abstract
233	1	quote * end quote
234	3	expand * state * cache * end expand
235	4	expand two * definition * state * cache * end expand
236	3	expand list * state * cache * end expand
237	0	macro
238	0	macro state
239	2	zip * with * end zip
240	3	assoc one * address * index * end assoc
241	1	protect * end protect
242	0	self
243	2	macro define * as * end define
244	2	value define * as * end define
245	2	intro define * as * end define
246	2	pyk define * as * end define
247	2	tex define * as * end define
248	2	tex name define * as * end define
249	1	priority table * end table
250	0	macro define one
251	1	macro define two * end define
252	1	macro define three * end define
253	4	macro define four * state * cache * definition * end define
254	3	state expand * state * cache * end expand
255	3	quote expand * term * stack * end expand
256	3	quote expand two * term * stack * end expand
257	4	quote expand three * term * stack * value * end expand
258	3	quote expand star * term * stack * end expand
259	1	parenthesis * end parenthesis
260	1	big parenthesis * end parenthesis
261	1	display * end display
262	1	statement * end statement
263	1	spying test * end test
264	1	false spying test * end test
265	2	aspect * subcodex * end aspect
266	3	aspect * term * cache * end aspect
267	1	tuple * end tuple
268	1	tuple one * end tuple
269	1	tuple two * end tuple
270	2	let two * apply * end let
271	2	let one * apply * end let
272	2	claim define * as * end define
273	0	checker
274	2	check * cache * end check
275	3	check two * cache * def * end check
276	3	check three * cache * def * end check
277	2	check list * cache * end check
278	3	check list two * cache * value * end check
279	1	test * end test
280	1	false test * end test
281	1	raw test * end test
282	0	message
283	2	message define * as * end define
284	0	the statement aspect
285	0	statement
286	2	statement define * as * end define
287	0	example axiom
288	0	example scheme
289	0	example rule
290	0	absurdity
291	0	contraexample
292	0	example theory primed
293	0	example lemma
294	1	metavar * end metavar
295	0	meta a
296	0	meta b
297	0	meta c
298	0	meta d
299	0	meta e
300	0	meta f
301	0	meta g
302	0	meta h
303	0	meta i
304	0	meta j
305	0	meta k
306	0	meta l
307	0	meta m
308	0	meta n
309	0	meta o
310	0	meta p
311	0	meta q
312	0	meta r
313	0	meta s
314	0	meta t
315	0	meta u
316	0	meta v
317	0	meta w
318	0	meta x
319	0	meta y
320	0	meta z
321	3	sub * set * to * end sub
322	3	sub star * set * to * end sub
323	0	the empty set
324	0	example remainder
325	1	make visible * end visible
326	4	intro * index * pyk * tex * end intro
327	3	intro * pyk * tex * end intro
328	2	error * term * end error
329	2	error two * term * end error
330	3	proof * term * cache * end proof
331	2	proof two * term * end proof
332	2	sequent eval * term * end eval
333	2	seqeval init * term * end eval
334	2	seqeval modus * term * end eval
335	3	seqeval modus one * term * sequent * end eval
336	2	seqeval verify * term * end eval
337	3	seqeval verify one * term * sequent * end eval
338	2	sequent eval plus * term * end eval
339	3	seqeval plus one * term * sequent * end eval
340	2	seqeval minus * term * end eval
341	3	seqeval minus one * term * sequent * end eval
342	2	seqeval deref * term * end eval
343	3	seqeval deref one * term * sequent * end eval
344	4	seqeval deref two * term * sequent * def * end eval
345	2	seqeval at * term * end eval
346	3	seqeval at one * term * sequent * end eval
347	2	seqeval infer * term * end eval
348	4	seqeval infer one * term * premise * sequent * end eval
349	2	seqeval endorse * term * end eval
350	4	seqeval endorse one * term * side * sequent * end eval
351	2	seqeval est * term * end eval
352	4	seqeval est one * term * name * sequent * end eval
353	5	seqeval est two * term * name * sequent * def * end eval
354	2	seqeval all * term * end eval
355	4	seqeval all one * term * variable * sequent * end eval
356	2	seqeval cut * term * end eval
357	3	seqeval cut one * term * forerunner * end eval
358	4	seqeval cut two * term * forerunner * sequent * end eval
359	1	computably true * end true
360	3	claims * cache * ref * end claims
361	3	claims two * cache * ref * end claims
362	0	the proof aspect
363	0	proof
364	2	lemma * says * end lemma
365	2	proof of * reads * end proof
366	3	in theory * lemma * says * end lemma
367	3	in theory * antilemma * says * end antilemma
368	3	in theory * rule * says * end rule
369	3	in theory * antirule * says * end antirule
370	0	verifier
371	1	verify one * end verify
372	2	verify two * proofs * end verify
373	4	verify three * ref * sequents * diagnose * end verify
374	2	verify four * premises * end verify
375	4	verify five * ref * array * sequents * end verify
376	4	verify six * ref * list * sequents * end verify
377	4	verify seven * ref * id * sequents * end verify
378	2	cut * and * end cut
379	1	head * end head
380	1	tail * end tail
381	2	rule one * theory * end rule
382	2	rule * subcodex * end rule
383	0	rule tactic
384	2	plus * and * end plus
385	1	theory * end theory
386	2	theory two * cache * end theory
387	2	theory three * name * end theory
388	3	theory four * name * sum * end theory
389	0	example axiom lemma primed
390	0	example scheme lemma primed
391	0	example rule lemma primed
392	0	contraexample lemma primed
393	0	example axiom lemma
394	0	example scheme lemma
395	0	example rule lemma
396	0	contraexample lemma
397	0	example theory
398	0	ragged right
399	0	ragged right expansion
400	3	parameter term * stack * seed * end parameter
401	3	parameter term star * stack * seed * end parameter
402	2	instantiate * with * end instantiate
403	2	instantiate star * with * end instantiate
404	3	occur * in * substitution * end occur
405	3	occur star * in * substitution * end occur
406	3	unify * with * substitution * end unify
407	3	unify star * with * substitution * end unify
408	3	unify two * with * substitution * end unify
409	0	ell a
410	0	ell b
411	0	ell c
412	0	ell d
413	0	ell e
414	0	ell f
415	0	ell g
416	0	ell h
417	0	ell i
418	0	ell j
419	0	ell k
420	0	ell l
421	0	ell m
422	0	ell n
423	0	ell o
424	0	ell p
425	0	ell q
426	0	ell r
427	0	ell s
428	0	ell t
429	0	ell u
430	0	ell v
431	0	ell w
432	0	ell x
433	0	ell y
434	0	ell z
435	0	ell big a
436	0	ell big b
437	0	ell big c
438	0	ell big d
439	0	ell big e
440	0	ell big f
441	0	ell big g
442	0	ell big h
443	0	ell big i
444	0	ell big j
445	0	ell big k
446	0	ell big l
447	0	ell big m
448	0	ell big n
449	0	ell big o
450	0	ell big p
451	0	ell big q
452	0	ell big r
453	0	ell big s
454	0	ell big t
455	0	ell big u
456	0	ell big v
457	0	ell big w
458	0	ell big x
459	0	ell big y
460	0	ell big z
461	0	ell dummy
462	0	sequent reflexivity
463	0	tactic reflexivity
464	0	sequent commutativity
465	0	tactic commutativity
466	0	the tactic aspect
467	0	tactic
468	2	tactic define * as * end define
469	3	proof expand * state * cache * end expand
470	3	proof expand list * state * cache * end expand
471	0	proof state
472	2	conclude one * cache * end conclude
473	3	conclude two * proves * cache * end conclude
474	4	conclude three * proves * lemma * substitution * end conclude
475	2	conclude four * lemma * end conclude
476	2	* sub * end sub
477	5	* intro * index * pyk * tex * end intro
478	4	* intro * pyk * tex * end intro
479	6	* intro * index * pyk * tex * name * end intro
480	5	* intro * pyk * tex * name * end intro
481	1	* prime
482	2	* assoc * end assoc
483	3	* set * to * end set
484	3	* set multi * to * end set
485	1	* bit nil
486	1	* bit one
487	0	binary
488	2	* color * end color
489	2	* color star * end color
490	1	* raw head
491	1	* raw tail
492	1	* cardinal untag
493	1	* head
494	1	* tail
495	1	* is singular
496	1	* is cardinal
497	1	* is data
498	1	* is atomic
499	1	* cardinal retract
500	1	* tagged retract
501	1	* boolean retract
502	1	* ref
503	1	* id
504	1	* debug
505	1	* root
506	1	* zeroth
507	1	* first
508	1	* second
509	1	* third
510	1	* fourth
511	1	* fifth
512	1	* sixth
513	1	* seventh
514	1	* eighth
515	1	* ninth
516	1	* is error
517	1	* is metavar
518	1	* is metaclosed
519	1	* is metaclosed star
520	1	newline *
521	1	macro newline *
522	2	* apply *
523	2	* tagged apply *
524	2	* times *
525	2	* times zero *
526	2	* plus *
527	2	* plus zero *
528	2	* plus one *
529	2	* minus *
530	2	* minus zero *
531	2	* minus one *
532	2	* term plus * end plus
533	2	* term union *
534	2	* term minus * end minus
535	2	* raw pair *
536	2	* eager pair *
537	2	* tagged pair *
538	2	* untagged double *
539	2	* pair *
540	2	* double *
541	2	* comma *
542	2	* boolean equal *
543	2	* data equal *
544	2	* cardinal equal *
545	2	* peano equal *
546	2	* tagged equal *
547	2	* math equal *
548	2	* reduce to *
549	2	* term equal *
550	2	* term list equal *
551	2	* term root equal *
552	2	* term in *
553	2	* term subset *
554	2	* term set equal *
555	2	* sequent equal *
556	2	* free in *
557	2	* free in star *
558	3	* free for * in *
559	3	* free for star * in *
560	2	* claim in *
561	2	* less *
562	2	* less zero *
563	2	* less one *
564	1	not *
565	2	* and *
566	2	* macro and *
567	2	* simple and *
568	2	* claim and *
569	2	* or *
570	2	* parallel *
571	2	* macro or *
572	2	* macro imply *
573	2	* guard *
574	2	* spy *
575	2	* tagged guard *
576	3	* select * else * end select
577	2	lambda * dot *
578	2	tagged lambda * dot *
579	1	tagging *
580	3	open if * then * else *
581	3	let * be * in *
582	3	let * abbreviate * in *
583	1	* init
584	1	* modus
585	1	* verify
586	1	* curry plus
587	1	* curry minus
588	1	* dereference
589	2	* at *
590	2	* modus ponens *
591	2	* modus probans *
592	2	* conclude *
593	2	* infer *
594	2	* endorse *
595	2	* id est *
596	2	all * indeed *
597	2	* rule plus *
598	2	* cut *
599	2	* proves *
600	3	* proof of * reads *
601	4	line * because * indeed * end line *
602	2	because * indeed * qed
603	3	line * premise * end line *
604	3	line * side condition * end line *
605	2	arbitrary * end line *
606	3	locally define * as * end line *
607	2	* tab *
608	2	* row *