Logiweb dictionary of eriksen

Up Help

0	0	eriksen
1	1	contains-empty {MissingArg} end empty
2	2	1deduction {MissingArg} conclude {MissingArg} end 1deduction
3	2	1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
4	3	1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
5	3	1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
6	3	1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
7	4	1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
8	4	1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
9	4	1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
10	3	1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
11	4	1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
12	4	1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
13	1	1deduction seven {MissingArg} end 1deduction
14	2	1deduction eight {MissingArg} bound {MissingArg} end 1deduction
15	2	1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
16	0	cdots
17	0	object-var
18	0	ex-var
19	0	ph-var
20	0	vaerdi
21	0	variabel
22	2	op2 {MissingArg} comma {MissingArg} end op2
23	1	op {MissingArg} end op
24	0	placeholder-var1
25	0	placeholder-var2
26	0	placeholder-var3
27	1	placeholder-var {MissingArg} end var
28	1	{MissingArg} is placeholder-var
29	4	ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
30	4	ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
31	4	ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
32	4	ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
33	1	existential var {MissingArg} end var
34	1	{MissingArg} is existential var
35	0	ex1
36	0	ex2
37	0	ex10
38	0	ex20
39	4	exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
40	4	exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
41	4	exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
42	4	exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
43	0	var big set
44	0	object big set
45	0	meta big set
46	0	system zf
47	0	1rule mp
48	0	1rule gen
49	0	1rule deduction
50	0	1rule ad absurdum
51	0	1rule repetition
52	0	1rule exist intro
53	0	axiom extensionality
54	0	axiom separation definition
55	0	axiom pair definition
56	0	axiom union definition
57	0	axiom power definition
58	0	axiom empty set
59	0	cheating axiom all disjoint
60	0	zermelo empty set
61	0	lemma separation2formula
62	0	lemma formula2separation
63	0	lemma equivalence nec condition0
64	0	lemma equivalence nec condition
65	0	lemma eq subset0
66	0	lemma eq subset
67	0	lemma set equality suff condition
68	0	prop lemma weakening
69	0	prop lemma negative mt
70	0	prop lemma mp2
71	0	prop lemma mp3
72	0	prop lemma mp4
73	0	prop lemma mp5
74	0	prop lemma technicality
75	0	prop lemma mt
76	0	prop lemma add double neg
77	0	prop lemma remove double neg
78	0	prop lemma and commutativity
79	0	prop lemma first conjunct
80	0	prop lemma second conjunct
81	0	prop lemma join conjuncts
82	0	prop lemma iff first
83	0	prop lemma iff second
84	0	prop lemma contrapositive
85	0	prop lemma from contradiction
86	0	lemma er is reflexive
87	0	lemma er is symmetric
88	0	lemma er is transitive
89	0	lemma reflexivity0
90	0	lemma reflexivity
91	0	lemma symmetry0
92	0	lemma symmetry
93	0	lemma transitivity0
94	0	lemma transitivity
95	0	lemma auto member
96	0	lemma set equality skip quantifier
97	0	lemma set equality nec condition
98	0	lemma empty set is subset
99	0	lemma unique empty set0
100	0	lemma unique empty set
101	0	lemma none-equivalence nec condition0
102	0	lemma none-equivalence nec condition1
103	0	lemma none-equivalence nec condition
104	0	prop lemma auto imply
105	0	prop lemma imply transitivity
106	0	lemma member not empty
107	0	lemma member not empty0
108	0	lemma =reflexivity
109	0	lemma =symmetry
110	0	lemma =transitivity0
111	0	lemma =transitivity
112	0	lemma formula2union
113	0	lemma union2formula
114	0	lemma subset transitive
115	0	lemma subset in power set
116	0	lemma power set is subset0
117	0	lemma power set is subset0-switch
118	0	lemma power set is subset
119	0	lemma power set is subset-switch
120	0	lemma equivalence class is subset
121	0	lemma bs subset union(bs/r)
122	0	lemma union(bs/r) subset bs
123	0	lemma union(bs/r) is bs
124	0	lemma eq-system not empty0
125	0	lemma eq-system not empty
126	0	prop lemma weaken or first
127	0	prop lemma weaken or second
128	0	prop lemma from disjuncts
129	0	prop lemma iff commutativity
130	0	lemma pair2formula
131	0	lemma set equality suff condition(t)0
132	0	lemma set equality suff condition(t)
133	0	lemma formula2pair
134	0	lemma pair subset0
135	0	lemma pair subset1
136	0	lemma pair subset
137	0	lemma same pair
138	0	lemma same singleton
139	0	lemma union subset
140	0	lemma same union
141	0	lemma separation subset
142	0	lemma same binary union
143	0	lemma same separation
144	0	lemma intersection subset
145	0	lemma same intersection
146	0	lemma equivalence classes are disjoint
147	0	lemma transfer ~is0
148	0	lemma transfer ~is
149	0	lemma all disjoint
150	0	lemma all disjoint-imply
151	0	theorem eq-system is partition
152	2	intersection {MissingArg} comma {MissingArg} end intersection
153	2	eq-system of {MissingArg} modulo {MissingArg}
154	1	union {MissingArg} end union
155	1	power {MissingArg} end power
156	2	binary-union {MissingArg} comma {MissingArg} end union
157	1	zermelo singleton {MissingArg} end singleton
158	2	{MissingArg} zermelo pair {MissingArg}
159	2	{MissingArg} zermelo ordered pair {MissingArg}
160	2	{MissingArg} zermelo in {MissingArg}
161	2	{MissingArg} zermelo ~in {MissingArg}
162	2	{MissingArg} is partition of {MissingArg}
163	3	{MissingArg} is related to {MissingArg} under {MissingArg}
164	2	{MissingArg} is reflexive relation in {MissingArg}
165	2	{MissingArg} is symmetric relation in {MissingArg}
166	2	{MissingArg} is transitive relation in {MissingArg}
167	2	{MissingArg} is equivalence relation in {MissingArg}
168	3	equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
169	2	{MissingArg} zermelo is {MissingArg}
170	2	{MissingArg} is subset of {MissingArg}
171	1	not0 {MissingArg}
172	2	{MissingArg} zermelo ~is {MissingArg}
173	2	{MissingArg} and0 {MissingArg}
174	2	{MissingArg} or0 {MissingArg}
175	2	{MissingArg} iff {MissingArg}
176	2	the set of ph in {MissingArg} such that {MissingArg} end set