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