Logiweb dictionary of kvanti

Up Help

0	0	kvanti
1	0	lemma uniqueMember
2	0	lemma uniqueMember(Type)
3	0	lemma sameSeries
4	0	lemma a4
5	0	lemma sameMember
6	0	1rule Qclosed(Addition)
7	0	1rule Qclosed(Multiplication)
8	0	1rule fromCartProd(1)
9	0	1rule fromCartProd(2)
10	1	constantRationalSeries( {MissingArg} )
11	2	cartProd( {MissingArg} , {MissingArg} )
12	1	P( {MissingArg} )
13	2	binaryUnion( {MissingArg} , {MissingArg} )
14	0	setOfRationalSeries
15	2	isSubset( {MissingArg} , {MissingArg} )
16	2	(p {MissingArg} , {MissingArg} )
17	1	(s {MissingArg} )
18	0	cdots
19	0	object-var
20	0	ex-var
21	0	ph-var
22	0	vaerdi
23	0	variabel
24	1	op {MissingArg} end op
25	2	op2 {MissingArg} comma {MissingArg} end op2
26	2	define-equal {MissingArg} comma {MissingArg} end equal
27	1	contains-empty {MissingArg} end empty
28	1	Nat( {MissingArg} )
29	2	1deduction {MissingArg} conclude {MissingArg} end 1deduction
30	2	1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
31	3	1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
32	3	1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
33	3	1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
34	4	1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
35	4	1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
36	4	1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
37	3	1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
38	4	1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
39	4	1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
40	1	1deduction seven {MissingArg} end 1deduction
41	2	1deduction eight {MissingArg} bound {MissingArg} end 1deduction
42	2	1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
43	0	ex1
44	0	ex2
45	0	ex3
46	0	ex10
47	0	ex20
48	1	existential var {MissingArg} end var
49	1	{MissingArg} is existential var
50	4	exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
51	4	exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
52	4	exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
53	4	exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
54	0	ph1
55	0	ph2
56	0	ph3
57	1	placeholder-var {MissingArg} end var
58	1	{MissingArg} is placeholder-var
59	4	ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
60	4	ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
61	4	ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
62	4	ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
63	4	meta-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
64	4	meta-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
65	4	meta-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
66	0	var big set
67	0	object big set
68	0	meta big set
69	0	zermelo empty set
70	0	system Q
71	0	1rule mp
72	0	1rule gen
73	0	1rule repetition
74	0	1rule ad absurdum
75	0	1rule deduction
76	0	1rule exist intro
77	0	axiom extensionality
78	0	axiom empty set
79	0	axiom pair definition
80	0	axiom union definition
81	0	axiom power definition
82	0	axiom separation definition
83	0	prop lemma add double neg
84	0	prop lemma remove double neg
85	0	prop lemma and commutativity
86	0	prop lemma auto imply
87	0	prop lemma contrapositive
88	0	prop lemma first conjunct
89	0	prop lemma second conjunct
90	0	prop lemma from contradiction
91	0	prop lemma from disjuncts
92	0	prop lemma iff commutativity
93	0	prop lemma iff first
94	0	prop lemma iff second
95	0	prop lemma imply transitivity
96	0	prop lemma join conjuncts
97	0	prop lemma mp2
98	0	prop lemma mp3
99	0	prop lemma mp4
100	0	prop lemma mp5
101	0	prop lemma mt
102	0	prop lemma negative mt
103	0	prop lemma technicality
104	0	prop lemma weakening
105	0	prop lemma weaken or first
106	0	prop lemma weaken or second
107	0	lemma formula2pair
108	0	lemma pair2formula
109	0	lemma formula2union
110	0	lemma union2formula
111	0	lemma formula2separation
112	0	lemma separation2formula
113	0	lemma formula2power
114	0	lemma subset in power set
115	0	lemma power set is subset0
116	0	lemma power set is subset
117	0	lemma power set is subset0-switch
118	0	lemma power set is subset-switch
119	0	lemma set equality suff condition
120	0	lemma set equality suff condition(t)0
121	0	lemma set equality suff condition(t)
122	0	lemma set equality skip quantifier
123	0	lemma set equality nec condition
124	0	lemma reflexivity0
125	0	lemma reflexivity
126	0	lemma symmetry0
127	0	lemma symmetry
128	0	lemma transitivity0
129	0	lemma transitivity
130	0	lemma er is reflexive
131	0	lemma er is symmetric
132	0	lemma er is transitive
133	0	lemma empty set is subset
134	0	lemma member not empty0
135	0	lemma member not empty
136	0	lemma unique empty set0
137	0	lemma unique empty set
138	0	lemma ==Reflexivity
139	0	lemma ==Symmetry
140	0	lemma ==Transitivity0
141	0	lemma ==Transitivity
142	0	lemma transfer ~is0
143	0	lemma transfer ~is
144	0	lemma pair subset0
145	0	lemma pair subset1
146	0	lemma pair subset
147	0	lemma same pair
148	0	lemma same singleton
149	0	lemma union subset
150	0	lemma same union
151	0	lemma separation subset
152	0	lemma same separation
153	0	lemma same binary union
154	0	lemma intersection subset
155	0	lemma same intersection
156	0	lemma auto member
157	0	lemma eq-system not empty0
158	0	lemma eq-system not empty
159	0	lemma eq subset0
160	0	lemma eq subset
161	0	lemma equivalence nec condition0
162	0	lemma equivalence nec condition
163	0	lemma none-equivalence nec condition0
164	0	lemma none-equivalence nec condition1
165	0	lemma none-equivalence nec condition
166	0	lemma equivalence class is subset
167	0	lemma equivalence classes are disjoint
168	0	lemma all disjoint
169	0	lemma all disjoint-imply
170	0	lemma bs subset union(bs/r)
171	0	lemma union(bs/r) subset bs
172	0	lemma union(bs/r) is bs
173	0	theorem eq-system is partition
174	0	var x1
175	0	var x2
176	0	var y1
177	0	var y2
178	0	var v1
179	0	var v2
180	0	var v3
181	0	var v4
182	0	var v2n
183	0	var m1
184	0	var m2
185	0	var n1
186	0	var n2
187	0	var n3
188	0	var ep
189	0	var ep1
190	0	var ep2
191	0	var fep
192	0	var fx
193	0	var fy
194	0	var fz
195	0	var fu
196	0	var fv
197	0	var fw
198	0	var rx
199	0	var ry
200	0	var rz
201	0	var ru
202	0	var sx
203	0	var sx1
204	0	var sy
205	0	var sy1
206	0	var sz
207	0	var sz1
208	0	var su
209	0	var su1
210	0	var fxs
211	0	var fys
212	0	var crs1
213	0	var f1
214	0	var f2
215	0	var f3
216	0	var f4
217	0	var op1
218	0	var op2
219	0	var r1
220	0	var s1
221	0	var s2
222	0	meta x1
223	0	meta x2
224	0	meta y1
225	0	meta y2
226	0	meta v1
227	0	meta v2
228	0	meta v3
229	0	meta v4
230	0	meta v2n
231	0	meta m1
232	0	meta m2
233	0	meta n1
234	0	meta n2
235	0	meta n3
236	0	meta ep
237	0	meta ep1
238	0	meta ep2
239	0	meta fx
240	0	meta fy
241	0	meta fz
242	0	meta fu
243	0	meta fv
244	0	meta fw
245	0	meta fep
246	0	meta rx
247	0	meta ry
248	0	meta rz
249	0	meta ru
250	0	meta sx
251	0	meta sx1
252	0	meta sy
253	0	meta sy1
254	0	meta sz
255	0	meta sz1
256	0	meta su
257	0	meta su1
258	0	meta fxs
259	0	meta fys
260	0	meta f1
261	0	meta f2
262	0	meta f3
263	0	meta f4
264	0	meta op1
265	0	meta op2
266	0	meta r1
267	0	meta s1
268	0	meta s2
269	0	object ep
270	0	object crs1
271	0	object f1
272	0	object f2
273	0	object f3
274	0	object f4
275	0	object n1
276	0	object n2
277	0	object op1
278	0	object op2
279	0	object r1
280	0	object s1
281	0	object s2
282	0	ph4
283	0	ph5
284	0	ph6
285	0	NAT
286	0	RATIONAL_SERIES
287	0	SERIES
288	0	setOfReals
289	0	setOfFxs
290	0	N
291	0	Q
292	0	X
293	0	xs
294	0	xsF
295	0	ysF
296	0	us
297	0	usF
298	0	0
299	0	1
300	0	(-1)
301	0	2
302	0	3
303	0	1/2
304	0	1/3
305	0	2/3
306	0	0f
307	0	1f
308	0	00
309	0	01
310	0	(--01)
311	0	02
312	0	01//02
313	0	lemma plusAssociativity(R)
314	0	lemma plusAssociativity(R)XX
315	0	lemma plus0(R)
316	0	lemma negative(R)
317	0	lemma times1(R)
318	0	lemma lessAddition(R)
319	0	lemma plusCommutativity(R)
320	0	lemma leqAntisymmetry(R)
321	0	lemma leqTransitivity(R)
322	0	lemma leqAddition(R)
323	0	lemma distribution(R)
324	0	axiom a4
325	0	axiom induction
326	0	axiom equality
327	0	axiom eqLeq
328	0	axiom eqAddition
329	0	axiom eqMultiplication
330	0	axiom QisClosed(reciprocal)
331	0	lemma QisClosed(reciprocal)
332	0	axiom QisClosed(negative)
333	0	lemma QisClosed(negative)
334	0	axiom leqReflexivity
335	0	axiom leqAntisymmetry
336	0	axiom leqTransitivity
337	0	axiom leqTotality
338	0	axiom leqAddition
339	0	axiom leqMultiplication
340	0	axiom plusAssociativity
341	0	axiom plusCommutativity
342	0	axiom negative
343	0	axiom plus0
344	0	axiom timesAssociativity
345	0	axiom timesCommutativity
346	0	axiom reciprocal
347	0	axiom times1
348	0	axiom distribution
349	0	axiom 0not1
350	0	lemma eqLeq(R)
351	0	lemma timesAssociativity(R)
352	0	lemma timesCommutativity(R)
353	0	1rule adhoc sameR
354	0	lemma separation2formula(1)
355	0	lemma separation2formula(2)
356	0	axiom cauchy
357	0	axiom plusF
358	0	axiom reciprocalF
359	0	1rule from==
360	0	1rule to==
361	0	1rule fromInR
362	0	lemma plusR(Sym)
363	0	axiom reciprocalR
364	0	1rule lessMinus1(N)
365	0	axiom nonnegative(N)
366	0	axiom US0
367	0	1rule nextXS(upperBound)
368	0	1rule nextXS(noUpperBound)
369	0	1rule nextUS(upperBound)
370	0	1rule nextUS(noUpperBound)
371	0	1rule expZero
372	0	1rule expPositive
373	0	1rule expZero(R)
374	0	1rule expPositive(R)
375	0	1rule base(1/2)Sum zero
376	0	1rule base(1/2)Sum positive
377	0	1rule UStelescope zero
378	0	1rule UStelescope positive
379	0	1rule adhoc eqAddition(R)
380	0	1rule fromLimit
381	0	1rule toUpperBound
382	0	1rule fromUpperBound
383	0	axiom USisUpperBound
384	0	axiom 0not1(R)
385	0	1rule expUnbounded
386	0	1rule fromLeq(Advanced)(N)
387	0	1rule fromLeastUpperBound
388	0	1rule toLeastUpperBound
389	0	axiom XSisNotUpperBound
390	0	axiom ysFGreater
391	0	axiom ysFLess
392	0	1rule smallInverse
393	0	axiom natType
394	0	axiom rationalType
395	0	axiom seriesType
396	0	axiom max
397	0	axiom numerical
398	0	axiom numericalF
399	0	axiom memberOfSeries
400	0	prop lemma doubly conditioned join conjuncts
401	0	prop lemma imply negation
402	0	prop lemma tertium non datur
403	0	prop lemma from negated imply
404	0	prop lemma to negated imply
405	0	prop lemma from negated double imply
406	0	prop lemma from negated and
407	0	prop lemma from negated or
408	0	prop lemma to negated or
409	0	prop lemma from negations
410	0	prop lemma from three disjuncts
411	0	prop lemma from two times two disjuncts
412	0	prop lemma negate first disjunct
413	0	prop lemma negate second disjunct
414	0	prop lemma expand disjuncts
415	0	lemma set equality nec condition(1)
416	0	lemma set equality nec condition(2)
417	0	lemma lessLeq(R)
418	0	lemma memberOfSeries
419	0	lemma memberOfSeries(Type)
420	2	{MissingArg} ^ {MissingArg}
421	1	R( {MissingArg} )
422	1	--R( {MissingArg} )
423	1	1/ {MissingArg}
424	2	eq-system of {MissingArg} modulo {MissingArg}
425	2	intersection {MissingArg} comma {MissingArg} end intersection
426	2	[ {MissingArg} ; {MissingArg} ]
427	1	union {MissingArg} end union
428	2	binary-union {MissingArg} comma {MissingArg} end union
429	1	power {MissingArg} end power
430	1	zermelo singleton {MissingArg} end singleton
431	3	stateExpand( {MissingArg} , {MissingArg} , {MissingArg} )
432	1	extractSeries( {MissingArg} )
433	1	setOfSeries( {MissingArg} )
434	1	--Macro( {MissingArg} )
435	3	expandList( {MissingArg} , {MissingArg} , {MissingArg} )
436	1	**Macro( {MissingArg} )
437	1	++Macro( {MissingArg} )
438	1	<
439	1	||Macro( {MissingArg} )
440	1	01//Macro( {MissingArg} )
441	2	upperBound( {MissingArg} , {MissingArg} )
442	2	leastUpperBound( {MissingArg} , {MissingArg} )
443	2	base(1/2)Sum( {MissingArg} , {MissingArg} )
444	2	UStelescope( {MissingArg} , {MissingArg} )
445	1	( {MissingArg} )
446	1	|f {MissingArg} |
447	1	|r {MissingArg} |
448	2	limit( {MissingArg} , {MissingArg} )
449	1	U( {MissingArg} )
450	3	isOrderedPair( {MissingArg} , {MissingArg} , {MissingArg} )
451	3	isRelation( {MissingArg} , {MissingArg} , {MissingArg} )
452	3	isFunction( {MissingArg} , {MissingArg} , {MissingArg} )
453	2	isSeries( {MissingArg} , {MissingArg} )
454	1	isNatural( {MissingArg} )
455	2	(o {MissingArg} , {MissingArg} )
456	1	typeNat( {MissingArg} )
457	1	typeNat0( {MissingArg} )
458	1	typeRational( {MissingArg} )
459	1	typeRational0( {MissingArg} )
460	2	typeSeries( {MissingArg} , {MissingArg} )
461	2	typeSeries0( {MissingArg} , {MissingArg} )
462	2	zermelo pair {MissingArg} comma {MissingArg} end pair
463	2	zermelo ordered pair {MissingArg} comma {MissingArg} end pair
464	1	- {MissingArg}
465	1	-f {MissingArg}
466	1	-- {MissingArg}
467	1	1f/ {MissingArg}
468	1	01// {MissingArg}
469	3	{MissingArg} is related to {MissingArg} under {MissingArg}
470	2	{MissingArg} is reflexive relation in {MissingArg}
471	2	{MissingArg} is symmetric relation in {MissingArg}
472	2	{MissingArg} is transitive relation in {MissingArg}
473	2	{MissingArg} is equivalence relation in {MissingArg}
474	3	equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
475	2	{MissingArg} is partition of {MissingArg}
476	2	{MissingArg} * {MissingArg}
477	2	{MissingArg} *f {MissingArg}
478	2	{MissingArg} ** {MissingArg}
479	2	{MissingArg} + {MissingArg}
480	2	{MissingArg} - {MissingArg}
481	2	{MissingArg} +f {MissingArg}
482	2	{MissingArg} -f {MissingArg}
483	2	{MissingArg} ++ {MissingArg}
484	2	R( {MissingArg} ) -- R( {MissingArg} )
485	2	{MissingArg} in0 {MissingArg}
486	1	| {MissingArg} |
487	3	if( {MissingArg} , {MissingArg} , {MissingArg} )
488	2	max( {MissingArg} , {MissingArg} )
489	2	maxR( {MissingArg} , {MissingArg} )
490	2	{MissingArg} = {MissingArg}
491	2	{MissingArg} != {MissingArg}
492	2	{MissingArg} <= {MissingArg}
493	2	{MissingArg} < {MissingArg}
494	2	{MissingArg}
495	2	{MissingArg} <=f {MissingArg}
496	2	{MissingArg} sameF {MissingArg}
497	2	{MissingArg} == {MissingArg}
498	2	{MissingArg} !!== {MissingArg}
499	2	{MissingArg} << {MissingArg}
500	2	{MissingArg} <<== {MissingArg}
501	2	{MissingArg} zermelo is {MissingArg}
502	2	{MissingArg} is subset of {MissingArg}
503	1	not0 {MissingArg}
504	2	{MissingArg} zermelo ~in {MissingArg}
505	2	{MissingArg} zermelo ~is {MissingArg}
506	2	{MissingArg} and0 {MissingArg}
507	2	{MissingArg} or0 {MissingArg}
508	2	exist0 {MissingArg} indeed {MissingArg}
509	2	{MissingArg} iff {MissingArg}
510	2	the set of ph in {MissingArg} such that {MissingArg} end set