Logiweb codex of am in pyk
Up
Help
ref-0-id-0
am
ref-0-id-1
cdots
ref-0-id-2
object-var
ref-0-id-3
ex-var
ref-0-id-4
ph-var
ref-0-id-5
vaerdi
ref-0-id-6
variabel
ref-0-id-7
op {MissingArg} end op
ref-0-id-8
op2 {MissingArg} comma {MissingArg} end op2
ref-0-id-9
define-equal {MissingArg} comma {MissingArg} end equal
ref-0-id-10
contains-empty {MissingArg} end empty
ref-0-id-11
1deduction {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-12
1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-13
1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-14
1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-15
1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-16
1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-17
1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-18
1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-19
1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-20
1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-21
1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-22
1deduction seven {MissingArg} end 1deduction
ref-0-id-23
1deduction eight {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-24
1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-25
ex1
ref-0-id-26
ex2
ref-0-id-27
ex3
ref-0-id-28
ex10
ref-0-id-29
ex20
ref-0-id-30
existential var {MissingArg} end var
ref-0-id-31
{MissingArg} is existential var
ref-0-id-32
exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-33
exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-34
exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-35
exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-36
placeholder-var1
ref-0-id-37
placeholder-var2
ref-0-id-38
placeholder-var3
ref-0-id-39
placeholder-var {MissingArg} end var
ref-0-id-40
{MissingArg} is placeholder-var
ref-0-id-41
ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-42
ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-43
ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-44
ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-45
var big set
ref-0-id-46
object big set
ref-0-id-47
meta big set
ref-0-id-48
zermelo empty set
ref-0-id-49
system Q
ref-0-id-50
1rule mp
ref-0-id-51
1rule gen
ref-0-id-52
1rule repetition
ref-0-id-53
1rule ad absurdum
ref-0-id-54
1rule deduction
ref-0-id-55
1rule exist intro
ref-0-id-56
axiom extensionality
ref-0-id-57
axiom empty set
ref-0-id-58
axiom pair definition
ref-0-id-59
axiom union definition
ref-0-id-60
axiom power definition
ref-0-id-61
axiom separation definition
ref-0-id-62
prop lemma add double neg
ref-0-id-63
prop lemma remove double neg
ref-0-id-64
prop lemma and commutativity
ref-0-id-65
prop lemma auto imply
ref-0-id-66
prop lemma contrapositive
ref-0-id-67
prop lemma first conjunct
ref-0-id-68
prop lemma second conjunct
ref-0-id-69
prop lemma from contradiction
ref-0-id-70
prop lemma from disjuncts
ref-0-id-71
prop lemma iff commutativity
ref-0-id-72
prop lemma iff first
ref-0-id-73
prop lemma iff second
ref-0-id-74
prop lemma imply transitivity
ref-0-id-75
prop lemma join conjuncts
ref-0-id-76
prop lemma mp2
ref-0-id-77
prop lemma mp3
ref-0-id-78
prop lemma mp4
ref-0-id-79
prop lemma mp5
ref-0-id-80
prop lemma mt
ref-0-id-81
prop lemma negative mt
ref-0-id-82
prop lemma technicality
ref-0-id-83
prop lemma weakening
ref-0-id-84
prop lemma weaken or first
ref-0-id-85
prop lemma weaken or second
ref-0-id-86
lemma formula2pair
ref-0-id-87
lemma pair2formula
ref-0-id-88
lemma formula2union
ref-0-id-89
lemma union2formula
ref-0-id-90
lemma formula2separation
ref-0-id-91
lemma separation2formula
ref-0-id-92
lemma subset in power set
ref-0-id-93
lemma power set is subset0
ref-0-id-94
lemma power set is subset
ref-0-id-95
lemma power set is subset0-switch
ref-0-id-96
lemma power set is subset-switch
ref-0-id-97
lemma set equality suff condition
ref-0-id-98
lemma set equality suff condition(t)0
ref-0-id-99
lemma set equality suff condition(t)
ref-0-id-100
lemma set equality skip quantifier
ref-0-id-101
lemma set equality nec condition
ref-0-id-102
lemma reflexivity0
ref-0-id-103
lemma reflexivity
ref-0-id-104
lemma symmetry0
ref-0-id-105
lemma symmetry
ref-0-id-106
lemma transitivity0
ref-0-id-107
lemma transitivity
ref-0-id-108
lemma er is reflexive
ref-0-id-109
lemma er is symmetric
ref-0-id-110
lemma er is transitive
ref-0-id-111
lemma empty set is subset
ref-0-id-112
lemma member not empty0
ref-0-id-113
lemma member not empty
ref-0-id-114
lemma unique empty set0
ref-0-id-115
lemma unique empty set
ref-0-id-116
lemma ==Reflexivity
ref-0-id-117
lemma ==Symmetry
ref-0-id-118
lemma ==Transitivity0
ref-0-id-119
lemma ==Transitivity
ref-0-id-120
lemma transfer ~is0
ref-0-id-121
lemma transfer ~is
ref-0-id-122
lemma pair subset0
ref-0-id-123
lemma pair subset1
ref-0-id-124
lemma pair subset
ref-0-id-125
lemma same pair
ref-0-id-126
lemma same singleton
ref-0-id-127
lemma union subset
ref-0-id-128
lemma same union
ref-0-id-129
lemma separation subset
ref-0-id-130
lemma same separation
ref-0-id-131
lemma same binary union
ref-0-id-132
lemma intersection subset
ref-0-id-133
lemma same intersection
ref-0-id-134
lemma auto member
ref-0-id-135
lemma eq-system not empty0
ref-0-id-136
lemma eq-system not empty
ref-0-id-137
lemma eq subset0
ref-0-id-138
lemma eq subset
ref-0-id-139
lemma equivalence nec condition0
ref-0-id-140
lemma equivalence nec condition
ref-0-id-141
lemma none-equivalence nec condition0
ref-0-id-142
lemma none-equivalence nec condition1
ref-0-id-143
lemma none-equivalence nec condition
ref-0-id-144
lemma equivalence class is subset
ref-0-id-145
lemma equivalence classes are disjoint
ref-0-id-146
lemma all disjoint
ref-0-id-147
lemma all disjoint-imply
ref-0-id-148
lemma bs subset union(bs/r)
ref-0-id-149
lemma union(bs/r) subset bs
ref-0-id-150
lemma union(bs/r) is bs
ref-0-id-151
theorem eq-system is partition
ref-0-id-152
var ep
ref-0-id-153
var fx
ref-0-id-154
var fy
ref-0-id-155
var fz
ref-0-id-156
var fu
ref-0-id-157
var fv
ref-0-id-158
var rx
ref-0-id-159
var ry
ref-0-id-160
var rz
ref-0-id-161
var ru
ref-0-id-162
meta ep
ref-0-id-163
meta fx
ref-0-id-164
meta fy
ref-0-id-165
meta fz
ref-0-id-166
meta fu
ref-0-id-167
meta fv
ref-0-id-168
meta rx
ref-0-id-169
meta ry
ref-0-id-170
meta rz
ref-0-id-171
meta ru
ref-0-id-172
0
ref-0-id-173
1
ref-0-id-174
(-1)
ref-0-id-175
2
ref-0-id-176
1/2
ref-0-id-177
0f
ref-0-id-178
1f
ref-0-id-179
00
ref-0-id-180
01
ref-0-id-181
axiom leqReflexivity
ref-0-id-182
axiom leqAntisymmetry
ref-0-id-183
axiom leqTransitivity
ref-0-id-184
axiom leqTotality
ref-0-id-185
axiom leqAddition
ref-0-id-186
axiom leqMultiplication
ref-0-id-187
axiom plusAssociativity
ref-0-id-188
axiom plusCommutativity
ref-0-id-189
axiom negative
ref-0-id-190
axiom plus0
ref-0-id-191
axiom timesAssociativity
ref-0-id-192
axiom timesCommutativity
ref-0-id-193
axiom reciprocal
ref-0-id-194
axiom times1
ref-0-id-195
axiom distribution
ref-0-id-196
axiom 0not1
ref-0-id-197
axiom equality
ref-0-id-198
axiom eqLeq
ref-0-id-199
axiom eqAddition
ref-0-id-200
axiom eqMultiplication
ref-0-id-201
lemma set equality nec condition(1)
ref-0-id-202
lemma set equality nec condition(2)
ref-0-id-203
1rule ifThenElse true
ref-0-id-204
1rule ifThenElse false
ref-0-id-205
1rule from=f
ref-0-id-206
1rule to=f
ref-0-id-207
1rule from
ref-0-id-208
1rule to
ref-0-id-209
axiom plusF
ref-0-id-210
axiom timesF
ref-0-id-211
axiom minusF
ref-0-id-212
axiom 0f
ref-0-id-213
axiom 1f
ref-0-id-214
1rule fromSameF
ref-0-id-215
1rule toSameF
ref-0-id-216
1rule to==XX
ref-0-id-217
1rule from==
ref-0-id-218
1rule to==
ref-0-id-219
1rule from<
ref-0-id-220
1rule from<
ref-0-id-221
1rule from<
ref-0-id-222
1rule to<
ref-0-id-223
1rule from<<
ref-0-id-224
1rule to<<
ref-0-id-225
1rule fromInR
ref-0-id-226
axiom plusR
ref-0-id-227
axiom timesR
ref-0-id-228
lemma leqAntisymmetry
ref-0-id-229
lemma leqTransitivity
ref-0-id-230
lemma leqAddition
ref-0-id-231
lemma leqMultiplication
ref-0-id-232
lemma reciprocal
ref-0-id-233
lemma equality
ref-0-id-234
lemma eqLeq
ref-0-id-235
lemma eqAddition
ref-0-id-236
lemma eqMultiplication
ref-0-id-237
prop lemma to negated imply
ref-0-id-238
prop lemma tertium non datur
ref-0-id-239
prop lemma imply negation
ref-0-id-240
prop lemma from negations
ref-0-id-241
prop lemma from three disjuncts
ref-0-id-242
prop lemma from two times two disjuncts
ref-0-id-243
prop lemma negate first disjunct
ref-0-id-244
prop lemma negate second disjunct
ref-0-id-245
prop lemma expand disjuncts
ref-0-id-246
lemma eqReflexivity
ref-0-id-247
lemma eqSymmetry
ref-0-id-248
lemma eqTransitivity
ref-0-id-249
lemma eqTransitivity4
ref-0-id-250
lemma eqTransitivity5
ref-0-id-251
lemma eqTransitivity6
ref-0-id-252
lemma plus0Left
ref-0-id-253
lemma times1Left
ref-0-id-254
lemma eqAdditionLeft
ref-0-id-255
lemma eqMultiplicationLeft
ref-0-id-256
lemma distributionOut
ref-0-id-257
lemma three2twoTerms
ref-0-id-258
lemma three2threeTerms
ref-0-id-259
lemma three2twoFactors
ref-0-id-260
lemma addEquations
ref-0-id-261
lemma subtractEquations
ref-0-id-262
lemma subtractEquationsLeft
ref-0-id-263
lemma eqNegated
ref-0-id-264
lemma positiveToRight(Eq)
ref-0-id-265
lemma positiveToLeft(Eq)(1 term)
ref-0-id-266
lemma negativeToLeft(Eq)
ref-0-id-267
lemma lessNeq
ref-0-id-268
lemma neqSymmetry
ref-0-id-269
lemma neqNegated
ref-0-id-270
lemma subNeqRight
ref-0-id-271
lemma subNeqLeft
ref-0-id-272
lemma neqAddition
ref-0-id-273
lemma neqMultiplication
ref-0-id-274
lemma uniqueNegative
ref-0-id-275
lemma doubleMinus
ref-0-id-276
lemma leqLessEq
ref-0-id-277
lemma lessLeq
ref-0-id-278
lemma from leqGeq
ref-0-id-279
lemma subLeqRight
ref-0-id-280
lemma subLeqLeft
ref-0-id-281
lemma leqPlus1
ref-0-id-282
lemma positiveToRight(Leq)
ref-0-id-283
lemma positiveToRight(Leq)(1 term)
ref-0-id-284
lemma negativeToLeft(Leq)
ref-0-id-285
lemma leqAdditionLeft
ref-0-id-286
lemma leqSubtraction
ref-0-id-287
lemma leqSubtractionLeft
ref-0-id-288
lemma thirdGeq
ref-0-id-289
lemma leqNegated
ref-0-id-290
lemma addEquations(Leq)
ref-0-id-291
lemma thirdGeqSeries
ref-0-id-292
lemma leqNeqLess
ref-0-id-293
lemma fromLess
ref-0-id-294
lemma toLess
ref-0-id-295
lemma fromNotLess
ref-0-id-296
lemma toNotLess
ref-0-id-297
lemma negativeLessPositive
ref-0-id-298
lemma leqLessTransitivity
ref-0-id-299
lemma lessLeqTransitivity
ref-0-id-300
lemma lessTransitivity
ref-0-id-301
lemma lessTotality
ref-0-id-302
lemma subLessRight
ref-0-id-303
lemma subLessLeft
ref-0-id-304
lemma lessAddition
ref-0-id-305
lemma lessAdditionLeft
ref-0-id-306
lemma lessMultiplication
ref-0-id-307
lemma lessMultiplicationLeft
ref-0-id-308
lemma lessDivision
ref-0-id-309
lemma addEquations(Less)
ref-0-id-310
lemma lessNegated
ref-0-id-311
lemma positiveNegated
ref-0-id-312
lemma nonpositiveNegated
ref-0-id-313
lemma negativeNegated
ref-0-id-314
lemma nonnegativeNegated
ref-0-id-315
lemma positiveHalved
ref-0-id-316
lemma nonnegativeNumerical
ref-0-id-317
lemma negativeNumerical
ref-0-id-318
lemma positiveNumerical
ref-0-id-319
lemma nonpositiveNumerical
ref-0-id-320
lemma |0|=0
ref-0-id-321
lemma 0<=|x|
ref-0-id-322
lemma sameNumerical
ref-0-id-323
lemma signNumerical(+)
ref-0-id-324
lemma signNumerical
ref-0-id-325
lemma numericalDifference
ref-0-id-326
lemma splitNumericalSumHelper
ref-0-id-327
lemma splitNumericalSum(++)
ref-0-id-328
lemma splitNumericalSum(--)
ref-0-id-329
lemma splitNumericalSum(+-, smallNegative)
ref-0-id-330
lemma splitNumericalSum(+-, bigNegative)
ref-0-id-331
lemma splitNumericalSum(+-)
ref-0-id-332
lemma splitNumericalSum(-+)
ref-0-id-333
lemma splitNumericalSum
ref-0-id-334
lemma insertMiddleTerm(Numerical)
ref-0-id-335
lemma x+y=zBackwards
ref-0-id-336
lemma x*y=zBackwards
ref-0-id-337
lemma x=x+(y-y)
ref-0-id-338
lemma x=x+y-y
ref-0-id-339
lemma x=x*y*(1/y)
ref-0-id-340
lemma insertMiddleTerm(Sum)
ref-0-id-341
lemma insertMiddleTerm(Difference)
ref-0-id-342
lemma x*0+x=x
ref-0-id-343
lemma x*0=0
ref-0-id-344
lemma (-1)*(-1)+(-1)*1=0
ref-0-id-345
lemma (-1)*(-1)=1
ref-0-id-346
lemma 0<1Helper
ref-0-id-347
lemma 0<1
ref-0-id-348
lemma 0<2
ref-0-id-349
lemma 0<1/2
ref-0-id-350
lemma x+x=2*x
ref-0-id-351
lemma (1/2)x+(1/2)x=x
ref-0-id-352
lemma -x-y=-(x+y)
ref-0-id-353
lemma minusNegated
ref-0-id-354
lemma times(-1)
ref-0-id-355
lemma times(-1)Left
ref-0-id-356
lemma -0=0
ref-0-id-357
lemma sameFsymmetry
ref-0-id-358
lemma sameFtransitivity
ref-0-id-359
lemma =f to sameF
ref-0-id-360
lemma plusF(Sym)
ref-0-id-361
lemma timesF(Sym)
ref-0-id-362
lemma f2R(Plus)
ref-0-id-363
lemma f2R(Times)
ref-0-id-364
lemma plusR(Sym)
ref-0-id-365
lemma timesR(Sym)
ref-0-id-366
lemma lessLeq(R)
ref-0-id-367
lemma eqLeq(R)
ref-0-id-368
lemma subLessRight(R)
ref-0-id-369
lemma subLessLeft(R)
ref-0-id-370
lemma <
ref-0-id-371
lemma <
ref-0-id-372
lemma <<==Reflexivity
ref-0-id-373
lemma <<==AntisymmetryHelper(Q)
ref-0-id-374
lemma <<==Antisymmetry
ref-0-id-375
lemma <<==Transitivity
ref-0-id-376
lemma plus0f
ref-0-id-377
lemma plus00
ref-0-id-378
lemma ==Addition
ref-0-id-379
lemma ==AdditionLeft
ref-0-id-380
lemma <
ref-0-id-381
lemma <<==Addition
ref-0-id-382
lemma plusAssociativity(F)
ref-0-id-383
lemma plusAssociativity(R)
ref-0-id-384
lemma negative(R)
ref-0-id-385
lemma plusCommutativity(F)
ref-0-id-386
lemma plusCommutativity(R)
ref-0-id-387
lemma timesAssociativity(F)
ref-0-id-388
lemma timesAssociativity(R)
ref-0-id-389
lemma times1f
ref-0-id-390
lemma times01
ref-0-id-391
lemma timesCommutativity(F)
ref-0-id-392
lemma timesCommutativity(R)
ref-0-id-393
lemma distribution(F)
ref-0-id-394
lemma distribution(R)
ref-0-id-395
R( {MissingArg} )
ref-0-id-396
--R( {MissingArg} )
ref-0-id-397
1/ {MissingArg}
ref-0-id-398
eq-system of {MissingArg} modulo {MissingArg}
ref-0-id-399
intersection {MissingArg} comma {MissingArg} end intersection
ref-0-id-400
[ {MissingArg} ; {MissingArg} ]
ref-0-id-401
union {MissingArg} end union
ref-0-id-402
binary-union {MissingArg} comma {MissingArg} end union
ref-0-id-403
power {MissingArg} end power
ref-0-id-404
zermelo singleton {MissingArg} end singleton
ref-0-id-405
zermelo pair {MissingArg} comma {MissingArg} end pair
ref-0-id-406
zermelo ordered pair {MissingArg} comma {MissingArg} end pair
ref-0-id-407
- {MissingArg}
ref-0-id-408
-f {MissingArg}
ref-0-id-409
{MissingArg} in0 {MissingArg}
ref-0-id-410
{MissingArg} is related to {MissingArg} under {MissingArg}
ref-0-id-411
{MissingArg} is reflexive relation in {MissingArg}
ref-0-id-412
{MissingArg} is symmetric relation in {MissingArg}
ref-0-id-413
{MissingArg} is transitive relation in {MissingArg}
ref-0-id-414
{MissingArg} is equivalence relation in {MissingArg}
ref-0-id-415
equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
ref-0-id-416
{MissingArg} is partition of {MissingArg}
ref-0-id-417
{MissingArg} * {MissingArg}
ref-0-id-418
{MissingArg} *f {MissingArg}
ref-0-id-419
{MissingArg} ** {MissingArg}
ref-0-id-420
{MissingArg} + {MissingArg}
ref-0-id-421
{MissingArg} - {MissingArg}
ref-0-id-422
{MissingArg} +f {MissingArg}
ref-0-id-423
{MissingArg} -f {MissingArg}
ref-0-id-424
{MissingArg} ++ {MissingArg}
ref-0-id-425
R( {MissingArg} ) -- R( {MissingArg} )
ref-0-id-426
| {MissingArg} |
ref-0-id-427
if( {MissingArg} , {MissingArg} , {MissingArg} )
ref-0-id-428
{MissingArg} = {MissingArg}
ref-0-id-429
{MissingArg} != {MissingArg}
ref-0-id-430
{MissingArg} <= {MissingArg}
ref-0-id-431
{MissingArg} < {MissingArg}
ref-0-id-432
{MissingArg} =f {MissingArg}
ref-0-id-433
{MissingArg}
ref-0-id-434
{MissingArg} sameF {MissingArg}
ref-0-id-435
{MissingArg} == {MissingArg}
ref-0-id-436
{MissingArg} << {MissingArg}
ref-0-id-437
{MissingArg} <<== {MissingArg}
ref-0-id-438
{MissingArg} zermelo is {MissingArg}
ref-0-id-439
{MissingArg} is subset of {MissingArg}
ref-0-id-440
not0 {MissingArg}
ref-0-id-441
{MissingArg} zermelo ~in {MissingArg}
ref-0-id-442
{MissingArg} zermelo ~is {MissingArg}
ref-0-id-443
{MissingArg} and0 {MissingArg}
ref-0-id-444
{MissingArg} or0 {MissingArg}
ref-0-id-445
{MissingArg} iff {MissingArg}
ref-0-id-446
the set of ph in {MissingArg} such that {MissingArg} end set
The pyk compiler
, version 0.grue.20060417+ by
Klaus Grue
,
GRD-2006-09-15.UTC:09:33:20.992497
=
MJD-53993.TAI:09:33:53.992497
=
LGT-4665029633992497e-6