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