$( set.mm - Version of 11-Mar-2010 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# Metamath source file for logic, set theory, numbers, and Hilbert space #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# ~~ PUBLIC DOMAIN ~~ This file is placed in the public domain per the Creative Commons Public Domain Dedication: http://creativecommons.org/licenses/publicdomain/ The public domain release applies worldwide. In case this is not legally possible, the right is granted to use the work for any purpose, without any conditions, unless such conditions are required by law. Norman Megill - http://us.metamath.org/email.html Contributor list: DA David Abernethy DH David Harvey JM Jeff Madsen SA Stefan Allan J2 Jeff Hoffman MO Mel L. O'Cat JA Juha Arpiainen SJ Szymon Jaroszewicz JO Jason Orendorff GB Gregory Bush GL Gerard Lang JP Josh Purinton PC Paul Chapman RL Raph Levien SR Steve Rodriguez SF Scott Fenton FL Frederic Line AS Alan Sare JH Jeffrey Hankins R2 Roy F. Longton ES Eric Schmidt =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Contents of this header =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 1. Recent label changes 2. Finding shorter proofs 3. Bibliography 4. Quick "How To" 5. Metamath syntax summary 6. Other notes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 1. Recent label changes =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= This is part of an ongoing project to improve naming consistency. If you are using an older version of set.mm as the base for your project, you should review the following changes before updating to this version. If you want to create an automated script, you can make can make global substitutions into your database by processing the ones *without* "Notes" in *reverse* order, starting backwards from the date of the set.mm version you used. When doing global substitutions, match a space or beginning-of-line before the label and a space or end-of-line after the label. The ones *with* "Notes" must be processed manually. If you have suggestions for better names, let me know. IMPORTANT: Except for general-purpose utility theorems, I often do not include label changes of theorems first added in the past year, because the current work in progress is subject to frequent changes. If you are using theorems from a new section being developed, let me know. Currently I do not include label changes in the Hilbert space or mathbox sections. Date Old New Notes 24-Jul-09 sandbox mathbox 12-Jun-09 mulge0 [--same--] rearranged antecedent 12-Jun-09 mulgt0 [--same--] rearranged antecedent 12-May-09 --- --- changed math symbol from "ZZ_>" to "ZZ>=" 2-May-09 snsspr snsspr1 2-May-09 axpow zfpow 2-May-09 axac zfac 2-May-09 axun zfun 27-Apr-09 pm4.22 bitr 24-Apr-09 axinf zfinf 24-Apr-09 zfinf zfinf2 2-Apr-09 infmssuzle [--same--] changed -. S = (/) to S =/= (/) 23-Mar-09 eqfnfvf --- obsolete; use eqfnfvf2 instead 23-Mar-09 ffnoprval ffnoprv 23-Mar-09 eqfnoprval eqfnoprv 23-Mar-09 fnoprval fnoprv 23-Mar-09 foprval foprv 23-Mar-09 oprvalres oprvres 23-Mar-09 oprssoprval oprssoprv 23-Mar-09 fnrnoprval fnrnoprv 23-Mar-09 fooprval fooprv 23-Mar-09 fnoprvalrn fnoprvrn 23-Mar-09 oprvalelrn oprvelrn 23-Mar-09 oprvalconst2 oprvconst2 23-Mar-09 oprvalex oprvex 23-Mar-09 symgoprval symgoprv 23-Mar-09 fnoprvalrn2 fnoprvrn2 22-Mar-09 icoshf icoshft 8-Mar-09 nnont nnon 7-Mar-09 eluzsubii eluzsubi 7-Mar-09 eluzaddii eluzaddi 7-Mar-09 divexp expdiv 7-Mar-09 recexp exprec 7-Mar-09 --- --- changed math symbol from "ZZ>" to "ZZ_>" 27-Feb-09 lediv23 [--same--] rearranged antecedent 27-Feb-09 ltdiv23 [--same--] rearranged antecedent 3-Jan-09 muln0 mulne0 3-Jan-09 vne0 vn0 3-Jan-09 n0 neq0 3-Jan-09 ne0 n0 3-Jan-09 ssne0 ssn0 3-Jan-09 onne0 onn0 3-Jan-09 dmsnne0 dmsnn0 3-Jan-09 rnsnne0 rnsnn0 3-Jan-09 1ne0 1n0 3-Jan-09 metne0 metn0 3-Jan-09 blne0 bln0 2-Jan-08 flrecl reflcl 30-Dec-08 letrdi letrd 30-Dec-08 lelttrdi lelttrd 30-Dec-08 ltletrdi ltletrd 30-Dec-08 lttrdi lttrd 29-Dec-08 hbnegi hbneg 29-Dec-08 hbnegdi hbnegd 29-Dec-08 hbsumi hbsum 29-Dec-08 hbsum1i hbsum1 28-Dec-08 negnei negne0i 28-Dec-08 negne0i negne0bi 28-Dec-08 lemul2 [--same--] rearranged antecedent 28-Dec-08 lemul1 [--same--] rearranged antecedent 28-Dec-08 ltmul2 [--same--] rearranged antecedent 28-Dec-08 ltmul1 [--same--] rearranged antecedent 28-Dec-08 ecdmn0 [--same--] changed -. ... = to =/= 27-Dec-08 divdiv24 [--same--] rearranged antecedent 27-Dec-08 divdiv13 [--same--] rearranged antecedent 27-Dec-08 divadddiv [--same--] rearranged antecedent 27-Dec-08 divdivdiv [--same--] rearranged antecedent 27-Dec-08 recndi recnd 27-Dec-08 divdivmul divdiv1 27-Dec-08 divdiv23 [--same--] rearranged antecedent 27-Dec-08 dmsnsn0 --- obsolete; use the more general dmsn0el 25-Dec-08 div12 [--same--] rearranged antecedent 25-Dec-08 div13 [--same--] rearranged antecedent 25-Dec-08 div23 [--same--] rearranged antecedent 25-Dec-08 expm1 expm1t 25-Dec-08 divmuldiv [--same--] rearranged antecedent 25-Dec-08 recexp [--same--] rearranged antecedent 25-Dec-08 expne0i [--same--] rearranged antecedent 25-Dec-08 expsub [--same--] rearranged antecedent 25-Dec-08 divexp [--same--] rearranged antecedent 21-Dec-08 imaun2 imaundir 21-Dec-08 imaun imaundi 19-Dec-08 sbhyp --- obsolete; use sbhypf 19-Dec-08 opelcog opelco2g 18-Dec-08 fsumspl fsumsplit 18-Dec-08 fsum0spl fsum0split 18-Dec-08 fsumshf fsumshft 18-Dec-08 fsumcons fsumconst 18-Dec-08 dmco2 dmco 17-Dec-08 --- --- the math token "Base" was changed to "BaseSet" 17-Dec-08 ssxpr --- obsolete; use ssxpb 17-Dec-08 nicodraw --- obsolete; use nic-ax 17-Dec-08 nicodmpraw --- obsolete; use nic-mp 17-Dec-08 3exbi 3exbii 17-Dec-08 relssdr relssdmrn 16-Dec-08 dfoprab4 dfoprab5s 16-Dec-08 dfoprab5 dfoprab4s 16-Dec-08 dffxxx dff2 16-Dec-08 dff4 dff3 16-Dec-08 dff3 dff4 16-Dec-08 dff4 dffxxx 16-Dec-08 dffunmo dffun6 16-Dec-08 dffun6 dffun7 16-Dec-08 dffun7 dffun8 16-Dec-08 dffun8 dffun9 16-Dec-08 dffunmof dffun6f 16-Dec-08 fnopabfv dffn5 16-Dec-08 fnforn dffn4 16-Dec-08 fnfrn dffn3 16-Dec-08 fnf dffn2 16-Dec-08 f1fvf dff13f 16-Dec-08 f1fv dff13 16-Dec-08 f11 dff12 16-Dec-08 f1ofv dff1o6 16-Dec-08 f1o5 dff1o5 16-Dec-08 f1o4 dff1o4 16-Dec-08 f1o3 dff1o3 16-Dec-08 f1o2 dff1o2 15-Dec-08 pm4.2d biidd 15-Dec-08 pm4.2 biid 15-Dec-08 pm4.1 con34b 15-Dec-08 bi2.15 con1b 15-Dec-08 bi2.03 con2b 15-Dec-08 a3d con4d 15-Dec-08 a3i con4i 13-Dec-08 2climnni 2climnn 13-Dec-08 2climnn0i 2climnn0 12-Dec-08 reeftlclti reeftlcl 12-Dec-08 eftlclti eftlcl 12-Dec-08 eftlexti eftlex 12-Dec-08 fnsmnti arisumi 12-Dec-08 nn0le2msqti nn0le2msqi 12-Dec-08 reccnvi reccnv 12-Dec-08 expcnvi expcnv 11-Dec-08 isummulc1i isummulc1 11-Dec-08 iserzgt0i iserzgt0 11-Dec-08 isumreclti isumrecl 11-Dec-08 isumclti isumcl 11-Dec-08 isumnn0nni isumnn0nn 11-Dec-08 isum1pi isum1p 11-Dec-08 isumnuli isumnul 11-Dec-08 isumclim5ti isumclim5 11-Dec-08 isumclim4ti isumclim4 11-Dec-08 isumclim3ti isumclim3 11-Dec-08 isumclim2ti isumclim2 11-Dec-08 isumclim2tfi isumclim2f 11-Dec-08 isum1climi isum1clim 11-Dec-08 isumclimti isumclim 11-Dec-08 isumval2ti isumval2 11-Dec-08 isumvalti isumval 11-Dec-08 cvgcmp3ceti cvgcmp3ce 11-Dec-08 iserzcmp0i iserzcmp0 11-Dec-08 iserzcmpi iserzcmp 11-Dec-08 climsqueeze2i climsqueeze2 11-Dec-08 climsqueezei climsqueeze 11-Dec-08 climcmpc1i climcmpc1 11-Dec-08 climcmpi climcmp 11-Dec-08 iserzmulc1i iserzmulc1 11-Dec-08 iserzexti iserzex 11-Dec-08 clim2serzti clim2serz 11-Dec-08 climsubc2i climsubc2 11-Dec-08 climsubi climsub 11-Dec-08 climmulc2i climmulc2 11-Dec-08 climmuli climmul 11-Dec-08 climaddc2i climaddc2 11-Dec-08 climaddc1i climaddc1 11-Dec-08 climaddi climadd 11-Dec-08 climge0i climge0 11-Dec-08 climrecli climrecl 11-Dec-08 climreui climreu 11-Dec-08 climeui climeu 11-Dec-08 climuniii climunii 11-Dec-08 climunii climuni 11-Dec-08 clm4ati clm4a 11-Dec-08 serzmulc1i serzmulc1 11-Dec-08 serzspliti serzsplit 11-Dec-08 serzcmp0i serzcmp0 11-Dec-08 serzcmpi serzcmp 11-Dec-08 serz1pi serz1p 11-Dec-08 serzreclti serzrecl 11-Dec-08 serzcl2ti serzcl2 11-Dec-08 ser1clti ser1cl 11-Dec-08 ser0clti ser0cl 11-Dec-08 serzclti serzcl 11-Dec-08 fsum4i fsum4 11-Dec-08 fsum3i fsum3 11-Dec-08 fsum2i fsum2 11-Dec-08 fsum0spli fsum0spl 11-Dec-08 fsumspli fsumspl 11-Dec-08 serzfsumi serzfsum 11-Dec-08 fsumserz2i fsumserz2 11-Dec-08 fsumserzi fsumserz 11-Dec-08 cvg1ii cvg1i 11-Dec-08 cvg1i cvg1 11-Dec-08 seqzres2i seqzres2 11-Dec-08 seqzresi seqzres 11-Dec-08 seqzresvali seqzresval 11-Dec-08 seqzcli seqzcl 11-Dec-08 seqzrni seqzrn 11-Dec-08 seqzrn2i seqzrn2 11-Dec-08 seqzeqi seqzeq 11-Dec-08 seqzfveqi seqzfveq 11-Dec-08 seqzval2ti seqzval2 11-Dec-08 seq01i seq01 11-Dec-08 seq0p1i seq0p1 11-Dec-08 seq00i seq00 11-Dec-08 seqzm1i seqzm1 11-Dec-08 seqzp1i seqzp1 11-Dec-08 seqz1i seqz1 11-Dec-08 seq0fni seq0fn 11-Dec-08 seq1seq0i seq1seq0 11-Dec-08 seq1seq0ti seq1seq01 11-Dec-08 seq1seq02ti seq1seq02 11-Dec-08 seq0seqzi seq0seqz 11-Dec-08 seq1seqzi seq1seqz 11-Dec-08 seqzvalti seqzval 11-Dec-08 seqzfni seqzfn 11-Dec-08 seqzfval2i seqzfval2 11-Dec-08 seqzfvali seqzfval 11-Dec-08 seq0valti seq0valt 11-Dec-08 seq0fvali seq0fval 11-Dec-08 seq1shftidi seq1shftid 11-Dec-08 shftidti shftidt 11-Dec-08 shftcan1ti shftcan1 11-Dec-08 shftcan2ti shftcan2 11-Dec-08 shftfi shftf 11-Dec-08 shftval5ti shftval5 11-Dec-08 shftval4ti shftval4 11-Dec-08 shftval3ti shftval3 11-Dec-08 shftval2ti shftval2 11-Dec-08 shftvalti shftval 11-Dec-08 shftresvalti shftresval 11-Dec-08 shftresi shftres 11-Dec-08 shftfni shftfn 11-Dec-08 shftfvali shftfval 11-Dec-08 seq1resi seq1res 11-Dec-08 seq1cl2i seq1cl2 11-Dec-08 seq1cli seq1cl 11-Dec-08 seq1f2i seq1f2 11-Dec-08 seq1fi seq1f 11-Dec-08 seq1rni seq1rn 11-Dec-08 seq1rn2i seq1rn2 11-Dec-08 seq1fni seq1fn 11-Dec-08 seq1m1i seq1m1 11-Dec-08 seq1p1i seq1p1 11-Dec-08 seq11i seq11 11-Dec-08 seq1val2i seq1val2 11-Dec-08 seq1vali seq1val 11-Dec-08 seq1rvali seq1rval 11-Dec-08 uznegi uzneg 9-Dec-08 nvelv vprc 9-Dec-08 inelv iprc 9-Dec-08 fipr fiprc 9-Dec-08 ecqs [--same--] eliminated redundant hypothesis A e. V 18-Nov-08 --- --- See mmnotes.txt entry of 18-Nov-2008 18-Nov-08 cdavalt cdaval 18-Nov-08 cdaval cdavali 18-Nov-08 unbnnt unbnn3 18-Nov-08 frsuct frsuc 18-Nov-08 fr0t fr0g 18-Nov-08 rdg0t rdg0g 18-Nov-08 ssonunit ssonuni 18-Nov-08 ssonuni ssonunii 18-Nov-08 eqtr3t eqtr3 18-Nov-08 eqtr2t eqtr2 18-Nov-08 eqtrt eqtr 18-Nov-08 3eqtr4r 3eqtr4ri 18-Nov-08 3eqtr3r 3eqtr3ri 18-Nov-08 3eqtr2r 3eqtr2ri 18-Nov-08 3eqtr4r 3eqtr4ri 18-Nov-08 3eqtr3r 3eqtr3ri 18-Nov-08 3bitr3r 3bitr3ri 18-Nov-08 3bitr4r 3bitr4ri 18-Nov-08 3bitr2r 3bitr2ri 18-Nov-08 biimpr biimpri 18-Nov-08 biimp biimpi 18-Nov-08 impbi impbii 18-Nov-08 --- --- See mmnotes.txt entry of 17-Nov-2008 17-Nov-08 --- --- Remember that substitutions are 17-Nov-08 --- --- made in _reverse_ order. 17-Nov-08 efi4pt efi4p 17-Nov-08 resin4pt resin4p 17-Nov-08 recos4pt recos4p 17-Nov-08 ef4pt ef4p 17-Nov-08 addclt addcl 17-Nov-08 readdclt readdcl 17-Nov-08 mulclt mulcl 17-Nov-08 remulclt remulcl 17-Nov-08 addcomt addcom 17-Nov-08 mulcomt mulcom 17-Nov-08 addasst addass 17-Nov-08 mulasst mulass 17-Nov-08 adddit adddi 17-Nov-08 addid1t addid1 17-Nov-08 mulid1t mulid1 17-Nov-08 recnt recn 17-Nov-08 adddirt adddir 17-Nov-08 addid2t addid2 17-Nov-08 add12t add12 17-Nov-08 add23t add23 17-Nov-08 add4t add4 17-Nov-08 add42t add42 17-Nov-08 cnegext cnegex 17-Nov-08 cnegextlem1 cnegexlem1 17-Nov-08 cnegextlem2 cnegexlem2 17-Nov-08 cnegextlem3 cnegexlem3 17-Nov-08 addcant addcan 17-Nov-08 addcan2t addcan2 17-Nov-08 subvalt subval 17-Nov-08 subclt subcl 17-Nov-08 negclt negcl 17-Nov-08 subaddt subadd 17-Nov-08 subsub23t subsub23 17-Nov-08 pncan3t pncan3 17-Nov-08 negidt negid 17-Nov-08 negsubt negsub 17-Nov-08 addsubasst addsubass 17-Nov-08 addsubt addsub 17-Nov-08 subadd23t subadd23 17-Nov-08 addsub12t addsub12 17-Nov-08 2addsubt 2addsub 17-Nov-08 negnegt negneg 17-Nov-08 subnegt subneg 17-Nov-08 subidt subid 17-Nov-08 subid1t subid1 17-Nov-08 pncant pncan 17-Nov-08 pncan2t pncan2 17-Nov-08 npcant npcan 17-Nov-08 npncant npncan 17-Nov-08 nppcant nppcan 17-Nov-08 subcan2t subcan2 17-Nov-08 subeq0t subeq0 17-Nov-08 neg11t neg11 17-Nov-08 negcon1t negcon1 17-Nov-08 negcon2t negcon2 17-Nov-08 subcant subcan 17-Nov-08 mulid2t mulid2 17-Nov-08 mul12t mul12 17-Nov-08 mul23t mul23 17-Nov-08 mul4t mul4 17-Nov-08 muladdt muladd 17-Nov-08 muladd11t muladd11 17-Nov-08 subdit subdi 17-Nov-08 subdirt subdir 17-Nov-08 renegclt renegcl 17-Nov-08 resubclt resubcl 17-Nov-08 mul01t mul01 17-Nov-08 mul02t mul02 17-Nov-08 mulneg1t mulneg1 17-Nov-08 mulneg2t mulneg2 17-Nov-08 mulneg12t mulneg12 17-Nov-08 mul2negt mul2neg 17-Nov-08 negdit negdi 17-Nov-08 negdi2t negdi2 17-Nov-08 negsubdit negsubdi 17-Nov-08 negsubdi2t negsubdi2 17-Nov-08 neg2subt neg2sub 17-Nov-08 submul2t submul2 17-Nov-08 subsub2t subsub2 17-Nov-08 subsubt subsub 17-Nov-08 subsub3t subsub3 17-Nov-08 subsub4t subsub4 17-Nov-08 sub23t sub23 17-Nov-08 nnncant nnncan 17-Nov-08 nnncan1t nnncan1 17-Nov-08 nnncan2t nnncan2 17-Nov-08 nncant nncan 17-Nov-08 nppcan2t nppcan2 17-Nov-08 mulm1t mulm1 17-Nov-08 addsub4t addsub4 17-Nov-08 subadd4t subadd4 17-Nov-08 sub4t sub4 17-Nov-08 mulsubt mulsub 17-Nov-08 pnpcant pnpcan 17-Nov-08 pnpcan2t pnpcan2 17-Nov-08 pnncant pnncan 17-Nov-08 ppncant ppncan 17-Nov-08 ltxrt ltxr 17-Nov-08 rexrt rexr 17-Nov-08 ltxrltt ltxrlt 17-Nov-08 xrlenltt xrlenlt 17-Nov-08 xrltnlet xrltnle 17-Nov-08 lttrt lttr 17-Nov-08 mulgt0t mulgt0 17-Nov-08 lenltt lenlt 17-Nov-08 ltnlet ltnle 17-Nov-08 lttri2t lttri2 17-Nov-08 lttri3t lttri3 17-Nov-08 lttri4t lttri4 17-Nov-08 ltnet ltne 17-Nov-08 letri3t letri3 17-Nov-08 leloet leloe 17-Nov-08 eqleltt eqlelt 17-Nov-08 ltlet ltle 17-Nov-08 leltnet leltne 17-Nov-08 ltlent ltlen 17-Nov-08 lelttrt lelttr 17-Nov-08 ltletrt ltletr 17-Nov-08 letrt letr 17-Nov-08 ltnrt ltnr 17-Nov-08 leidt leid 17-Nov-08 ltnsymt ltnsym 17-Nov-08 ltnsym2t ltnsym2 17-Nov-08 renepnft renepnf 17-Nov-08 renemnft renemnf 17-Nov-08 xrltnrt xrltnr 17-Nov-08 ltpnft ltpnf 17-Nov-08 mnfltt mnflt 17-Nov-08 mnfltxrt mnfltxr 17-Nov-08 pnfnltt pnfnlt 17-Nov-08 nltmnft nltmnf 17-Nov-08 pnfget pnfge 17-Nov-08 mnflet mnfle 17-Nov-08 xrltnsymt xrltnsym 17-Nov-08 xrltnsym2t xrltnsym2 17-Nov-08 xrlttrit xrlttri 17-Nov-08 xrlttrt xrlttr 17-Nov-08 xrlttri2t xrlttri2 17-Nov-08 xrlttri3t xrlttri3 17-Nov-08 xrleloet xrleloe 17-Nov-08 xrleltnet xrleltne 17-Nov-08 xrltlet xrltle 17-Nov-08 xrleidt xrleid 17-Nov-08 xrletrit xrletri 17-Nov-08 xrlelttrt xrlelttr 17-Nov-08 xrltletrt xrltletr 17-Nov-08 xrletrt xrletr 17-Nov-08 xrltnet xrltne 17-Nov-08 nltpnftt nltpnft 17-Nov-08 ngtmnftt ngtmnft 17-Nov-08 xrrebndt xrrebnd 17-Nov-08 xrret xrre 17-Nov-08 xrre2t xrre2 17-Nov-08 eqlet eqle 17-Nov-08 msqgt0t msqgt0 17-Nov-08 msqge0t msqge0 17-Nov-08 gt0ne0t gt0ne0 17-Nov-08 ne0gt0t ne0gt0 17-Nov-08 letrit letric 17-Nov-08 lelttrit lelttric 17-Nov-08 ltadd1t ltadd1 17-Nov-08 ltadd2t ltadd2 17-Nov-08 leadd1t leadd1 17-Nov-08 leadd2t leadd2 17-Nov-08 ltsubaddt ltsubadd 17-Nov-08 ltsubadd2t ltsubadd2 17-Nov-08 lesubaddt lesubadd 17-Nov-08 lesubadd2t lesubadd2 17-Nov-08 ltaddsubt ltaddsub 17-Nov-08 ltaddsub2t ltaddsub2 17-Nov-08 leaddsubt leaddsub 17-Nov-08 leaddsub2t leaddsub2 17-Nov-08 sublet suble 17-Nov-08 lesubt lesub 17-Nov-08 ltsub23t ltsub23 17-Nov-08 ltsub13t ltsub13 17-Nov-08 lt2addt lt2add 17-Nov-08 le2addt le2add 17-Nov-08 ltleaddt ltleadd 17-Nov-08 leltaddt leltadd 17-Nov-08 addgt0t addgt0 17-Nov-08 addgegt0t addgegt0 17-Nov-08 addgtge0t addgtge0 17-Nov-08 addge0t addge0 17-Nov-08 ltaddpost ltaddpos 17-Nov-08 ltaddpos2t ltaddpos2 17-Nov-08 ltsubpost ltsubpos 17-Nov-08 posdift posdif 17-Nov-08 ltnegt ltneg 17-Nov-08 ltnegcon1t ltnegcon1 17-Nov-08 lenegt leneg 17-Nov-08 lenegcon1t lenegcon1 17-Nov-08 lenegcon2t lenegcon2 17-Nov-08 lesub1t lesub1 17-Nov-08 lesub2t lesub2 17-Nov-08 ltsub1t ltsub1 17-Nov-08 ltsub2t ltsub2 17-Nov-08 lt0neg1t lt0neg1 17-Nov-08 lt0neg2t lt0neg2 17-Nov-08 le0neg1t le0neg1 17-Nov-08 le0neg2t le0neg2 17-Nov-08 addge01t addge01 17-Nov-08 addge02t addge02 17-Nov-08 subge0t subge0 17-Nov-08 suble0t suble0 17-Nov-08 subge02t subge02 17-Nov-08 lesub0t lesub0 17-Nov-08 mulge0t mulge0 17-Nov-08 recext recex 17-Nov-08 mulcant mulcan 17-Nov-08 mulcan2t mulcan2 17-Nov-08 mul0ort mul0or 17-Nov-08 muln0bt muln0b 17-Nov-08 muln0t muln0 17-Nov-08 muleqaddt muleqadd 17-Nov-08 divmult divmul 17-Nov-08 divmul2t divmul2 17-Nov-08 divmul3t divmul3 17-Nov-08 divclt divcl 17-Nov-08 recclt reccl 17-Nov-08 divcan1t divcan1 17-Nov-08 divcan2t divcan2 17-Nov-08 divne0bt divne0b 17-Nov-08 divne0t divne0 17-Nov-08 recne0t recne0 17-Nov-08 recidt recid 17-Nov-08 recid2t recid2 17-Nov-08 divrect divrec 17-Nov-08 divrec2t divrec2 17-Nov-08 divasst divass 17-Nov-08 div23t div23 17-Nov-08 div13t div13 17-Nov-08 div12t div12 17-Nov-08 divdirt divdir 17-Nov-08 divcan3t divcan3 17-Nov-08 divcan4t divcan4 17-Nov-08 div11t div11 17-Nov-08 dividt divid 17-Nov-08 div0t div0 17-Nov-08 diveq0t diveq0 17-Nov-08 div1t div1 17-Nov-08 divnegt divneg 17-Nov-08 divsubdirt divsubdir 17-Nov-08 recrect recrec 17-Nov-08 rec11rt rec11r 17-Nov-08 divmuldivt divmuldiv 17-Nov-08 divcan5t divcan5 17-Nov-08 divmul13t divmul13 17-Nov-08 divmul24t divmul24 17-Nov-08 divadddivt divadddiv 17-Nov-08 divdivdivt divdivdiv 17-Nov-08 recdivt recdiv 17-Nov-08 divcan6t divcan6 17-Nov-08 divdiv23t divdiv23 17-Nov-08 divdivmult divdivmul 17-Nov-08 recdiv2t recdiv2 17-Nov-08 conjmult conjmul 17-Nov-08 redivclt redivcl 17-Nov-08 rerecclt rereccl 17-Nov-08 eqnegt eqneg 17-Nov-08 negeq0t negeq0 17-Nov-08 ltp1t ltp1 17-Nov-08 lep1t lep1 17-Nov-08 ltm1t ltm1 17-Nov-08 letrp1t letrp1 17-Nov-08 p1let p1le 17-Nov-08 prodgt0t prodgt0 17-Nov-08 prodgt02t prodgt02 17-Nov-08 prodge0t prodge0 17-Nov-08 prodge02t prodge02 17-Nov-08 ltmul1t ltmul1 17-Nov-08 ltmul2t ltmul2 17-Nov-08 lemul1t lemul1 17-Nov-08 lemul2t lemul2 17-Nov-08 lemul1it lemul1a 17-Nov-08 lemul2it lemul2a 17-Nov-08 ltmul12it ltmul12a 17-Nov-08 lemul12ait lemul12b 17-Nov-08 lemul12it lemul12a 17-Nov-08 mulgt1t mulgt1 17-Nov-08 ltmulgt11t ltmulgt11 17-Nov-08 ltmulgt12t ltmulgt12 17-Nov-08 lemulge11t lemulge11 17-Nov-08 ltdiv1t ltdiv1 17-Nov-08 lediv1t lediv1 17-Nov-08 gt0divt gt0div 17-Nov-08 ge0divt ge0div 17-Nov-08 divgt0t divgt0 17-Nov-08 divge0t divge0 17-Nov-08 recgt0t recgt0 17-Nov-08 ltmuldivt ltmuldiv 17-Nov-08 ltmuldiv2t ltmuldiv2 17-Nov-08 ltdivmult ltdivmul 17-Nov-08 ledivmult ledivmul 17-Nov-08 ltdivmul2t ltdivmul2 17-Nov-08 lt2mul2divt lt2mul2div 17-Nov-08 ledivmul2t ledivmul2 17-Nov-08 lemuldivt lemuldiv 17-Nov-08 lemuldiv2t lemuldiv2 17-Nov-08 ltrect ltrec 17-Nov-08 lerect lerec 17-Nov-08 lt2msqt lt2msq 17-Nov-08 ltdiv2t ltdiv2 17-Nov-08 ltrec1t ltrec1 17-Nov-08 lerec2t lerec2 17-Nov-08 ledivdivt ledivdiv 17-Nov-08 lediv2t lediv2 17-Nov-08 ltdiv23t ltdiv23 17-Nov-08 lediv23t lediv23 17-Nov-08 lediv12it lediv12a 17-Nov-08 lediv2it lediv2a 17-Nov-08 reclt1t reclt1 17-Nov-08 recgt1t recgt1 17-Nov-08 recgt1it recgt1i 17-Nov-08 recrecltt recreclt 17-Nov-08 le2msqt le2msq 17-Nov-08 ledivp1t ledivp1 17-Nov-08 xrmaxltt xrmaxlt 17-Nov-08 xrltmint xrltmin 17-Nov-08 maxlet maxle 17-Nov-08 lemint lemin 17-Nov-08 maxltt maxlt 17-Nov-08 ltmint ltmin 17-Nov-08 nnret nnre 17-Nov-08 nncnt nncn 17-Nov-08 nnaddclt nnaddcl 17-Nov-08 nnmulclt nnmulcl 17-Nov-08 nn2get nn2ge 17-Nov-08 nnge1t nnge1 17-Nov-08 nngt1ne1t nngt1ne1 17-Nov-08 nnle1eq1t nnle1eq1 17-Nov-08 nngt0t nngt0 17-Nov-08 nnne0t nnne0 17-Nov-08 nnrecret nnrecre 17-Nov-08 nnrecgt0t nnrecgt0 17-Nov-08 nnleltp1t nnleltp1 17-Nov-08 nnltp1let nnltp1le 17-Nov-08 nnsubt nnsub 17-Nov-08 nnaddm1clt nnaddm1cl 17-Nov-08 nndivt nndiv 17-Nov-08 nndivtrt nndivtr 17-Nov-08 2timest 2times 17-Nov-08 times2t times2 17-Nov-08 halfclt halfcl 17-Nov-08 rehalfclt rehalfcl 17-Nov-08 half0t half0 17-Nov-08 halfpost halfpos 17-Nov-08 halfpos2t halfpos2 17-Nov-08 halfnneg2t halfnneg2 17-Nov-08 2halvest 2halves 17-Nov-08 halfaddsubt halfaddsub 17-Nov-08 lt2halvest lt2halves 17-Nov-08 avglet avgle 17-Nov-08 rpret rpre 17-Nov-08 rpcnt rpcn 17-Nov-08 rpgt0t rpgt0 17-Nov-08 rpge0t rpge0 17-Nov-08 rpregt0t rpregt0 17-Nov-08 rpne0t rpne0 17-Nov-08 rprene0t rprene0 17-Nov-08 rpcnne0t rpcnne0 17-Nov-08 rpaddclt rpaddcl 17-Nov-08 rpmulclt rpmulcl 17-Nov-08 rpdivclt rpdivcl 17-Nov-08 rerpdivclt rerpdivcl 17-Nov-08 rpnegt rpneg 17-Nov-08 nnreclt nnrecl 17-Nov-08 nnnn0t nnnn0 17-Nov-08 nn0ret nn0re 17-Nov-08 nn0cnt nn0cn 17-Nov-08 nn0ge0t nn0ge0 17-Nov-08 nn0le0eq0t nn0le0eq0 17-Nov-08 nn0addclt nn0addcl 17-Nov-08 nn0mulclt nn0mulcl 17-Nov-08 nnnn0addclt nnnn0addcl 17-Nov-08 nn0nnaddclt nn0nnaddcl 17-Nov-08 nn0ltp1let nn0ltp1le 17-Nov-08 nn0leltp1t nn0leltp1 17-Nov-08 nn0ltlem1t nn0ltlem1 17-Nov-08 nn0addge1t nn0addge1 17-Nov-08 nn0addge2t nn0addge2 17-Nov-08 zret zre 17-Nov-08 zcnt zcn 17-Nov-08 nnzt nnz 17-Nov-08 nn0zt nn0z 17-Nov-08 znnnlt1t znnnlt1 17-Nov-08 nn0subt nn0sub 17-Nov-08 nn0sub2t nn0sub2 17-Nov-08 znegclt znegcl 17-Nov-08 zaddclt zaddcl 17-Nov-08 zsubclt zsubcl 17-Nov-08 zrevaddclt zrevaddcl 17-Nov-08 nn0p1nnt nn0p1nn 17-Nov-08 nnm1nn0t nnm1nn0 17-Nov-08 znnsubt znnsub 17-Nov-08 znn0subt znn0sub 17-Nov-08 znn0sub2t znn0sub2 17-Nov-08 zmulclt zmulcl 17-Nov-08 zltp1let zltp1le 17-Nov-08 zleltp1t zleltp1 17-Nov-08 zlem1ltt zlem1lt 17-Nov-08 zltlem1t zltlem1 17-Nov-08 nn0lem1ltt nn0lem1lt 17-Nov-08 nnlem1ltt nnlem1lt 17-Nov-08 nnltlem1t nnltlem1 17-Nov-08 zdivt zdiv 17-Nov-08 zdivaddt zdivadd 17-Nov-08 zdivmult zdivmul 17-Nov-08 z2get z2ge 17-Nov-08 zextlet zextle 17-Nov-08 zextltt zextlt 17-Nov-08 recnzt recnz 17-Nov-08 btwnnzt btwnnz 17-Nov-08 gtndivt gtndiv 17-Nov-08 primet prime 17-Nov-08 nneot nneo 17-Nov-08 zeot zeo 17-Nov-08 qret qre 17-Nov-08 zqt zq 17-Nov-08 nnqt nnq 17-Nov-08 qcnt qcn 17-Nov-08 qaddclt qaddcl 17-Nov-08 qnegclt qnegcl 17-Nov-08 qmulclt qmulcl 17-Nov-08 qsubclt qsubcl 17-Nov-08 qrecclt qreccl 17-Nov-08 qdivclt qdivcl 17-Nov-08 qrevaddclt qrevaddcl 17-Nov-08 nnrecqt nnrecq 17-Nov-08 irraddt irradd 17-Nov-08 irrmult irrmul 17-Nov-08 flvalt flval 17-Nov-08 flclt flcl 17-Nov-08 flreclt flrecl 17-Nov-08 flleltt fllelt 17-Nov-08 fllet flle 17-Nov-08 flltp1t flltp1 17-Nov-08 fraclt1t fraclt1 17-Nov-08 fracge0t fracge0 17-Nov-08 flget flge 17-Nov-08 flltt fllt 17-Nov-08 flidt flid 17-Nov-08 flidmt flidm 17-Nov-08 flidzt flidz 17-Nov-08 flwordit flwordi 17-Nov-08 flval2t flval2 17-Nov-08 flval3t flval3 17-Nov-08 flbit flbi 17-Nov-08 flbi2t flbi2 17-Nov-08 flge0nn0t flge0nn0 17-Nov-08 flge1nnt flge1nn 17-Nov-08 fladdzt fladdz 17-Nov-08 btwnzge0t btwnzge0 17-Nov-08 flhalft flhalf 17-Nov-08 ceiclt ceicl 17-Nov-08 ceiget ceige 17-Nov-08 ceim1lt ceim1l 17-Nov-08 ceilet ceile 17-Nov-08 fldivt fldiv 17-Nov-08 fldiv2t fldiv2 17-Nov-08 modvalt modval 17-Nov-08 modclt modcl 17-Nov-08 modge0t modge0 17-Nov-08 modltt modlt 17-Nov-08 modfract modfrac 17-Nov-08 flmodt flmod 17-Nov-08 modcyct modcyc 17-Nov-08 modcyc2t modcyc2 17-Nov-08 modadd1t modadd1 17-Nov-08 modmul1t modmul1 17-Nov-08 moddit moddi 17-Nov-08 modirrt modirr 17-Nov-08 ioovalt iooval 17-Nov-08 iooval2t iooval2 17-Nov-08 ioo0t ioo0 17-Nov-08 ioon0t ioon0 17-Nov-08 iooint iooin 17-Nov-08 iocvalt iocval 17-Nov-08 icovalt icoval 17-Nov-08 iccvalt iccval 17-Nov-08 elioo1t elioo1 17-Nov-08 elioo2t elioo2 17-Nov-08 elioc1t elioc1 17-Nov-08 elico1t elico1 17-Nov-08 elicc1t elicc1 17-Nov-08 elioo5t elioo5 17-Nov-08 eliooret elioore 17-Nov-08 eliooxrt eliooxr 17-Nov-08 eliooordt eliooord 17-Nov-08 elioc2t elioc2 17-Nov-08 elico2t elico2 17-Nov-08 elicc2t elicc2 17-Nov-08 iooshft iooshf 17-Nov-08 iccssret iccssre 17-Nov-08 lbicc2t lbicc2 17-Nov-08 ubicc2t ubicc2 17-Nov-08 ioonegt iooneg 17-Nov-08 iccnegt iccneg 17-Nov-08 icoshft icoshf 17-Nov-08 ioojoint ioojoin 17-Nov-08 uzvalt uzval 17-Nov-08 eluz1t eluz1 17-Nov-08 eluz2t eluz2 17-Nov-08 eluzt eluz 17-Nov-08 uzidt uzid 17-Nov-08 uznegit uznegi 17-Nov-08 uz11t uz11 17-Nov-08 eluzp1m1t eluzp1m1 17-Nov-08 eluzp1lt eluzp1l 17-Nov-08 eluzp1p1t eluzp1p1 17-Nov-08 uzaddclt uzaddcl 17-Nov-08 fzvalt fzval 17-Nov-08 elfz1t elfz1 17-Nov-08 elfzt elfz 17-Nov-08 elfz2t elfz2 17-Nov-08 elfz5t elfz5 17-Nov-08 elfz4t elfz4 17-Nov-08 eluzfzt eluzfz 17-Nov-08 elfzuz3t elfzuz3 17-Nov-08 elfzuz2t elfzuz2 17-Nov-08 eluzfz1t eluzfz1 17-Nov-08 elfzuzt elfzuz 17-Nov-08 eluzfz2t eluzfz2 17-Nov-08 elfz3t elfz3 17-Nov-08 elfz1eqt elfz1eq 17-Nov-08 fznt fzn 17-Nov-08 elfznnt elfznn 17-Nov-08 elfz2nn0t elfz2nn0 17-Nov-08 elfznn0t elfznn0 17-Nov-08 elfz3nn0t elfz3nn0 17-Nov-08 fznn0subt fznn0sub 17-Nov-08 fznn0sub2t fznn0sub2 17-Nov-08 fzaddelt fzaddel 17-Nov-08 fzsubelt fzsubel 17-Nov-08 fzoptht fzopth 17-Nov-08 fzss1t fzss1 17-Nov-08 fzss2t fzss2 17-Nov-08 fzssuzt fzssuz 17-Nov-08 fzssp1t fzssp1 17-Nov-08 fzp1sst fzp1ss 17-Nov-08 fzelp1t fzelp1 17-Nov-08 fzrevt fzrev 17-Nov-08 fzrev2t fzrev2 17-Nov-08 fzrev2it fzrev2i 17-Nov-08 fzrev3t fzrev3 17-Nov-08 fzrev3it fzrev3i 17-Nov-08 fznn0t fznn0 17-Nov-08 fz1sbct fz1sbc 17-Nov-08 fzneuzt fzneuz 17-Nov-08 fzrevralt fzrevral 17-Nov-08 fzrevral2t fzrevral2 17-Nov-08 fzrevral3t fzrevral3 17-Nov-08 fzshftralt fzshftral 17-Nov-08 ser1ft ser1f 17-Nov-08 limsupvalt limsupval 17-Nov-08 limsupclt limsupcl 17-Nov-08 expvalt expval 17-Nov-08 exp0t exp0 17-Nov-08 expnnvalt expnnval 17-Nov-08 exp1t exp1 17-Nov-08 expp1t expp1 17-Nov-08 nnexpclt nnexpcl 17-Nov-08 nn0expclt nn0expcl 17-Nov-08 zexpclt zexpcl 17-Nov-08 qexpclt qexpcl 17-Nov-08 reexpclt reexpcl 17-Nov-08 expclt expcl 17-Nov-08 rpexpclt rpexpcl 17-Nov-08 expm1t expm1 17-Nov-08 1expt 1exp 17-Nov-08 expeq0t expeq0 17-Nov-08 expne0t expne0 17-Nov-08 expne0it expne0i 17-Nov-08 expgt0t expgt0 17-Nov-08 0expt 0exp 17-Nov-08 expge0t expge0 17-Nov-08 expgt1t expgt1 17-Nov-08 expge1t expge1 17-Nov-08 mulexpt mulexp 17-Nov-08 recexpt recexp 17-Nov-08 expaddt expadd 17-Nov-08 expmult expmul 17-Nov-08 expsubt expsub 17-Nov-08 divexpt divexp 17-Nov-08 expordit expordi 17-Nov-08 expcant expcan 17-Nov-08 expordt expord 17-Nov-08 expwordit expwordi 17-Nov-08 expord2t expord2 17-Nov-08 expword2it expword2i 17-Nov-08 expmwordit expmwordi 17-Nov-08 exple1t exple1 17-Nov-08 expubndt expubnd 17-Nov-08 sqvalt sqval 17-Nov-08 sqnegt sqneg 17-Nov-08 sqclt sqcl 17-Nov-08 sqmult sqmul 17-Nov-08 sqeq0t sqeq0 17-Nov-08 sqne0t sqne0 17-Nov-08 resqclt resqcl 17-Nov-08 sqgt0t sqgt0 17-Nov-08 sq11t sq11 17-Nov-08 lt2sqt lt2sq 17-Nov-08 le2sqt le2sq 17-Nov-08 le2sqit le2sq2 17-Nov-08 sqge0t sqge0 17-Nov-08 sqlecant sqlecan 17-Nov-08 subsqt subsq 17-Nov-08 subsq2t subsq2 17-Nov-08 sqeqort sqeqor 17-Nov-08 binom2t binom2 17-Nov-08 sq01t sq01 17-Nov-08 expnbndt expnbnd 17-Nov-08 expnlbndt expnlbnd 17-Nov-08 expnlbnd2t expnlbnd2 17-Nov-08 nn0opth2t nn0opth2 17-Nov-08 sqrclt sqrcl 17-Nov-08 sqrgt0t sqrgt0 17-Nov-08 sqrge0t sqrge0 17-Nov-08 sqrlet sqrle 17-Nov-08 sqr00t sqr00 17-Nov-08 rpsqrclt rpsqrcl 17-Nov-08 sqrsqt sqrsq 17-Nov-08 sqsqrt sqsqr 17-Nov-08 crut cru 17-Nov-08 revalt reval 17-Nov-08 imvalt imval 17-Nov-08 reclt recl 17-Nov-08 imclt imcl 17-Nov-08 replimt replim 17-Nov-08 absvalt absval 17-Nov-08 cjvalt cjval 17-Nov-08 cjclt cjcl 17-Nov-08 crret crre 17-Nov-08 crimt crim 17-Nov-08 imret imre 17-Nov-08 reim0t reim0 17-Nov-08 reim0bt reim0b 17-Nov-08 rerebt rereb 17-Nov-08 mulret mulre 17-Nov-08 reret rere 17-Nov-08 cjrebt cjreb 17-Nov-08 cjmulrclt cjmulrcl 17-Nov-08 cjmulvalt cjmulval 17-Nov-08 cjmulge0t cjmulge0 17-Nov-08 renegt reneg 17-Nov-08 readdt readd 17-Nov-08 resubt resub 17-Nov-08 imnegt imneg 17-Nov-08 imaddt imadd 17-Nov-08 imsubt imsub 17-Nov-08 cjret cjre 17-Nov-08 cjcjt cjcj 17-Nov-08 cjaddt cjadd 17-Nov-08 cjmult cjmul 17-Nov-08 cjnegt cjneg 17-Nov-08 addcjt addcj 17-Nov-08 cjsubt cjsub 17-Nov-08 cjexpt cjexp 17-Nov-08 recjt recj 17-Nov-08 imcjt imcj 17-Nov-08 cjreimt cjreim 17-Nov-08 cjreim2t cjreim2 17-Nov-08 cj11t cj11 17-Nov-08 cjne0t cjne0 17-Nov-08 absnegt absneg 17-Nov-08 absclt abscl 17-Nov-08 abscjt abscj 17-Nov-08 absvalsqt absvalsq 17-Nov-08 absvalsq2t absvalsq2 17-Nov-08 sqabsaddt sqabsadd 17-Nov-08 sqabssubt sqabssub 17-Nov-08 absval2t absval2 17-Nov-08 abs00t abs00 17-Nov-08 absge0t absge0 17-Nov-08 absrpclt absrpcl 17-Nov-08 absreimsqt absreimsq 17-Nov-08 absreimt absreim 17-Nov-08 absmult absmul 17-Nov-08 absdivt absdiv 17-Nov-08 absidt absid 17-Nov-08 absnidt absnid 17-Nov-08 leabst leabs 17-Nov-08 absort absor 17-Nov-08 absret absre 17-Nov-08 absresqt absresq 17-Nov-08 absexpt absexp 17-Nov-08 absrelet absrele 17-Nov-08 absimlet absimle 17-Nov-08 nn0absclt nn0abscl 17-Nov-08 absltt abslt 17-Nov-08 abslet absle 17-Nov-08 abssubne0t abssubne0 17-Nov-08 absdifltt absdiflt 17-Nov-08 absdiflet absdifle 17-Nov-08 lenegsqt lenegsq 17-Nov-08 releabst releabs 17-Nov-08 cjdivt cjdiv 17-Nov-08 absidmt absidm 17-Nov-08 absgt0t absgt0 17-Nov-08 abssubt abssub 17-Nov-08 abssubge0t abssubge0 17-Nov-08 abssuble0t abssuble0 17-Nov-08 absmaxt absmax 17-Nov-08 abstrit abstri 17-Nov-08 abs3dift abs3dif 17-Nov-08 abs2dift abs2dif 17-Nov-08 abs2difabst abs2difabs 17-Nov-08 recant recan 17-Nov-08 abs3lemt abs3lem 17-Nov-08 facnnt facnn 17-Nov-08 facp1t facp1 17-Nov-08 facnn2t facnn2 17-Nov-08 facclt faccl 17-Nov-08 facne0t facne0 17-Nov-08 facdivt facdiv 17-Nov-08 facndivt facndiv 17-Nov-08 facwordit facwordi 17-Nov-08 facavgt facavg 17-Nov-08 bcvalt bcval 17-Nov-08 bcval2t bcval2 17-Nov-08 bcval3t bcval3 17-Nov-08 bcval4t bcval4 17-Nov-08 bccmplt bccmpl 17-Nov-08 bcn0t bcn0 17-Nov-08 bcnnt bcnn 17-Nov-08 bcnp11t bcnp11 17-Nov-08 bcnp1nt bcnp1n 17-Nov-08 bcpasc2t bcpasc2 17-Nov-08 bcpasct bcpasc 17-Nov-08 bccl2t bccl2 17-Nov-08 bcclt bccl 17-Nov-08 permnnt permnn 17-Nov-08 fsumclt fsumcl 17-Nov-08 fsum0clt fsum0cl 17-Nov-08 fsumreclt fsumrecl 17-Nov-08 fsumsplit fsumspli 17-Nov-08 fsum0split fsum0spli 17-Nov-08 fsumshft fsumshf 17-Nov-08 fsumconst fsumcons 17-Nov-08 clmi2at clmi2a 17-Nov-08 caucvg3t caucvg3 17-Nov-08 eftclt eftcl 17-Nov-08 efvalt efval 17-Nov-08 efclt efcl 17-Nov-08 reefclt reefcl 17-Nov-08 efcjt efcj 17-Nov-08 efaddt efadd 17-Nov-08 efcant efcan 17-Nov-08 efne0t efne0 17-Nov-08 efsubt efsub 17-Nov-08 efexpt efexp 17-Nov-08 efnn0valt efnn0val 17-Nov-08 reeftclt reeftcl 17-Nov-08 eftlubclt eftlubcl 17-Nov-08 efgt0t efgt0 17-Nov-08 reef11t reef11 17-Nov-08 eflegeot eflegeo 17-Nov-08 efm1legeot efm1legeo 17-Nov-08 sinvalt sinval 17-Nov-08 cosvalt cosval 17-Nov-08 sinclt sincl 17-Nov-08 cosclt coscl 17-Nov-08 resinvalt resinval 17-Nov-08 recosvalt recosval 17-Nov-08 resinclt resincl 17-Nov-08 recosclt recoscl 17-Nov-08 sinnegt sinneg 17-Nov-08 cosnegt cosneg 17-Nov-08 efivalt efival 17-Nov-08 efmivalt efmival 17-Nov-08 efeult efeul 17-Nov-08 sinaddt sinadd 17-Nov-08 cosaddt cosadd 17-Nov-08 sinsubt sinsub 17-Nov-08 cossubt cossub 17-Nov-08 addsint addsin 17-Nov-08 subsint subsin 17-Nov-08 addcost addcos 17-Nov-08 subcost subcos 17-Nov-08 sincossqt sincossq 17-Nov-08 sin2tt sin2t 17-Nov-08 cos2tt cos2t 17-Nov-08 cos2tsint cos2tsin 17-Nov-08 sinbndt sinbnd 17-Nov-08 cosbndt cosbnd 17-Nov-08 absefit absefi 17-Nov-08 abseft absef 17-Nov-08 absefibt absefib 17-Nov-08 cosh111t cosh111 17-Nov-08 logclt logcl 17-Nov-08 relogclt relogcl 17-Nov-08 eflogt eflog 17-Nov-08 reeflogt reeflog 17-Nov-08 logeft logef 17-Nov-08 relogeft relogef 17-Nov-08 relogmult relogmul 17-Nov-08 relogdivt relogdiv 17-Nov-08 explogt explog 17-Nov-08 reexplogt reexplog 17-Nov-08 relogexpt relogexp 17-Nov-08 logltbt logltb 17-Nov-08 1p1times 1p1timesi 17-Nov-08 2climnn 2climnni 17-Nov-08 2climnn0 2climnn0i 17-Nov-08 2shft 2shfti 17-Nov-08 2times 2timesi 17-Nov-08 abs00 abs00i 17-Nov-08 abs1m abs1mi 17-Nov-08 abs3dif abs3difi 17-Nov-08 abscj abscji 17-Nov-08 abscl abscli 17-Nov-08 absdivz absdivzi 17-Nov-08 absef01tlub absef01tlubi 17-Nov-08 absefm1le absefm1lei 17-Nov-08 absge0 absge0i 17-Nov-08 absgt0 absgt0i 17-Nov-08 absid absidi 17-Nov-08 absle abslei 17-Nov-08 abslt abslti 17-Nov-08 absmul absmuli 17-Nov-08 absneg absnegi 17-Nov-08 absnid absnidi 17-Nov-08 absor absori 17-Nov-08 abspef01tlub abspef01tlubi 17-Nov-08 absre absrei 17-Nov-08 abssub abssubi 17-Nov-08 abstri abstrii 17-Nov-08 absval2 absval2i 17-Nov-08 absvalsq absvalsqi 17-Nov-08 absvalsq2 absvalsq2i 17-Nov-08 add12 add12i 17-Nov-08 add20 add20i 17-Nov-08 add23 add23i 17-Nov-08 add4 add4i 17-Nov-08 add42 add42i 17-Nov-08 addass addassi 17-Nov-08 addcan addcani 17-Nov-08 addcan2 addcan2i 17-Nov-08 addcj addcji 17-Nov-08 addcl addcli 17-Nov-08 addcom addcomi 17-Nov-08 adddi adddii 17-Nov-08 adddir adddiri 17-Nov-08 addge0 addge0i 17-Nov-08 addgegt0 addgegt0i 17-Nov-08 addgt0 addgt0i 17-Nov-08 addgt0i addgt0ii 17-Nov-08 addid1 addid1i 17-Nov-08 addid2 addid2i 17-Nov-08 addsub addsubi 17-Nov-08 addsub4 addsub4i 17-Nov-08 addsubass addsubassi 17-Nov-08 bcpasc bcpasci 17-Nov-08 bcpasc2 bcpasc2i 17-Nov-08 binom binomi 17-Nov-08 binom1p binom1pi 17-Nov-08 binom2 binom2i 17-Nov-08 binom2a binom2ai 17-Nov-08 cau2 cau2i 17-Nov-08 cau3 cau3i 17-Nov-08 cau3i cau3ii 17-Nov-08 cau3ir cau3iri 17-Nov-08 cau4i cau4ii 17-Nov-08 cau5 cau5i 17-Nov-08 cau5i cau5ii 17-Nov-08 caubnd caubndi 17-Nov-08 caucvg caucvgi 17-Nov-08 caucvg2 caucvg2i 17-Nov-08 caucvg3 caucvg3i 17-Nov-08 caucvg3a caucvg3ai 17-Nov-08 cauim cauimi 17-Nov-08 caure caurei 17-Nov-08 cbvsum cbvsumi 17-Nov-08 cjadd cjaddi 17-Nov-08 cjcj cjcji 17-Nov-08 cjcl cjcli 17-Nov-08 cjdiv cjdivi 17-Nov-08 cjmul cjmuli 17-Nov-08 cjmulge0 cjmulge0i 17-Nov-08 cjmulrcl cjmulrcli 17-Nov-08 cjmulval cjmulvali 17-Nov-08 cjneg cjnegi 17-Nov-08 cjreb cjrebi 17-Nov-08 clim2serz clim2serzi 17-Nov-08 clim2serzt clim2serzti 17-Nov-08 climabs climabsi 17-Nov-08 climabs0 climabs0i 17-Nov-08 climadd climaddi 17-Nov-08 climaddc climaddci 17-Nov-08 climaddc1 climaddc1i 17-Nov-08 climaddc2 climaddc2i 17-Nov-08 climcau climcaui 17-Nov-08 climcj climcji 17-Nov-08 climcmp climcmpi 17-Nov-08 climcmpc1 climcmpc1i 17-Nov-08 climconst climconsti 17-Nov-08 climeu climeui 17-Nov-08 climfnrcl climfnrcli 17-Nov-08 climge0 climge0i 17-Nov-08 climim climimi 17-Nov-08 climmul climmuli 17-Nov-08 climmulc climmulci 17-Nov-08 climmulc2 climmulc2i 17-Nov-08 climre climrei 17-Nov-08 climrecl climrecli 17-Nov-08 climres climresi 17-Nov-08 climreu climreui 17-Nov-08 climserzle climserzlei 17-Nov-08 climshft climshfti 17-Nov-08 climshft2 climshft2i 17-Nov-08 climsqueeze climsqueezei 17-Nov-08 climsqueeze2 climsqueeze2i 17-Nov-08 climsub climsubi 17-Nov-08 climsubc2 climsubc2i 17-Nov-08 climsup climsupi 17-Nov-08 climub climubi 17-Nov-08 climubi climubii 17-Nov-08 climuni climunii 17-Nov-08 climunii climuniii 17-Nov-08 climuz0 climuz0i 17-Nov-08 clm0 clm0i 17-Nov-08 clm0i clm0ii 17-Nov-08 clm0nns clm0nnsi 17-Nov-08 clm1 clm1i 17-Nov-08 clm2 clm2i 17-Nov-08 clm3 clm3i 17-Nov-08 clm4 clm4i 17-Nov-08 clm4at clm4ati 17-Nov-08 clm4f clm4fi 17-Nov-08 clm4le clm4lei 17-Nov-08 clmi1 clmi1i 17-Nov-08 clmi2 clmi2i 17-Nov-08 clmi2rp clmi2rpi 17-Nov-08 clmnns clmnnsi 17-Nov-08 cnegex cnegexi 17-Nov-08 cosadd cosaddi 17-Nov-08 crim crimi 17-Nov-08 crmul crmuli 17-Nov-08 crne0 crne0i 17-Nov-08 crre crrei 17-Nov-08 crrecz crreczi 17-Nov-08 cru crui 17-Nov-08 cvg1 cvg1i 17-Nov-08 cvg1i cvg1ii 17-Nov-08 cvg2 cvg2i 17-Nov-08 cvg3 cvg3i 17-Nov-08 cvganuz cvganuzi 17-Nov-08 cvgcmp cvgcmpi 17-Nov-08 cvgcmp2 cvgcmp2i 17-Nov-08 cvgcmp2c cvgcmp2ci 17-Nov-08 cvgcmp3c cvgcmp3ci 17-Nov-08 cvgcmp3ce cvgcmp3cei 17-Nov-08 cvgcmp3cet cvgcmp3ceti 17-Nov-08 cvgcmpub cvgcmpubi 17-Nov-08 cvgrat cvgrati 17-Nov-08 dfef2 dfef2i 17-Nov-08 dfuz dfuzi 17-Nov-08 div0 div0i 17-Nov-08 div1 div1i 17-Nov-08 div11 div11i 17-Nov-08 div23 div23i 17-Nov-08 divadddiv divadddivi 17-Nov-08 divass divassi 17-Nov-08 divassz divasszi 17-Nov-08 divcan1 divcan1i 17-Nov-08 divcan1z divcan1zi 17-Nov-08 divcan2 divcan2i 17-Nov-08 divcan2z divcan2zi 17-Nov-08 divcan3 divcan3i 17-Nov-08 divcan3z divcan3zi 17-Nov-08 divcan4 divcan4i 17-Nov-08 divcan4z divcan4zi 17-Nov-08 divcl divcli 17-Nov-08 divclz divclzi 17-Nov-08 divdir divdiri 17-Nov-08 divdirz divdirzi 17-Nov-08 divdiv23 divdiv23i 17-Nov-08 divdiv23z divdiv23zi 17-Nov-08 divdivdiv divdivdivi 17-Nov-08 divge0 divge0i 17-Nov-08 divgt0 divgt0i 17-Nov-08 divgt0i divgt0ii 17-Nov-08 divgt0i2 divgt0i2i 17-Nov-08 divid dividi 17-Nov-08 divmul divmuli 17-Nov-08 divmul13 divmul13i 17-Nov-08 divmuldiv divmuldivi 17-Nov-08 divmulz divmulzi 17-Nov-08 divne0 divne0i 17-Nov-08 divrec divreci 17-Nov-08 divrecz divreczi 17-Nov-08 divval divvali 17-Nov-08 dsupivth dsupivthi 17-Nov-08 ef01tlub ef01tlubi 17-Nov-08 ef1tlub ef1tlubi 17-Nov-08 ef4p ef4pi 17-Nov-08 efadd efaddi 17-Nov-08 efcj efcji 17-Nov-08 effsumle effsumlei 17-Nov-08 efge1 efge1i 17-Nov-08 efge1p efge1pi 17-Nov-08 efgt0 efgt0i 17-Nov-08 efgt1 efgt1i 17-Nov-08 eflegeo eflegeoi 17-Nov-08 eflt eflti 17-Nov-08 efltb efltbi 17-Nov-08 efm1legeo efm1legeoi 17-Nov-08 efm1lim efm1limi 17-Nov-08 efsep efsepi 17-Nov-08 eft0val eft0vali 17-Nov-08 eftabs eftabsi 17-Nov-08 eftlclt eftlclti 17-Nov-08 eftlext eftlexti 17-Nov-08 elcncf1d elcncf1di 17-Nov-08 elcncf1i elcncf1ii 17-Nov-08 elfzel2 elfzel2i 17-Nov-08 elrpi elrpii 17-Nov-08 eluz1 eluz1i 17-Nov-08 eluzaddi eluzaddii 17-Nov-08 eluzsubi eluzsubii 17-Nov-08 eqle eqlei 17-Nov-08 eqneg eqnegi 17-Nov-08 expcnv expcnvi 17-Nov-08 fnsmnt fnsmnti 17-Nov-08 fseqsupub fseqsupubi 17-Nov-08 fsum1 fsum1i 17-Nov-08 fsum1f fsum1fi 17-Nov-08 fsum2 fsum2i 17-Nov-08 fsum3 fsum3i 17-Nov-08 fsum4 fsum4i 17-Nov-08 fsump1 fsump1i 17-Nov-08 fsump1f fsump1fi 17-Nov-08 fsumser0f fsumser0fi 17-Nov-08 fsumser1f fsumser1fi 17-Nov-08 fsumserz fsumserzi 17-Nov-08 fsumserz2 fsumserz2i 17-Nov-08 fsumserzf fsumserzfi 17-Nov-08 fzelp1 fzelp1i 17-Nov-08 geoser geoseri 17-Nov-08 geosum geosumi 17-Nov-08 gt0ne0 gt0ne0i 17-Nov-08 gt0ne0i gt0ne0ii 17-Nov-08 halfpos halfposi 17-Nov-08 hbneg hbnegi 17-Nov-08 hbnegd hbnegdi 17-Nov-08 hbsum hbsumi 17-Nov-08 hbsum1 hbsum1i 17-Nov-08 icoshftf1oi icoshftf1oii 17-Nov-08 imadd imaddi 17-Nov-08 imcj imcji 17-Nov-08 imcl imcli 17-Nov-08 immul immuli 17-Nov-08 imneg imnegi 17-Nov-08 infcvg infcvgi 17-Nov-08 infcvgaux1 infcvgaux1i 17-Nov-08 infcvgaux2 infcvgaux2i 17-Nov-08 ipcn ipcni 17-Nov-08 iserzabs iserzabsi 17-Nov-08 iserzcmp iserzcmpi 17-Nov-08 iserzcmp0 iserzcmp0i 17-Nov-08 iserzex iserzexi 17-Nov-08 iserzext iserzexti 17-Nov-08 iserzgt0 iserzgt0i 17-Nov-08 iserzmulc1 iserzmulc1i 17-Nov-08 iserzshft iserzshfti 17-Nov-08 iserzshft2 iserzshft2i 17-Nov-08 isum0split isum0spliti 17-Nov-08 isum1clim isum1climi 17-Nov-08 isum1p isum1pi 17-Nov-08 isumclim2t isumclim2ti 17-Nov-08 isumclim2tf isumclim2tfi 17-Nov-08 isumclim3t isumclim3ti 17-Nov-08 isumclim4t isumclim4ti 17-Nov-08 isumclim5t isumclim5ti 17-Nov-08 isumclimt isumclimti 17-Nov-08 isumclimtf isumclimtfi 17-Nov-08 isumclt isumclti 17-Nov-08 isumcmpi isumcmpii 17-Nov-08 isummulc1 isummulc1i 17-Nov-08 isummulc1ALT isummulc1iALT 17-Nov-08 isummulc1a isummulc1ai 17-Nov-08 isumnn0nn isumnn0nni 17-Nov-08 isumnn0nna isumnn0nnai 17-Nov-08 isumnul isumnuli 17-Nov-08 isumreclt isumreclti 17-Nov-08 isumshft isumshfti 17-Nov-08 isumshft2 isumshft2i 17-Nov-08 isumsplit isumspliti 17-Nov-08 isumval2t isumval2ti 17-Nov-08 isumvalt isumvalti 17-Nov-08 isumvaltf isumvaltfi 17-Nov-08 isupivth isupivthi 17-Nov-08 le2add le2addi 17-Nov-08 le2msq le2msqi 17-Nov-08 le2sq le2sqi 17-Nov-08 le2tri3 le2tri3i 17-Nov-08 leabs leabsi 17-Nov-08 leadd1 leadd1i 17-Nov-08 leadd2 leadd2i 17-Nov-08 lecase lecasei 17-Nov-08 ledivp1 ledivp1i 17-Nov-08 leid leidi 17-Nov-08 leloe leloei 17-Nov-08 lelttr lelttri 17-Nov-08 lelttrd lelttrdi 17-Nov-08 lemul1 lemul1i 17-Nov-08 lemul2 lemul2i 17-Nov-08 leneg lenegi 17-Nov-08 lenegcon1 lenegcon1i 17-Nov-08 lenlt lenlti 17-Nov-08 lerec lereci 17-Nov-08 lesub0 lesub0i 17-Nov-08 lesubadd lesubaddi 17-Nov-08 lesubadd2 lesubadd2i 17-Nov-08 letr letri 17-Nov-08 letrd letrdi 17-Nov-08 letri letrii 17-Nov-08 letri3 letri3i 17-Nov-08 lt2add lt2addi 17-Nov-08 lt2msq lt2msqi 17-Nov-08 lt2sq lt2sqi 17-Nov-08 ltadd1 ltadd1i 17-Nov-08 ltadd2 ltadd2i 17-Nov-08 ltaddpos ltaddposi 17-Nov-08 ltaddsub ltaddsubi 17-Nov-08 ltdiv1 ltdiv1i 17-Nov-08 ltdiv1i ltdiv1ii 17-Nov-08 ltdiv23 ltdiv23i 17-Nov-08 ltdiv23i ltdiv23ii 17-Nov-08 ltdivp1 ltdivp1i 17-Nov-08 ltle ltlei 17-Nov-08 ltlei ltleii 17-Nov-08 ltlen ltleni 17-Nov-08 ltletr ltletri 17-Nov-08 ltletrd ltletrdi 17-Nov-08 ltmul1 ltmul1i 17-Nov-08 ltmul1i ltmul1ii 17-Nov-08 ltmul2 ltmul2i 17-Nov-08 ltmuldiv ltmuldivi 17-Nov-08 ltne ltnei 17-Nov-08 ltneg ltnegi 17-Nov-08 ltnegcon1 ltnegcon1i 17-Nov-08 ltnegcon2 ltnegcon2i 17-Nov-08 ltnle ltnlei 17-Nov-08 ltnr ltnri 17-Nov-08 ltnsym ltnsymi 17-Nov-08 ltp1 ltp1i 17-Nov-08 ltrec ltreci 17-Nov-08 ltreci ltrecii 17-Nov-08 ltsubadd ltsubaddi 17-Nov-08 ltsubadd2 ltsubadd2i 17-Nov-08 lttr lttri 17-Nov-08 lttrd lttrdi 17-Nov-08 lttri2 lttri2i 17-Nov-08 lttri3 lttri3i 17-Nov-08 msq0 msq0i 17-Nov-08 msq11 msq11i 17-Nov-08 msqge0 msqge0i 17-Nov-08 msqgt0 msqgt0i 17-Nov-08 mul01 mul01i 17-Nov-08 mul02 mul02i 17-Nov-08 mul0or mul0ori 17-Nov-08 mul12 mul12i 17-Nov-08 mul23 mul23i 17-Nov-08 mul2neg mul2negi 17-Nov-08 mul4 mul4i 17-Nov-08 muladd muladdi 17-Nov-08 mulass mulassi 17-Nov-08 mulcan mulcani 17-Nov-08 mulcant2 mulcant2i 17-Nov-08 mulcl mulcli 17-Nov-08 mulcom mulcomi 17-Nov-08 mulge0 mulge0i 17-Nov-08 mulgt0 mulgt0i 17-Nov-08 mulgt0i mulgt0ii 17-Nov-08 mulid1 mulid1i 17-Nov-08 mulid2 mulid2i 17-Nov-08 mulm1 mulm1i 17-Nov-08 muln0 muln0i 17-Nov-08 mulneg1 mulneg1i 17-Nov-08 mulneg2 mulneg2i 17-Nov-08 neg11 neg11i 17-Nov-08 negcl negcli 17-Nov-08 negcon1 negcon1i 17-Nov-08 negcon2 negcon2i 17-Nov-08 negdi negdii 17-Nov-08 negeu negeui 17-Nov-08 negfcncf negfcncfi 17-Nov-08 negid negidi 17-Nov-08 negn0 negn0i 17-Nov-08 negne0 negne0i 17-Nov-08 negneg negnegi 17-Nov-08 negreb negrebi 17-Nov-08 negsub negsubi 17-Nov-08 negsubdi negsubdii 17-Nov-08 negsubdi2 negsubdi2i 17-Nov-08 nn0addcl nn0addcli 17-Nov-08 nn0addge1 nn0addge1i 17-Nov-08 nn0addge2 nn0addge2i 17-Nov-08 nn0cn nn0cni 17-Nov-08 nn0ge0 nn0ge0i 17-Nov-08 nn0le2msqt nn0le2msqti 17-Nov-08 nn0le2x nn0le2xi 17-Nov-08 nn0lele2x nn0lele2xi 17-Nov-08 nn0mulcl nn0mulcli 17-Nov-08 nn0opth nn0opthi 17-Nov-08 nn0opth2 nn0opth2i 17-Nov-08 nn0re nn0rei 17-Nov-08 nncn nncni 17-Nov-08 nneo nneoi 17-Nov-08 nnesq nnesqi 17-Nov-08 nngt0 nngt0i 17-Nov-08 nnlesq nnlesqi 17-Nov-08 nnne0 nnne0i 17-Nov-08 nnnn0 nnnn0i 17-Nov-08 nnre nnrei 17-Nov-08 nnsqcl nnsqcli 17-Nov-08 nnsub nnsubi 17-Nov-08 om2uz0 om2uz0i 17-Nov-08 om2uzf1o om2uzf1oi 17-Nov-08 om2uziso om2uzisoi 17-Nov-08 om2uzlt om2uzlti 17-Nov-08 om2uzlt2 om2uzlt2i 17-Nov-08 om2uzran om2uzrani 17-Nov-08 om2uzsuc om2uzsuci 17-Nov-08 om2uzuz om2uzuzi 17-Nov-08 peano2zd peano2zdi 17-Nov-08 peano5nn peano5nni 17-Nov-08 peano5uz peano5uzi 17-Nov-08 peano5uzt peano5uzti 17-Nov-08 pm2.61ltle pm2.61ltlei 17-Nov-08 pncan3 pncan3i 17-Nov-08 pnncan pnncani 17-Nov-08 posdif posdifi 17-Nov-08 posex posexi 17-Nov-08 prodge0 prodge0i 17-Nov-08 prodgt0 prodgt0i 17-Nov-08 readd readdi 17-Nov-08 readdcl readdcli 17-Nov-08 rec11 rec11i 17-Nov-08 rec11i rec11ii 17-Nov-08 reccl reccli 17-Nov-08 recclz recclzi 17-Nov-08 reccnv reccnvi 17-Nov-08 receu receui 17-Nov-08 recex recexi 17-Nov-08 recgt0 recgt0i 17-Nov-08 recgt0i recgt0ii 17-Nov-08 recid recidi 17-Nov-08 recidz recidzi 17-Nov-08 recj recji 17-Nov-08 recl recli 17-Nov-08 recn recni 17-Nov-08 recnd recndi 17-Nov-08 recne0z recne0zi 17-Nov-08 recrec recreci 17-Nov-08 recvalz recvalzi 17-Nov-08 redivcl redivcli 17-Nov-08 redivclz redivclzi 17-Nov-08 reef11 reef11i 17-Nov-08 reefcl reefcli 17-Nov-08 reeftlclt reeftlclti 17-Nov-08 reim0b reim0bi 17-Nov-08 releabs releabsi 17-Nov-08 remul remuli 17-Nov-08 remulcl remulcli 17-Nov-08 reneg renegi 17-Nov-08 renegcl renegcli 17-Nov-08 replim replimi 17-Nov-08 rereb rerebi 17-Nov-08 rereccl rereccli 17-Nov-08 rerecclz rerecclzi 17-Nov-08 resqcl resqcli 17-Nov-08 resubcl resubcli 17-Nov-08 reuunineg reuuninegi 17-Nov-08 seq00 seq00i 17-Nov-08 seq01 seq01i 17-Nov-08 seq0fn seq0fni 17-Nov-08 seq0fval seq0fvali 17-Nov-08 seq0p1 seq0p1i 17-Nov-08 seq0seqz seq0seqzi 17-Nov-08 seq0valt seq0valti 17-Nov-08 seq11 seq11i 17-Nov-08 seq1bnd seq1bndi 17-Nov-08 seq1cl seq1cli 17-Nov-08 seq1cl2 seq1cl2i 17-Nov-08 seq1f seq1fi 17-Nov-08 seq1f2 seq1f2i 17-Nov-08 seq1fn seq1fni 17-Nov-08 seq1m1 seq1m1i 17-Nov-08 seq1p1 seq1p1i 17-Nov-08 seq1res seq1resi 17-Nov-08 seq1rn seq1rni 17-Nov-08 seq1rn2 seq1rn2i 17-Nov-08 seq1rval seq1rvali 17-Nov-08 seq1seq0 seq1seq0i 17-Nov-08 seq1seq02t seq1seq02ti 17-Nov-08 seq1seq0t seq1seq0ti 17-Nov-08 seq1seqz seq1seqzi 17-Nov-08 seq1shftid seq1shftidi 17-Nov-08 seq1ub seq1ubi 17-Nov-08 seq1val seq1vali 17-Nov-08 seq1val2 seq1val2i 17-Nov-08 seqz1 seqz1i 17-Nov-08 seqzcl seqzcli 17-Nov-08 seqzeq seqzeqi 17-Nov-08 seqzfn seqzfni 17-Nov-08 seqzfval seqzfvali 17-Nov-08 seqzfval2 seqzfval2i 17-Nov-08 seqzfveq seqzfveqi 17-Nov-08 seqzm1 seqzm1i 17-Nov-08 seqzp1 seqzp1i 17-Nov-08 seqzres seqzresi 17-Nov-08 seqzres2 seqzres2i 17-Nov-08 seqzresval seqzresvali 17-Nov-08 seqzrn seqzrni 17-Nov-08 seqzrn2 seqzrn2i 17-Nov-08 seqzval2t seqzval2ti 17-Nov-08 seqzvalt seqzvalti 17-Nov-08 ser00 ser00i 17-Nov-08 ser0cj ser0cji 17-Nov-08 ser0cl1 ser0cl1i 17-Nov-08 ser0clt ser0clti 17-Nov-08 ser0f ser0fi 17-Nov-08 ser0mulc ser0mulci 17-Nov-08 ser0p1 ser0p1i 17-Nov-08 ser11 ser11i 17-Nov-08 ser1absdif ser1absdifi 17-Nov-08 ser1add ser1addi 17-Nov-08 ser1add2 ser1add2i 17-Nov-08 ser1cl1 ser1cl1i 17-Nov-08 ser1cl2 ser1cl2i 17-Nov-08 ser1clt ser1clti 17-Nov-08 ser1cmp ser1cmpi 17-Nov-08 ser1cmp0 ser1cmp0i 17-Nov-08 ser1cmp2 ser1cmp2i 17-Nov-08 ser1const ser1consti 17-Nov-08 ser1f ser1fi 17-Nov-08 ser1f0 ser1f0i 17-Nov-08 ser1f2 ser1f2i 17-Nov-08 ser1mono ser1monoi 17-Nov-08 ser1mulc ser1mulci 17-Nov-08 ser1p1 ser1p1i 17-Nov-08 ser1recl ser1recli 17-Nov-08 ser1ref ser1refi 17-Nov-08 ser1ser0 ser1ser0i 17-Nov-08 serz1p serz1pi 17-Nov-08 serzcj serzcji 17-Nov-08 serzcl1 serzcl1i 17-Nov-08 serzcl2t serzcl2ti 17-Nov-08 serzclt serzclti 17-Nov-08 serzcmp serzcmpi 17-Nov-08 serzcmp0 serzcmp0i 17-Nov-08 serzf0 serzf0i 17-Nov-08 serzfsum serzfsumi 17-Nov-08 serzim serzimi 17-Nov-08 serzmulc serzmulci 17-Nov-08 serzmulc1 serzmulc1i 17-Nov-08 serzre serzrei 17-Nov-08 serzreclt serzreclti 17-Nov-08 serzref serzrefi 17-Nov-08 serzsplit serzspliti 17-Nov-08 shftcan1t shftcan1ti 17-Nov-08 shftcan2t shftcan2ti 17-Nov-08 shftf shftfi 17-Nov-08 shftfn shftfni 17-Nov-08 shftfval shftfvali 17-Nov-08 shftidt shftidti 17-Nov-08 shftres shftresi 17-Nov-08 shftresvalt shftresvalti 17-Nov-08 shftval2t shftval2ti 17-Nov-08 shftval3t shftval3ti 17-Nov-08 shftval4t shftval4ti 17-Nov-08 shftval5t shftval5ti 17-Nov-08 shftvalt shftvalti 17-Nov-08 sinadd sinaddi 17-Nov-08 sq11 sq11i 17-Nov-08 sqabsadd sqabsaddi 17-Nov-08 sqabssub sqabssubi 17-Nov-08 sqcl sqcli 17-Nov-08 sqdiv sqdivi 17-Nov-08 sqeq0 sqeq0i 17-Nov-08 sqeqor sqeqori 17-Nov-08 sqge0 sqge0i 17-Nov-08 sqgt0 sqgt0i 17-Nov-08 sqmul sqmuli 17-Nov-08 sqr11 sqr11i 17-Nov-08 sqrcl sqrcli 17-Nov-08 sqreci sqrecii 17-Nov-08 sqrge0 sqrge0i 17-Nov-08 sqrgt0 sqrgt0i 17-Nov-08 sqrgt0i sqrgt0ii 17-Nov-08 sqrle sqrlei 17-Nov-08 sqrlt sqrlti 17-Nov-08 sqrmsq sqrmsqi 17-Nov-08 sqrmsq2 sqrmsq2i 17-Nov-08 sqrmul sqrmuli 17-Nov-08 sqrmuli sqrmulii 17-Nov-08 sqrsq sqrsqi 17-Nov-08 sqrth sqrthi 17-Nov-08 sqsqr sqsqri 17-Nov-08 sqval sqvali 17-Nov-08 subadd subaddi 17-Nov-08 subadd2 subadd2i 17-Nov-08 subaddri subaddrii 17-Nov-08 subcan subcani 17-Nov-08 subcan2 subcan2i 17-Nov-08 subcl subcli 17-Nov-08 subdi subdii 17-Nov-08 subdir subdiri 17-Nov-08 subeq0 subeq0i 17-Nov-08 subge0 subge0i 17-Nov-08 subid subidi 17-Nov-08 subid1 subid1i 17-Nov-08 subneg subnegi 17-Nov-08 subsq subsqi 17-Nov-08 subsq0 subsq0i 17-Nov-08 subsub23 subsub23i 17-Nov-08 sumsqne0 sumsqne0i 17-Nov-08 sup3i sup3ii 17-Nov-08 suprcli suprclii 17-Nov-08 suprleubi suprleubii 17-Nov-08 suprlubi suprlubii 17-Nov-08 suprnubi suprnubii 17-Nov-08 suprubi suprubii 17-Nov-08 times2 times2i 17-Nov-08 uzinfm uzinfmi 17-Nov-08 uzrdgfnuz uzrdgfnuzi 17-Nov-08 uzrdgini uzrdginii 17-Nov-08 uzrdginip1 uzrdginip1i 17-Nov-08 uzrdgsuc uzrdgsuci 17-Nov-08 uzrdgval uzrdgvali 17-Nov-08 zre zrei 17-Nov-08 abs3lem abs3lemi 17-Nov-08 abs2difabs abs2difabsi 17-Nov-08 abs2dif abs2difi 17-Nov-08 2basgent 2basgen 17-Nov-08 basgent basgen 17-Nov-08 basgen2t basgen2 17-Nov-08 tgss3t tgss3 17-Nov-08 tgss2t tgss2 17-Nov-08 tgsst tgss 17-Nov-08 tgtop11t tgtop11 17-Nov-08 bastopt bastop 17-Nov-08 bastop bastop1 17-Nov-08 tgidmt tgidm 17-Nov-08 eltop3t eltop3 17-Nov-08 eltop2t eltop2 17-Nov-08 eltopt eltop 17-Nov-08 tgtopt tgtop 17-Nov-08 topbast topbas 17-Nov-08 eltg3t eltg3 17-Nov-08 tgval3t tgval3 17-Nov-08 tgclt tgcl 17-Nov-08 unitgt unitg 17-Nov-08 bastgt bastg 17-Nov-08 tg2t tg2 17-Nov-08 tg1t tg1 17-Nov-08 eltg2t eltg2 17-Nov-08 eltgt eltg 17-Nov-08 tgval2t tgval2 17-Nov-08 tgvalt tgval 17-Nov-08 basis2t basis2 17-Nov-08 basis1t basis1 17-Nov-08 0opnt 0opn 17-Nov-08 inopnt inopn 17-Nov-08 iunopnt iunopn 17-Nov-08 uniopnt uniopn 17-Nov-08 uniopn uniopn2 17-Nov-08 entrt entr 17-Nov-08 entr4 entr4i 17-Nov-08 entr3 entr3i 17-Nov-08 entr2 entr2i 17-Nov-08 entr entri 17-Nov-08 entri entric 17-Nov-08 rdglimt rdglim 17-Nov-08 onelpsst onelpss 17-Nov-08 rdgsuct rdgsuc 17-Nov-08 on0eqelt on0eqel 17-Nov-08 onelsst onelss 17-Nov-08 onsst onss 17-Nov-08 rdglim rdglimi 17-Nov-08 rdgsuc rdgsuci 17-Nov-08 nnon nnoni 17-Nov-08 onsucss onsucssi 17-Nov-08 onun onun2i 17-Nov-08 onssel onsseli 17-Nov-08 onuninsuc onuninsuci 17-Nov-08 onuniorsuc onuniorsuci 17-Nov-08 onunisuc onunisuci 17-Nov-08 onsuc onsuci 17-Nov-08 onelun oneluni 17-Nov-08 onelin onelini 17-Nov-08 onssneli2 onssnel2i 17-Nov-08 onelss onelssi 17-Nov-08 onss onssi 17-Nov-08 onel oneli 17-Nov-08 onirr onirri 17-Nov-08 ontrc ontrci 17-Nov-08 onord onordi 17-Nov-08 --- --- The *tr* inferences were changed to *tr*i, 17-Nov-08 --- --- for consistency with *tr*d 17-Nov-08 bitr bitri 17-Nov-08 bitr2 bitr2i 17-Nov-08 bitr3 bitr3i 17-Nov-08 bitr4 bitr4i 17-Nov-08 3bitr 3bitri 17-Nov-08 3bitrr 3bitrri 17-Nov-08 3bitr2 3bitr2i 17-Nov-08 3bitr3 3bitr3i 17-Nov-08 3bitr4 3bitr4i 17-Nov-08 3imtr3 3imtr3i 17-Nov-08 3imtr4 3imtr4i 17-Nov-08 eqtr eqtri 17-Nov-08 eqtr2 eqtr2i 17-Nov-08 eqtr3 eqtr3i 17-Nov-08 eqtr4 eqtr4i 17-Nov-08 3eqtr 3eqtri 17-Nov-08 3eqtrr 3eqtrri 17-Nov-08 3eqtr2 3eqtr2i 17-Nov-08 3eqtr3 3eqtr3i 17-Nov-08 3eqtr4 3eqtr4i 17-Nov-08 eq2tr eq2tri 17-Nov-08 eqeltr eqeltri 17-Nov-08 eqeltrr eqeltrri 17-Nov-08 eleqtr eleqtri 17-Nov-08 eleqtrr eleqtrri 17-Nov-08 eqsstr eqsstri 17-Nov-08 eqsstr3 eqsstr3i 17-Nov-08 sseqtr sseqtri 17-Nov-08 sseqtr4 sseqtr4i 17-Nov-08 3sstr3 3sstr3i 17-Nov-08 3sstr4 3sstr4i 17-Nov-08 eqbrtr eqbrtri 17-Nov-08 eqbrtrr eqbrtrri 17-Nov-08 breqtr breqtri 17-Nov-08 breqtrr breqtrri 17-Nov-08 3brtr3 3brtr3i 17-Nov-08 3brtr4 3brtr4i 16-Nov-08 opabsb opelopabsb 14-Nov-08 zfext2 axext3 14-Nov-08 axext axext2 14-Nov-08 nega notnot2 14-Nov-08 negai notnotri 14-Nov-08 negb notnot1 14-Nov-08 negbi notnoti 14-Nov-08 negbii notbii 14-Nov-08 negbid notbid 14-Nov-08 pm4.13 notnot 14-Nov-08 pm4.11 notbi 11-Nov-08 divmul3t [--same--] rearranged antecedent; renamed variables 11-Nov-08 divmul2t [--same--] rearranged antecedent; renamed variables 11-Nov-08 divmult [--same--] rearranged antecedent; renamed variables 11-Nov-08 elqsi [--same--] changed E. x ( x e. A /\ ... to E. x e. A ... 11-Nov-08 elqs [--same--] changed E. x ( x e. A /\ ... to E. x e. A ... 8-Nov-08 indistop [--same--] eliminated hypothesis A e. V 8-Nov-08 pri2 prid2 8-Nov-08 pri1 prid1 7-Nov-08 qdivclt [--same--] antecedent changed to use triple conjunction 6-Nov-08 rcfpfil [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 rcfpfillem6 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 rcfpfillem5 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 rcfpfillem4 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 rcfpfillem3 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 rcfpfillem2 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 rcfpfillem1 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fisub [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 filint2 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 efilcp [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fgsb [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fipfil2 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 sppfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fiv [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 df-fi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 emfin [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 ficli [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fiiu [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 abfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fine [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 infi1 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 spfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fctop [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 subbas2 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 subbas [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 istps5 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 istps4 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 istop2g [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 isfinite [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 pwfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 pwfilem [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 iunfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fofi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fodomfib [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 fodomfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 abfii5 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Nov-08 abfii4 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 31-Sep-08 isfinite1 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 31-Sep-08 domfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 31-Sep-08 unifi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 31-Sep-08 abfii1 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 31-Sep-08 abfii2 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 31-Sep-08 abfii3 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 10-Sep-08 isfinite2 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 9-Sep-08 finsucdom [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 7-Sep-08 ominf [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Sep-08 onfin [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Sep-08 pssinf {--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 6-Sep-08 divsubdirt [--same--] changed hyp. order 3-Sep-08 php3 [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 2-Sep-08 fiint [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 1-Sep-08 prfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 30-Aug-08 unfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 29-Aug-08 snfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 29-Aug-08 ssnnfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 29-Aug-08 ssfi [--same--] changed "E. ... e. om ... ~~ ..." to "e. Fin" 24-Aug-08 mulcant [--same--] changed antecendent order; swapped var. names 24-Aug-08 mulcan2t [--same--] changed antecendent order; swapped var. names 24-Aug-08 mulcant2 [--same--] changed hyp. order; swapped var. names 24-Aug-08 mulcan [--same--] changed hyp. order; swapped var. names 23-Aug-08 divcan4t [--same--] changed antecendent order; swapped var. names 23-Aug-08 divcan4z [--same--] changed hyp. order; swapped var. names 23-Aug-08 divcan3t [--same--] changed antecendent order; swapped var. names 23-Aug-08 divcan3z [--same--] changed hyp. order; swapped var. names 22-Aug-08 ssnn ssnnfi 22-Aug-08 divcan4 [--same--] changed hyp. order; swapped var. names 22-Aug-08 divcan3 [--same--] changed hyp. order; swapped var. names 21-Aug-08 pm4.2i biidd 21-Aug-08 divcan2t [--same--] changed antecendent order; swapped var. names 21-Aug-08 divcan2z [--same--] changed hyp. order; swapped var. names 20-Aug-08 divdirt [--same--] changed hyp. order 18-Aug-08 divcan2 [--same--] changed hyp. order; swapped var. names 18-Aug-08 divcan1t [--same--] changed antecendent order; swapped var. names 18-Aug-08 divcan1z [--same--] changed hyp. order; swapped var. names 18-Aug-08 divcan1 [--same--] changed hyp. order; swapped var. names 17-Aug-08 ltmuldiv2t [--same--] changed antecedent grouping 17-Aug-08 ltdivmult [--same--] changed antecedent grouping 17-Aug-08 ledivmult [--same--] changed antecedent grouping 17-Aug-08 ltdivmul2t [--same--] changed antecedent grouping 17-Aug-08 ledivmul2t [--same--] changed antecedent grouping 17-Aug-08 lemuldivt [--same--] changed antecedent grouping 17-Aug-08 lemuldiv2t [--same--] changed antecedent grouping 16-Aug-08 ltmuldivt [--same--] changed antecedent grouping 15-Aug-08 bii dfbi1 15-Aug-08 biigb dfbi1gb 15-Aug-08 bi dfbi2 15-Aug-08 dfbi dfbi3 14-Aug-08 lediv1t [--same--] changed antecedent grouping 14-Aug-08 ltdiv1t [--same--] changed antecedent grouping 10-Jul-08 expne0t [--same--] swapped biconditional 10-Jul-08 sq0t sqeq0t 10-Jul-08 sq00 sqeq0 7-Jul-08 syl3dan3 syld3an3 7-Jul-08 syl3dan2 syld3an2 31-May-08 isnvi [--same--] eliminated hypotheses G e. V, S e. V 31-May-08 isnvg --- obsolete; use isnv 31-May-08 isvcg --- obsolete; use isvc 31-May-08 ideq [--same--] eliminated hypothesis A e. V 31-May-08 ideqg [--same--] eliminated first antecedent A e. C 28-May-08 opelxpex --- obsolete; use opelxp1 22-May-08 ax9a ax9 22-May-08 ax9 ax9o 21-May-08 ax6-2 ax6 21-May-08 ax6-3 ax6o 21-May-08 ax-6 ax-6o 21-May-08 ax-5 ax-5o 17-May-08 ax-10 ax-10o 16-May-08 er2 dfer2 16-May-08 er2 dfer2 16-May-08 sb7 dfsb7 13-May-08 cla4e2v cla42ev 13-May-08 cla4e2gv cla42egv 12-May-08 a4w1 a4eiv 12-May-08 a4w a4imev 12-May-08 a4c1 a4imed 12-May-08 a4c a4ime 12-May-08 a4b1 a4v 12-May-08 a4b a4imv 12-May-08 a4at a4imt 12-May-08 a4a a4im 11-May-08 sbea4 a4sbe 11-May-08 sbia4 a4sbim 11-May-08 sbba4 a4sbbi 6-May-08 inf4 axinf2 6-May-08 minfnre mnfnre 27-Apr-08 sb6y sb6f 27-Apr-08 sb5y sb5f 17-Apr-08 sbn2 --- obsolete; use sbn 17-Apr-08 sbn1 --- obsolete; use sbn 9-Apr-08 isvci [--same--] weakened hyp from G : ... to dom G = ... 9-Apr-08 isabli [--same--] weakened hyp from G : ... to dom G = ... 2-Apr-08 19.2 [--same--] generalized to use 2 set variables 30-Mar-08 grprn [--same--] weakened hyp from G : ... to dom G = ... 11-Mar-08 absefimt absefit 11-Mar-08 axcnre [--same--] changed 'x. i' to 'i x.' 11-Mar-08 cnegexlem2 [--same--] changed 'x. i' to 'i x.' 11-Mar-08 cnegext [--same--] changed 'x. i' to 'i x.' 11-Mar-08 recextlem1 [--same--] changed 'x. i' to 'i x.' 11-Mar-08 recextlem2 [--same--] changed 'x. i' to 'i x.' 11-Mar-08 recext [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crulem [--same--] changed 'x. i' to 'i x.' 11-Mar-08 cru [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crut [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crne0 [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crmul [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crrecz [--same--] changed 'x. i' to 'i x.' 11-Mar-08 creur [--same--] changed 'x. i' to 'i x.' 11-Mar-08 creui [--same--] changed 'x. i' to 'i x.' 11-Mar-08 rimul [--same--] changed 'x. i' to 'i x.' 11-Mar-08 df-re [--same--] changed 'x. i' to 'i x.' 11-Mar-08 df-im [--same--] changed 'x. i' to 'i x.' 11-Mar-08 revalt [--same--] changed 'x. i' to 'i x.' 11-Mar-08 imvalt [--same--] changed 'x. i' to 'i x.' 11-Mar-08 replimt [--same--] changed 'x. i' to 'i x.' 11-Mar-08 df-cj [--same--] changed 'x. i' to 'i x.' 11-Mar-08 cjvalt [--same--] changed 'x. i' to 'i x.' 11-Mar-08 replim [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crret [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crimt [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crre [--same--] changed 'x. i' to 'i x.' 11-Mar-08 crim [--same--] changed 'x. i' to 'i x.' 11-Mar-08 efit4pt efi4pt changed 'x. i' to 'i x.' 10-Mar-08 fabex [--same--] added 3rd hypothesis 6-Mar-08 pm2.36 [--same--] corrected to match Principia Mathematica 6-Mar-08 pm2.37 [--same--] corrected to match Principia Mathematica 6-Mar-08 pm2.38 [--same--] corrected to match Principia Mathematica 2-Mar-08 csbiet csbiegft 2-Mar-08 csbie2g csbie2t 2-Mar-08 vsbcint sbhyp 2-Mar-08 cbvsbcv cbvralsv 1-Mar-08 sbcrex sbcrexg 1-Mar-08 sbcral sbcralg 1-Mar-08 19.23g 19.23t 1-Mar-08 19.21g 19.21t 1-Mar-08 minusex negex 1-Mar-08 negext cnegext 1-Mar-08 negex cnegex 29-Feb-08 hbneq hbne 29-Feb-08 hbne hbn 29-Feb-08 csbiet csbiegft 29-Feb-08 sbciet sbciegft 29-Feb-08 elabt elabgt 29-Feb-08 vtoclefg vtoclegft 23-Feb-08 sqdif0 subsq0 23-Feb-08 binom2a --- obsolete; use subsq 12-Feb-08 cnhl [--same--] added hypothesis to assign vector space to var 9-Feb-08 oneirr onirr 9-Feb-08 ordeirr ordirr 9-Feb-08 eirr elirr 9-Feb-08 eirrv elirrv 29-Jan-08 oibabs [--same--] swapped sides of biconditional 24-Jan-08 cos2t --- obsolete; use cos2tt 20-Jan-08 ffvrni ffvelrni 20-Jan-08 ffvrn ffvelrn 20-Jan-08 fnfvrn fnfvelrn 20-Jan-08 fvrn fvelrn 20-Jan-08 fvelrn fvelrnb 18-Jan-08 arch [--same--] changed x to n, changing $f hypothesis order 18-Jan-08 cos1lem4 8th4div3 18-Jan-08 eftlex --- obsolete; use eftlext 18-Jan-08 sin2t --- obsolete; use sin2tt 15-Jan-08 explt1t expord2t 15-Jan-08 eft0vallem eft0val 15-Jan-08 effsumlelem --- obsolete; use reeftclt 15-Jan-08 eftvallem eftval 15-Jan-08 efpartex eftlex 15-Jan-08 efcltlem4 efseq0ex 15-Jan-08 efcltlem2a ef0lem 15-Jan-08 dfef2lem dfef2 15-Jan-08 efcltlem3 efseq1ex 15-Jan-08 eftcltlem eftclt 15-Jan-08 eftabslem eftabs 12-Jan-08 rgen2xxx rgen2a 12-Jan-08 rgen2a rgen2 12-Jan-08 rgen2 rgen2xxx 12-Jan-08 cnbn [--same--] added hypothesis to assign vector space to var 12-Jan-08 cnph [--same--] added hypothesis to assign vector space to var 12-Jan-08 cnims [--same--] reorganized hypotheses and conclusion 14-Jan-08 rgen3 [--same--] generalized for 3 different class variables 12-Jan-08 cnnv [--same--] added hypothesis to assign vector space to var 10-Jan-08 zneo [--same--] changed -. ... = to =/= 3-Jan-08 ax7-467 ax467to7 3-Jan-08 ax6-467 ax467to6 3-Jan-08 ax4-467 ax467to4 3-Jan-08 ax6-67 ax67to6 3-Jan-08 ax7-67 ax67to7 3-Jan-08 ax4-46 ax46to4 3-Jan-08 ax5-46 ax46to5 29-Dec-07 eftvallem [--same--] added hypothesis 22-Dec-07 zfnuleu [--same--] added $e hypothesis to remove ax-nul dependency 8-Dec-07 supxrre2 [--same--] changed -. ... = to =/= 23-Nov-07 sub4 addsub4 23-Nov-07 sub4t addsub4t 17-Nov-07 climres [--same--] generalized antecedent from A e. CC to A e. B 12-Nov-07 climle climcmp 11-Nov-07 eqneqi necon3bii 11-Nov-07 eqneqd necon3bid 10-Nov-07 ser0cj [--same--] weakened hypotheses 9-Nov-07 ser1cj --- obsolete; derive from serzcj (as in ser0cj) 9-Nov-07 ser0re --- obsolete; derive from serzre (as in ser0cj) 9-Nov-07 ser1re --- obsolete; derive from serzre (as in ser0cj) 8-Nov-07 mp3dan mp3dan23 23-Oct-07 pm3.27bd pm3.27bi 23-Oct-07 pm3.26bd pm3.26bi 16-Oct-07 expbndt expubndt 16-Oct-07 expge1t [--same--] strengthened from N e. NN to N e. NN0 12-Oct-07 kmlem15 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem14 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem13 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem10 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem9 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem7 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem5 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem4 [--same--] changed -. ... = to =/= 12-Oct-07 kmlem3 [--same--] changed -. ... = to =/= 5-Oct-07 1open topopn 5-Oct-07 1clsd topcld 3-Oct-07 intss3 ntrss3 2-Oct-07 isopen3 isopn3 2-Oct-07 isopen2 isopn2 2-Oct-07 cmclsopen cmclsopn 2-Oct-07 snclsd sncld 2-Oct-07 clsdlp cldlp 2-Oct-07 isclsd3 iscld3 2-Oct-07 cmntrclsd cmntrcld 2-Oct-07 clsclsd clscld 2-Oct-07 clsdcls cldcls 2-Oct-07 unclsd uncld 2-Oct-07 intclsd intcld 2-Oct-07 iinclsd iincld 2-Oct-07 0clsd 0cld 2-Oct-07 openclsd opncld 2-Oct-07 clsdopen cldopn 2-Oct-07 clsdss cldss 2-Oct-07 isclsd2 iscld2 2-Oct-07 isclsd iscld 2-Oct-07 clsdval cldval 2-Oct-07 df-clsd df-cld 2-Oct-07 isopn2 isopn4 28-Sep-07 --- --- changed math symbol from "floor" to "|_" 26-Sep-07 ser0cl ser0cl1 26-Sep-07 ser1cl ser1cl1 25-Sep-07 ser1re2 ser1re 25-Sep-07 ser1re ser1ref 23-Sep-07 df-fac [--same--] swapped arguments of union 23-Sep-07 seqzrnx seqzrn 23-Sep-07 seqzrn seqzrn2 23-Sep-07 seqzrn2 seqzrnx 23-Sep-07 seq1rnx seq1rn 23-Sep-07 seq1rn seq1rn2 23-Sep-07 seq1rn2 seq1rnx 17-Sep-07 pm2.21nd pm2.24d 17-Sep-07 pm2.21ni pm2.24i 16-Sep-07 dvelimf2 dvelimfALT 8-Sep-07 lemul2it [--same--] rearranged antecedent 8-Sep-07 lemul1it [--same--] rearranged antecedent 7-Sep-07 0vval 0vfval 4-Sep-07 --- --- Many changes after df-ms, described in the 4-Sep-2007 entry of us.metamath.org/mpegif/mmnotes.txt 4-Sep-07 elssab --- obsolete; use elssabg 4-Sep-07 nvc nvvc 4-Sep-07 --- --- changed math symbol from "Met" to "MetSp" 4-Sep-07 --- --- changed math symbol from "CMet" to "CMetSp" 25-Aug-07 fopabco fopabcos 21-Aug-07 xrltnet [--same--] changed -. A = B to B =/= A; triple conjunction 21-Aug-07 lttri2 [--same--] changed -. A = B to A =/= B 21-Aug-07 lttri2t [--same--] changed -. A = B to A =/= B 15-Aug-07 sbccsbg sbccsb2g 11-Aug-07 recdivt [--same--] rearranged antecedent 9-Aug-07 funopabex2g opabex2g 9-Aug-07 funopabex2 opabex2 9-Aug-07 funopabex opabex 9-Aug-07 cnco [--same--] swapped 2nd & 3rd args in 1st triple conj 6-Aug-07 --- --- changed "ncv" to "nv" in the labels of: cncv df-ncv ncvss ncvrel ncvop ncvvop isncvg isncvi ncvi ncvv ncvgcl ncvscl ncvf ncvcl ncvcli ncvdm ncvs ncvm1 ncvdif ncvpi ncvz0 ncvz ncvtri ncvabs ncvge0 cnncv cnncv0 elimncvu ncvnd phncv bnncv hlncv hilncv 4-Aug-07 subval --- obsolete; use subvalt 31-Jul-07 divge0t [--same--] rearranged antecedent 31-Jul-07 divgt0t [--same--] rearranged antecedent 31-Jul-07 ltne [--same--] changed -. A = B to B =/= A 31-Jul-07 ltnet [--same--] changed -. A = B to B =/= A; triple conjunction 31-Jul-07 ltlen [--same--] changed -. A = B to B =/= A 31-Jul-07 ltlent [--same--] changed -. A = B to B =/= A 22-Jul-07 xrleltnet [--same--] changed -. A = B to B =/= A 20-Jul-07 nngt1ne1t [--same--] changed -. A = 1 to A =/= 1 18-Jul-07 leltnet [--same--] changed -. A = B to B =/= A 15-Ju1-07 zornx zorn 15-Ju1-07 zorn zorn2 15-Ju1-07 zorn2 zornx 18-Jun-07 caucvglem2 [--same--] changed -. S = (/) to S =/= (/) 17-Jun-07 seq1ublem [--same--] changed -. ... = (/) to =/= (/) 17-Jun-07 suppr supexpr 17-Jun-07 ruclem33 [--same--] changed -. ... = (/) to =/= (/) 16-Jun-07 ltrec1t [--same--] rearranged antecedent 15-Jun-07 lerec2t [--same--] rearranged antecedent 3-Jun-07 nordeq [--same--] changed -. A = B to A =/= B 3-Jun-07 xpsndisj [--same--] changed -. A = B to A =/= B 2-Jun-07 peano3 [--same--] changed -. A = (/) to A =/= (/) 2-Jun-07 disjsn2 [--same--] changed -. A = B to A =/= B 2-Jun-07 fun2ssres [--same--] antecedent changed to use triple conjunction 2-Jun-07 onelpsst [--same--] changed -. A = B to A =/= B 1-Jun-07 ordelssne [--same--] changed -. A = B to A =/= B 1-Jun-07 suprleubi [--same--] changed -. A = (/) to A =/= (/) 31-May-07 suprnubi [--same--] changed -. A = (/) to A =/= (/) 30-Mar-07 onssmin [--same--] changed -. A = (/) to A =/= (/) 29-May-07 suprlub [--same--] changed -. A = (/) to A =/= (/) 29-May-07 funssfv [--same--] antecedent changed to use triple conjunction 29-May-07 limuni3 [--same--] changed -. A = (/) to A =/= (/) 29-May-07 ordge1n0 [--same--] changed -. A = (/) to A =/= (/) 28-May-07 onmindif2 [--same--] changed -. A = (/) to A =/= (/) 28-May-07 suprleub [--same--] changed -. A = (/) to A =/= (/) 28-May-07 tz7.7 [--same--] changed -. B = A to B =/= A 27-May-07 nnullss [--same--] changed -. ... = (/) to =/= (/) 27-May-07 supxrre2 [--same--] changed -. A = (/) to A =/= (/) 27-May-07 fodomfib [--same--] changed -. A = (/) to A =/= (/) 26-May-07 supxrre1 [--same--] changed -. A = (/) to A =/= (/) 24-May-07 supxrgtmnf [--same--] changed -. A = (/) to A =/= (/) 23-May-07 ltmsqt --- obsolete; use msqgt0t 23-May-07 msqgt0 [--same--] changed -. A = (/) to A =/= (/) 22-May-07 supxrbnd [--same--] changed -. A = (/) to A =/= (/) 21-May-07 suprnub [--same--] changed -. A = (/) to A =/= (/) 21-May-07 19.3r --- obsolete; use 19.3 21-May-07 19.9rv --- obsolete; use 19.9v 20-May-07 19.9r --- obsolete; use 19.9 17-May-07 iunn0 [--same--] changed -. ... = (/) to =/= (/) 17-May-07 iinon [--same--] changed -. A = (/) to A =/= (/) 17-May-07 map0 [--same--] changed -. B = (/) to B =/= (/) 16-May-07 infmrcl [--same--] changed -. A = (/) to A =/= (/) 16-May-07 suprub [--same--] changed -. A = (/) to A =/= (/) 16-May-07 suprcli [--same--] changed -. A = (/) to A =/= (/) 16-May-07 suprubi [--same--] changed -. A = (/) to A =/= (/) 16-May-07 suprlubi [--same--] changed -. A = (/) to A =/= (/) 14-May-07 sup3i [--same--] changed -. A = (/) to A =/= (/) 13-May-07 kmlemxx kmlem8 changed -. ... = (/) to =/= (/) 13-May-07 kmlem8 kmlem9 13-May-07 kmlem9 kmlem10 13-May-07 kmlem10 kmlem11 13-May-07 kmlem11 kmlem12 changed -. ... = to =/= 13-May-07 kmlem12 kmlem13 changed -. ... = to =/= 13-May-07 kmlem13 kmlemxx 13-May-07 supxrre [--same--] changed -. A = (/) to A =/= (/) 13-May-07 infmsup [--same--] changed -. A = (/) to A =/= (/) 13-May-07 suprcl [--same--] changed -. A = (/) to A =/= (/) 12-May-07 kmlem1 [--same--] changed -. ... = to =/= 12-May-07 kmlem3 [--same--] changed -. ... = to =/= 12-May-07 kmlem6 [--same--] changed -. ... = to =/= 12-May-07 kmlem7 [--same--] changed -. ... = to =/= 11-May-07 infm3 [--same--] changed -. A = (/) to A =/= (/) 11-May-07 sup3 [--same--] changed -. A = (/) to A =/= (/) 10-May-07 oneqmin [--same--] changed -. B = (/) to B =/= (/) 10-May-07 infmssuzcl [--same--] changed -. S = (/) to S =/= (/) 5-May-07 xpexr2 [--same--] changed -. ... = (/) to =/= (/) 5-May-07 tz7.49c [--same--] changed -. ... = to =/= 4-May-07 tz7.49 [--same--] changed -. ... = to =/= 4-May-07 funimass2 [--same--] conjoined antecedents in hypothesis 3-May-07 ac4c [--same--] changed -. x = (/) to x =/= (/) 30-Apr-07 aceq6b [--same--] changed -. z = (/) to z =/= (/) 30-Apr-07 disjpss [--same--] changed -. B = (/) to B =/= (/) 30-Apr-07 infxpidmlem10 [--same--] changed -. g = (/) to g =/= (/) 30-Apr-07 1ne0 [--same--] changed -. 1o = (/) to 1o =/= (/) 30-Apr-07 ac5b [--same--] changed -. x = (/) to x =/= (/) 30-Apr-07 aceq6a [--same--] changed -. z = (/) to z =/= (/) 30-Apr-07 on0eln0 [--same--] changed -. A = (/) to A =/= (/) 28-Apr-07 tz7.2 [--same--] changed -. B = A to B =/= A; triple conjunction 25-Apr-07 ac5 [--same--] changed -. x = (/) to x =/= (/) 23-Apr-07 ac4 [--same--] changed -. z = (/) to z =/= (/) 22-Apr-07 ac8 [--same--] changed -. ... = to =/= 22-Apr-07 uzwo2 [--same--] changed -. S = (/) to S =/= (/) 21-Apr-07 aceq5 [--same--] changed -. ... = to =/= 21-Apr-07 epfrc [--same--] -. B = (/) to B =/= (/); triple conjunction 20-Apr-07 dfepfr [--same--] changed -. x = (/) to x =/= (/) 19-Apr-07 xpnz [--same--] changed -. ... = (/) to =/= (/) 18-Apr-07 ltexprlem1 [--same--] changed -. C = (/) to C =/= (/) 17-Apr-07 uzwo [--same--] changed -. S = (/) to S =/= (/) 17-Apr-07 aceq4 [--same--] changed -. z = (/) to z =/= (/) 17-Apr-07 prn0 [--same--] changed -. A = (/) to A =/= (/) 15-Apr-07 elni [--same--] changed -. A = (/) to A =/= (/) 14-Apr-07 aceq3lem [--same--] changed -. z = (/) to z =/= (/) 14-Apr-07 aceq3 [--same--] changed -. z = (/) to z =/= (/) 13-Apr-07 tpnz [--same--] changed -. ... = (/) to =/= (/) 13-Apr-07 0nep0 [--same--] changed -. (/) = { (/) } to (/) =/= { (/) } 12-Apr-07 1cn ax1cn 12-Apr-07 ax1re 1re 11-Apr-07 zfreg [--same--] changed -. A = (/) to A =/= (/) 11-Apr-07 zfreg2 [--same--] changed -. A = (/) to A =/= (/) 11-Apr-07 inf1 [--same--] changed -. x = (/) to x =/= (/) 11-Apr-07 inf2 [--same--] changed -. x = (/) to x =/= (/) 11-Apr-07 zorn2lem6 [--same--] changed -. H = (/) to H =/= (/) 11-Apr-07 zorn2lem5 [--same--] changed -. H = (/) to H =/= (/) 11-Apr-07 zorn2lem3 [--same--] changed -. D = (/) to D =/= (/) 11-Apr-07 zorn2lem2 [--same--] changed -. D = (/) to D =/= (/) 11-Apr-07 zorn2lem1 [--same--] changed -. D = (/) to D =/= (/) 11-Apr-07 inf3lem2 [--same--] changed -. ... = to =/= 11-Apr-07 inf3lem3 [--same--] changed -. ... = to =/= 11-Apr-07 inf3lem4 [--same--] changed -. -. x = (/) to x =/= (/) 11-Apr-07 inf3lem5 [--same--] changed -. -. x = (/) to x =/= (/) 11-Apr-07 inf3lem6 [--same--] changed -. -. x = (/) to x =/= (/) 11-Apr-07 inf3lem7 [--same--] changed -. -. x = (/) to x =/= (/) 11-Apr-07 inf3 [--same--] changed -. -. x = (/) to x =/= (/) 10-Apr-07 htalem [--same--] changed -. A = (/) to A =/= (/) 9-Apr-07 ac3 [--same--] changed -. z = (/) to z =/= (/) 9-Apr-07 rnxp [--same--] changed -. A = (/) to A =/= (/) 7-Apr-07 aceq2 [--same--] changed -. z = (/) to z =/= (/) 6-Apr-07 tz6.12i [--same--] changed -. B = (/) to B =/= (/) 6-Apr-07 scott0s [--same--] changed -. .. = (/) to =/= { (/) } 6-Apr-07 dmxp [--same--] changed -. A = (/) to A =/= (/) 6-Apr-07 nnsuc [--same--] changed -. A = (/) to A =/= (/) 5-Apr-07 onne0 [--same--] changed -. On = (/) to On =/= (/) 5-Apr-07 ord0eln0 [--same--] changed -. A = (/) to A =/= (/) 5-Apr-07 wereu [--same--] -. B = (/) to B =/= (/); triple conjunction 3-Apr-07 aceq5lem5 [--same--] changed -. u = (/) to u =/= (/) 3-Apr-07 aceq5lem4 [--same--] changed -. u = (/) to u =/= (/) 3-Apr-07 aceq5lem3 [--same--] changed -. u = (/) to u =/= (/) 3-Apr-07 aceq5lem2 [--same--] changed -. u = (/) to u =/= (/) 3-Apr-07 pssdifn0 [--same--] changed -. ... = to =/= 3-Apr-07 fri [--same--] changed -. ... = (/) to ... =/= (/) 2-Apr-07 cplem1 [--same--] changed -. ... = (/) to =/= (/) 2-Apr-07 cplem2 [--same--] changed -. ... = (/) to =/= (/) 2-Apr-07 0pss [--same--] changed -. A = (/) to A =/= (/) 2-Apr-07 inelcm [--same--] changed -. ... = (/) to =/= (/) 2-Apr-07 snnz [--same--] changed -. A = (/) to A =/= (/) 2-Apr-07 inf0 [--same--] changed conclusion to match ax-inf exactly 2-Apr-07 n0f --- obsolete; use ne0f 26-Mar-07 df-lim [--same--] changed -. A = (/) to A =/= (/) 26-Mar-07 pwen [--same--] eliminated redundant hypotheses 26-Mar-07 ssundif undif 23-Mar-07 fo2 dffo2 23-Mar-07 fofv dffo3 22-Mar-07 fnbr [--same--] eliminated redundant hypotheses 22-Mar-07 fnop [--same--] eliminated redundant hypotheses 21-Mar-07 kardex [--same--] eliminated redundant hypothesis 21-Mar-07 qsid [--same--] eliminated redundant hypothesis 21-Mar-07 0nelqs [--same--] eliminated redundant hypothesis 21-Mar-07 brecop2 [--same--] eliminated redundant hypothesis 21-Mar-07 ecelqsdm [--same--] eliminated redundant hypothesis 18-Mar-07 map0b [--same--] changed -. A = (/) to A =/= (/) 17-Mar-07 oninton [--same--] changed -. A = (/) to A =/= (/) 17-Mar-07 wefrc [--same--] -. B = (/) to B =/= (/); triple conjunction 17-Mar-07 onint [--same--] changed -. A = (/) to A =/= (/) 17-Mar-07 tz7.5 [--same--] -. B = (/) to B =/= (/); triple conjunction 17-Mar-07 fiint [--same--] changed -. x = (/) to x =/= (/) 16-Mar-07 ishlg [--same--] changed hypothesis from X = dom N to X = ran G 16-Mar-07 unitopt --- obsolete; use topopn 16-Mar-07 peano3nn0 nn0p1nnt 15-Mar-07 intex [--same--] changed -. A = (/) to A =/= (/) 4-Mar-07 opthreg [--same--] added converse: -> to <-> 15-Feb-07 qbtwnre [--same--] antecedent changed to use triple conjunction 13-Feb-07 rcla42ev [--same--] antecedent changed to use triple conjunction 10-Feb-07 fodomb [--same--] changed -. A = (/) to A =/= (/) 7-Feb-07 rabbidv [--same--] conjoined antecedents in hypothesis 5-Feb-07 equidALT equid1 5-Feb-07 ax-11 ax-11o 2-Feb-07 ax11a ax11v 1-Feb-07 frc [--same--] -. = (/) to =/= (/); conjoined antecedents 31-Jan-07 itimesi ixi 31-Jan-07 isqm1 i2 30-Jan-07 dffr2 [--same--] changed -. ... = (/) to ... =/= (/) 30-Jan-07 df-fr [--same--] changed -. ... = (/) to ... =/= (/) 30-Jan-07 f1oeng [--same--] conjoined antecedents 29-Jan-07 2sumeq2d --- obsolete; use 2sumeq2dv 29-Jan-07 sumeq12d --- obsolete; use sumeq12dv 29-Jan-07 sumeq12rd --- obsolete; use sumeq12rdv 29-Jan-07 eval [--same--] ( 1 ^ k ) changed to 1 22-Jan-07 ax11el [--same--] generalized with less restrictive variables 18-Jan-07 climcvgc1 --- obsolete; use clmi1 18-Jan-07 climcvg1 --- obsolete; use clmi2 18-Jan-07 clim1 --- obsolete; use clm2 18-Jan-07 clim1a --- obsolete; use clm3 18-Jan-07 clim2a --- obsolete; use clm2 18-Jan-07 clim2 --- obsolete; use clm4 18-Jan-07 climcvg2 --- obsolete; use clmi2 18-Jan-07 climcvg2z --- obsolete; use clmi2 18-Jan-07 climcvgc2z --- obsolete; use clmi1 18-Jan-07 climcvg2zb --- obsolete; use clmi2 18-Jan-07 clim2az --- obsolete; use clm3 18-Jan-07 clim3az --- obsolete; use clm3 18-Jan-07 clim3a --- obsolete; use clm3 18-Jan-07 clim3 --- obsolete; use clm4 18-Jan-07 clim3b --- obsolete; use clm2 18-Jan-07 climcvg3 --- obsolete; use clmi2 18-Jan-07 climcvg3z --- obsolete; use clmi2 18-Jan-07 clim4a --- obsolete; use clm3 18-Jan-07 clim4 --- obsolete; use clm4 18-Jan-07 climcvg4 --- obsolete; use clmi2 18-Jan-07 climcvgc4z --- obsolete; use clmi1 18-Jan-07 climcvg4z --- obsolete; use clmi2 18-Jan-07 clim0cvg4z --- obsolete; use clm0i 18-Jan-07 climcvgc5z --- obsolete; use clmi1 18-Jan-07 climcvg5z --- obsolete; use clmi2 18-Jan-07 clim0cvg5z --- obsolete; use clm0i 18-Jan-07 climnn0 --- obsolete; use clm4 18-Jan-07 climnn --- obsolete; use clm4 18-Jan-07 clim0nn --- obsolete; use clm0 18-Jan-07 climcvgnn --- obsolete; use clmi2 18-Jan-07 climcvgnn0 --- obsolete; use clmi2 18-Jan-07 clim0cvgnn0 --- obsolete; use clm0i 18-Jan-07 climcvg2nn0 --- obsolete; use clmi2 18-Jan-07 clim0cvg2nn0 --- obsolete; use clm0i 18-Jan-07 climnn0le --- obsolete; use clm4le 18-Jan-07 clim0nn0le --- obsolete; use clm4le and clm0 16-Jan-07 abn0 [--same--] changed -. ... = (/) to ... =/= (/) 16-Jan-07 rabn0 [--same--] changed -. ... = (/) to ... =/= (/) 16-Jan-07 nsuceq0 [--same--] changed -. ... = (/) to ... =/= (/) 16-Jan-07 iin0 [--same--] changed -. A = (/) to A =/= (/) 16-Jan-07 fint [--same--] changed -. B = (/) to B =/= (/) 14-Jan-07 clim3z clm4at 12-Jan-07 climconst [--same--] made M e. ZZ a hypothesis instead of antecedent 11-Jan-07 climres2 --- obsolete; use climres 4-Jan-07 iunconst [--same--] changed -. A = (/) to A =/= (/) 21-Dec-06 intssuni2 [--same--] changed -. A = (/) to A =/= (/) 21-Dec-06 intssuni [--same--] changed -. A = (/) to A =/= (/) 21-Dec-06 prer2 preqr2 20-Dec-06 ccms cnms 20-Dec-06 ccims cnims 20-Dec-06 ccmsval cnimsval 18-Dec-06 cvgannn --- obsolete; use cvganuz 18-Dec-06 cvgannn0 --- obsolete; use cvganuz 14-Dec-06 cleqreli eqrelriv 14-Dec-06 cleqrel eqrel 12-Dec-06 rnco rncoss 12-Dec-06 dmco dmcoss 5-Dec-06 r19.2z [--same--] -. A = (/) to A =/= (/); conjoined antecendents 24-Nov-06 infn0 [--same--] changed -. A = (/) to A =/= (/) 24-Nov-06 0sdom [--same--] changed -. A = (/) to A =/= (/) 24-Nov-06 0sdomg [--same--] changed -. A = (/) to A =/= (/) 24-Nov-06 infxpabs [--same--] -. B = (/) to B =/= (/); use w3a for antec. 24-Nov-06 xpdom3 [--same--] changed antecedent from -. B = (/) to B =/= (/) 14-Nov-06 zfnul axnul 14-Nov-06 zfaus axsep 28-Oct-06 inv inv1 25-Oct-06 orcana --- obsolete; use pm5.6 10-Oct-06 oprec [--same--] changed order of $f hypotheses 10-Oct-06 ecoprdi [--same--] changed order of $f hypotheses 10-Oct-06 ecoprass [--same--] changed order of $f hypotheses 9-Oct-06 unisseq --- obsolete; use unimax 8-Oct-06 notzfaus [--same--] more meaningful first hypothesis 8-Oct-06 intmin [--same--] swapped arguments of = sign 8-Oct-06 intmin2 [--same--] swapped arguments of = sign 5-Oct-06 expcant [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 expsubt [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 divexpt [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 expwordit [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 explt1t [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 recexpt [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 expordt [--same--] generalized antecedent from e. NN to e. NN0 5-Oct-06 iineq2dv [--same--] conjoined antecedents in hypothesis 5-Oct-06 iuneq2dv [--same--] conjoined antecedents in hypothesis 5-Oct-06 r19.9rzv [--same--] changed antecedent from -. A = (/) to A =/= (/) 5-Oct-06 r19.45zv [--same--] changed antecedent from -. A = (/) to A =/= (/) 5-Oct-06 r19.27zv [--same--] changed antecedent from -. A = (/) to A =/= (/) 5-Oct-06 r19.36zv [--same--] changed antecedent from -. A = (/) to A =/= (/) 5-Oct-06 iindif2 [--same--] changed antecedent from -. A = (/) to A =/= (/) 5-Oct-06 r19.28zv [--same--] changed antecedent from -. A = (/) to A =/= (/) 5-Oct-06 r19.3rzv [--same--] changed antecedent from -. A = (/) to A =/= (/) 2-Oct-06 phplem5 phplem4 2-Oct-06 phplem4 phplem3 2-Oct-06 phplem3 phplem2 2-Oct-06 phplem2 phplem1 2-Oct-06 phplem1 --- obsolete; use difsnid 29-Sep-06 uniord orduni 29-Sep-06 onunit ssonuni 29-Sep-06 onuni ssonunii 29-Sep-06 ac6s2 ac6s3 29-Sep-06 ac6c --- obsolete; use ac6s5 21-Sep-06 rankuni rankuni2 20-Sep-06 npnz [--same--] strengthened by adding converse 20-Sep-06 onsucuni2 [--same--] swapped arguments of = sign 19-Sep-06 nlimsuc --- obsolete; use nlimsucg 19-Sep-06 limuni2 limuni3 15-Sep-06 ranklon rankval4 13-Sep-06 cbvop rexxp 11-Sep-06 zfaus zfauscl 10-Sep-06 fex [--same--] antecedent changed to use conjunction & swapped 10-Sep-06 f1dmex [--same--] antecedent changed to use conjunction & swapped 10-Sep-06 fnex [--same--] antecedent changed to use conjunction & swapped 10-Sep-06 ssexg [--same--] antecedent changed to use conjunction & swapped 10-Sep-06 funimaexg [--same--] antecedent changed to use conjunction & swapped 10-Sep-06 resfunexg [--same--] antecedent changed to use conjunction & swapped 9-Sep-06 funex [--same--] antecedent changed to use conjunction & swapped 8-Sep-06 cls clsp 29-Aug-06 elab3g elab3 26-Aug-06 unop uniop 26-Aug-06 unpr unipr 26-Aug-06 unictb [--same--] removed irrelevant hypothesis 16-Aug-06 ssrab ssrab2 16-Aug-06 rabss rabss2 16-Aug-06 ssab ssab2 13-Aug-06 fvco3 [--same--] antecedent changed to use triple conjunction 13-Aug-06 fvco2 [--same--] antecedent changed to use triple conjunction 6-Jun-06 sq0 sq00 1-Jun-06 infpn infpn2 27-May-06 --- --- exp was changed to ex to prevent matching 27-May-06 --- --- math token 'exp'. 27-May-06 exp ex 26-May-06 f1ocnvfvb [--same--] antecedent changed to use triple conjunction 22-Apr-06 fvco [--same--] antecedent changed to use triple conjunction 10-Apr-06 plus1let p1let 10-Apr-06 leplus1t lep1t 10-Apr-06 ltplus1 ltp1 10-Apr-06 ltplus1t ltp1t 29-Mar-06 xpdom2 [--same--] eliminated the A e. V hypothesis 29-Mar-06 xpdom1 [--same--] eliminated the A e. V hypothesis 28-Mar-06 sspr [--same--] eliminated both $e hypotheses 26-Mar-06 fnfvop fnopfvb 26-Mar-06 fnfvbr fnbrfvb 26-Mar-06 eqri eqriv 26-Mar-06 eqrd eqrdv 26-Mar-06 nn0z nn0zrab 26-Mar-06 nnz nnzrab 24-Mar-06 fodomb [--same--] eliminated the B e. V hypothesis 24-Mar-06 eldmg eldm2g 22-Mar-06 prprc prprc1 22-Mar-06 sqrsqet sqrsqt 22-Mar-06 sqrsqe sqrsq 22-Mar-06 sqrsq sqrmsq2 21-Mar-06 nn0le2sqet nn0le2msqt 21-Mar-06 le2sqet le2sqt 21-Mar-06 le2sqt le2msqt 21-Mar-06 lt2sqet lt2sqt 21-Mar-06 lt2sqt lt2msqt 21-Mar-06 le2sqe le2sq 21-Mar-06 le2sq le2msq 21-Mar-06 lt2sqe lt2sq 21-Mar-06 lt2sq lt2msq 21-Mar-06 ltsqt ltmsqt 13-Mar-06 sq11t [--same--] rearranged antecedent 11-Mar-06 sqrecl resqcl 11-Mar-06 sqreclt resqclt 11-Mar-06 --- --- 'sq' is normal square (A ^ 2) 11-Mar-06 sqe0 sqeq0 11-Mar-06 sqe11 sq11 11-Mar-06 sqegt0 sqgt0 11-Mar-06 sqege0 sqge0 11-Mar-06 sqe11t sq11t 11-Mar-06 sqege0t sqge0t 11-Mar-06 --- --- 'msq' is square represented by mult. (A x. A) 11-Mar-06 sqeq0 msq0 11-Mar-06 sqgt0 msqgt0 11-Mar-06 sqge0 msqge0 11-Mar-06 sq11 msq11 11-Mar-06 sqznn msqznn 11-Mar-06 sqrsqid sqrmsq 11-Mar-06 sqeq0 msq0 24-Feb-06 lerect [--same--] rearranged antecedent 24-Feb-06 ltrect [--same--] rearranged antecedent 24-Feb-06 lt2sqet [--same--] rearranged antecedent 24-Feb-06 le2sqet [--same--] rearranged antecedent 24-Feb-06 lt2sqt [--same--] rearranged antecedent 24-Feb-06 le2sqt [--same--] rearranged antecedent 20-Feb-06 funfvopi funopfv 20-Feb-06 funopfv funfvop 20-Feb-06 funfvop funopfvb 9-Feb-06 divneq0bt divne0bt 9-Feb-06 divneq0 divne0 9-Feb-06 recneq0z recne0z 9-Feb-06 pm2.61an2 pm2.61dan 9-Feb-06 pm2.61an1 pm2.61ian 28-Jan-06 cleqfvf eqfnfvf 26-Jan-06 fri [--same--] changed to closed theorem instead of inference 17-Jan-06 relin relin1 17-Jan-06 ssrelqqq relss 17-Jan-06 relss ssrel 17-Jan-06 ssrel ssrelqqq 16-Jan-06 elrnqqq elrn2 16-Jan-06 elrn2 elrn 16-Jan-06 elrn elrnqqq 12-Jan-06 df-ef [--same--] revised to use new df-sum 9-Jan-06 rabeqbi2i rabeq2i 9-Jan-06 abeqbi2 abeq2 9-Jan-06 abeqbi1 abeq1 9-Jan-06 abeqbi2i abeq2i 9-Jan-06 abeqbi1i abeq1i 9-Jan-06 abeqbi2d abeq2d 9-Jan-06 abbieq2i abbi2i 9-Jan-06 abbieqi abbii 9-Jan-06 abbieqd abbid 9-Jan-06 abbieqdv abbidv 9-Jan-06 abbieq2dv abbi2dv 9-Jan-06 abbieq1dv abbi1dv 9-Jan-06 rabbieqi rabbii 9-Jan-06 rabbieqdv rabbidv 9-Jan-06 rabbieqsdv rabbisdv 9-Jan-06 rabbieqrdv rabbirdv 9-Jan-06 opabbieqd opabbid 9-Jan-06 opabbieqdv opabbidv 9-Jan-06 oprabbieqd oprabbid 9-Jan-06 oprabbieqdv oprabbidv 9-Jan-06 oprabbieqi oprabbii 9-Jan-06 abeqbi2 abeq2 9-Jan-06 abeqbi2i abeq2i 9-Jan-06 abeqbi1 abeq1 9-Jan-06 abeqbi2d abeq2d 9-Jan-06 abeqbi1i abeq1i 9-Jan-06 rabeqbi2i rabeq2i 9-Jan-06 oprabbieqi oprabbii 7-Jan-06 divgt0lem divgt0i2 5-Jan-06 lep1t letrp1t 4-Jan-06 nnegdift --- obsolete; use subge0t (swapped biconditional) 2-Jan-06 opabbii.2 opabbii 1-Jan-06 negdi2 negsubdi 1-Jan-06 negdi2t negsubdit 1-Jan-06 negdi3 negsubdi2t 1-Jan-06 negdi3t negsubdi2t 17-Dec-05 msca --- obsolete; now embedded inside equs4 proof 16-Dec-05 1expt [--same--] antecedent extended from NN to NN0 16-Dec-05 nnexpclt [--same--] antecedent extended from NN to NN0 16-Dec-05 nn0expclt [--same--] antecedent extended from NN to NN0 16-Dec-05 zexpclt [--same--] antecedent extended from NN to NN0 16-Dec-05 qexpclt [--same--] antecedent extended from NN to NN0 16-Dec-05 reexpclt [--same--] antecedent extended from NN to NN0 16-Dec-05 expclt [--same--] antecedent extended from NN to NN0 16-Dec-05 expcllem [--same--] antecedent extended from NN to NN0; + 3rd hyp. 16-Dec-05 expp1t [--same--] antecedent extended from NN to NN0 16-Dec-05 expvalt expnnvalt 13-Dec-05 sbcco sbccog 1-Dec-05 subneg2t subnegt 1-Dec-05 subnegt --- obsolete; use negsubt (swapped equality) 1-Dec-05 subneg --- obsolete; use negsub (swapped equality) 1-Dec-05 reueq reueq1 1-Dec-05 rexeq rexeq1 1-Dec-05 raleq raleq1 1-Dec-05 reueqf reueq1f 1-Dec-05 rexeqf rexeq1f 1-Dec-05 raleqf raleq1f 1-Dec-05 ad2antxx ad2antrr 1-Dec-05 ad2antrr ad2antll 1-Dec-05 ad2antll ad2antxx 29-Nov-05 sbcel2 sbcel2gv 29-Nov-05 sbcel1 sbcel1gv 28-Nov-05 sbcn sbcng 28-Nov-05 sbcim sbcimg 28-Nov-05 sbcbi sbcbidig 28-Nov-05 sbcor sbcorg 28-Nov-05 sbcan sbcang 28-Nov-05 sbcal sbcalg 28-Nov-05 sbcex sbcexg 28-Nov-05 sbceq1 sbceq1a 21-Nov-05 2o 2on 21-Nov-05 1o 1on 19-Nov-05 zfrep3 axrep5 19-Nov-05 zfrep2 axrep4 19-Nov-05 axrep axrep2 18-Nov-05 hbsbcg hbsbc1g 18-Nov-05 hbsbc hbsbc1 18-Nov-05 hbsbcv hbsbc1v 18-Nov-05 --- --- More changes to the bixx series below - 18-Nov-05 --- --- changed to xxbix to be analogous to the xxeqx 18-Nov-05 --- --- series e.g. uneq12d. Also, the bi(r)abxx were 18-Nov-05 --- --- changed to (r)abbieqxx: "bi" in hyp. and 18-Nov-05 --- --- "eq" in conclusion. 18-Nov-05 bial albii 18-Nov-05 bi2al 2albii 18-Nov-05 biex exbii 18-Nov-05 bi2ex 2exbii 18-Nov-05 bi3ex 3exbi 18-Nov-05 biald albid 18-Nov-05 biexd exbid 18-Nov-05 bisb sbbii 18-Nov-05 bisbd sbbid 18-Nov-05 bialdv albidv 18-Nov-05 biexdv exbidv 18-Nov-05 bi2aldv 2albidv 18-Nov-05 bi2exdv 2exbidv 18-Nov-05 bi3exdv 3exbidv 18-Nov-05 bi4exdv 4exbidv 18-Nov-05 bieud eubid 18-Nov-05 bieudv eubidv 18-Nov-05 bieu eubii 18-Nov-05 bimod mobid 18-Nov-05 bimo mobii 18-Nov-05 biralda ralbida 18-Nov-05 birexda rexbida 18-Nov-05 biraldva ralbidva 18-Nov-05 birexdva rexbidva 18-Nov-05 birald ralbid 18-Nov-05 birexd rexbid 18-Nov-05 biraldv ralbidv 18-Nov-05 birexdv rexbidv 18-Nov-05 biraldv2 ralbidv2 18-Nov-05 birexdv2 rexbidv2 18-Nov-05 biral ralbii 18-Nov-05 birex rexbii 18-Nov-05 bi2ral 2ralbii 18-Nov-05 bi2rex 2rexbii 18-Nov-05 biral2 ralbii2 18-Nov-05 birex2 rexbii2 18-Nov-05 birala ralbiia 18-Nov-05 birexa rexbiia 18-Nov-05 bi2rexa 2rexbiia 18-Nov-05 bi2ralda 2ralbida 18-Nov-05 bi2raldva 2ralbidva 18-Nov-05 bi2rexdva 2rexbidva 18-Nov-05 bireudva reubidva 18-Nov-05 bireudv reubidv 18-Nov-05 bireua reubiia 18-Nov-05 bireu reubii 18-Nov-05 bisbcdv sbcbidv 18-Nov-05 bisbc sbcbii 18-Nov-05 eqrabi rabeqbi2i 18-Nov-05 eqab abeqbi2 18-Nov-05 eqabr abeqbi1 18-Nov-05 eqabi abeqbi2i 18-Nov-05 eqabri abeqbi1i 18-Nov-05 eqabd abeqbi2d 18-Nov-05 biabri abbieq2i 18-Nov-05 biabi abbieqi 18-Nov-05 biabd abbieqd 18-Nov-05 biabdv abbieqdv 18-Nov-05 biabrdv abbieq2dv 18-Nov-05 biabldv abbieq1dv 18-Nov-05 birabi rabbieqi 18-Nov-05 birabdv rabbieqdv 18-Nov-05 birabsdv rabbieqsdv 18-Nov-05 birabrdv rabbieqrdv 18-Nov-05 biopabd opabbieqd 18-Nov-05 biopabdv opabbieqdv 18-Nov-05 bioprabd oprabbieqd 18-Nov-05 bioprabdv oprabbieqdv 18-Nov-05 bioprabi oprabbieqi 18-Nov-05 bicon1i con1bii 18-Nov-05 bicon2i con2bii 18-Nov-05 bicon4i con4bii 18-Nov-05 bicon4d con4bid 18-Nov-05 bicon2 con2bi 18-Nov-05 bicon2d con2bid 18-Nov-05 bicon1d con1bid 18-Nov-05 bisyl7 syl7ib 18-Nov-05 bisyl8 syl8ib 11-Nov-05 sbcbidv [--same--] swapped antecedents 21-Oct-05 ciin [--same--] "|^|" changed to "|^|_" 21-Oct-05 cuin [--same--] "U." changed to "U_" 21-Oct-05 ---SYMBOL CHANGE---- Changed "|^|" to "|^|_" in thm's using ciin 21-Oct-05 ---SYMBOL CHANGE---- Changed "U." to "U_" in thm's using ciun 20-Oct-05 rax5 ra5 20-Oct-05 rax4 --- obsolete; use ra4sbc 20-Oct-05 reuuni2f [--same--] weakened its hypotheses 19-Oct-05 reuss [--same--] antecedent changed to use triple conjunction 10-Oct-05 uzwo [--same--] changed to use ZZ>= notation 10-Oct-05 uzwo2 [--same--] changed to use ZZ>= notation 1-Oct-05 nnncant nnncan1t 13-Sep-05 leltnet [--same--] antecedent changed to use triple conjunction 10-Sep-05 ifel ifcl 6-Sep-05 dmopab2 dmopab3 5-Sep-05 peano2uz peano2uz2 1-Sep-05 cleqfv eqfnfv 1-Sep-05 df-seq df-seq1 1-Sep-05 cseqz cseq1 1-Sep-05 serft ser1ft 1-Sep-05 serf ser1f 1-Sep-05 sercl ser1cl 1-Sep-05 serrecl ser1recl 1-Sep-05 serre ser1re 1-Sep-05 sercl2 ser1cl2 1-Sep-05 serf2 ser1f2 1-Sep-05 ser12 ser11 1-Sep-05 sersuc2 ser1p1 1-Sep-05 sermono ser1mono 1-Sep-05 seradd2 ser1add2 1-Sep-05 seradd ser1add 1-Sep-05 serdir ser1dir 1-Sep-05 serabsdiflem ser1absdiflem 1-Sep-05 serabsdif ser1absdif 1-Sep-05 serre2 ser1re2 1-Sep-05 sercj ser1cj 1-Sep-05 serconst ser1const 1-Sep-05 sertrunclem ser1trunclem 1-Sep-05 sercmp ser1cmp 1-Sep-05 sercmp0 ser1cmp0 1-Sep-05 sercmp2lem ser1cmp2lem 1-Sep-05 sercmp2 ser1cmp2 1-Sep-05 seqlem1 seq1lem1 1-Sep-05 seqlem2 seq1lem2 1-Sep-05 seqrval seq1rval 1-Sep-05 seqval seq1val 1-Sep-05 seqfnlem seq1fnlem 1-Sep-05 seqval2 seq1val2 1-Sep-05 seq1lem seq11lem 1-Sep-05 seqsuclem seq1suclem 1-Sep-05 seqp1 seq1p1 1-Sep-05 seqm1 seq1m1 1-Sep-05 seqfn seq1fn 1-Sep-05 seqrn seq1rn2 1-Sep-05 seqrn2 seq1rn 1-Sep-05 seqcl seq1cl 1-Sep-05 seqres seq1res 1-Sep-05 seqbnd seq1bnd 1-Sep-05 sequblem seq1ublem 1-Sep-05 sequb seq1ub 1-Sep-05 seqhcau seq1hcau 1-Sep-05 ---SYMBOL CHANGE---- Changed math symbol 'seq' to 'seq1' 1-Sep-05 seq1 seq11 Warning: change _before_ symbol change above 17-Aug-05 df-clim [--same--] The old df-clim, df-shft, and df-seq0, and 17-Aug-05 df-shft [--same--] all derived theorems, have been scrapped 17-Aug-05 df-seq0 [--same--] or rederived from the new definitions. 30-Jul-05 --- --- syl* changes below were sugg'ed by Scott Fenton 30-Jul-05 syl34d imim12d 30-Jul-05 syl4d imim1d 30-Jul-05 syl3d imim2d 30-Jul-05 syl34 imim112i 30-Jul-05 syl4 imim1i 30-Jul-05 syl3 imim2i 30-Jul-05 syl2 imim1 30-Jul-05 syl1 imim2 27-Jul-05 uzind [--same--] weaker basis hyp.; different mand. hyp. order 13-Jul-05 mp3an11 mp3anl1 13-Jul-05 mp3an12 mp3anl2 13-Jul-05 mp3an13 mp3anl3 13-Jul-05 syl3an11 syl3anl1 13-Jul-05 syl3an12 syl3anl2 13-Jul-05 syl3an13 syl3anl3 13-Jul-05 mpan11 mpanl1 13-Jul-05 mpan12 mpanl2 13-Jul-05 mpan21 mpanr1 13-Jul-05 mpan22 mpanr2 13-Jul-05 sylan11 sylanl1 13-Jul-05 sylan12 sylanl2 13-Jul-05 sylan21 sylanr1 13-Jul-05 sylan22 sylanr2 13-Jul-05 mpan121 mpanlr1 13-Jul-05 ecased --- obsolete; use ecase23d (diff. hyp. order) 11-Jul-05 lelt lenlt 11-Jul-05 leltt lenltt 11-Jul-05 lenltt eqleltt 10-Jul-05 bcpasc bcpasc2 10-Jul-05 bcvalt bcval2t 9-Jul-05 sermconst --- obsolete; use ser1mulc 9-Jul-05 seqsuc seq1p1 3-Jul-05 peano5c --- obsolete; use peano5nn (restr. qntfr.) 3-Jul-05 df-n [--same--] shortened with restricted quantifier 2-Jul-05 mulge0t [--same--] conjoined antecedents 2-Jul-05 prodgt02t [--same--] swapped A e. RR and B e. RR 27-Jun-05 syl3an [--same--] changed order of hypotheses 25-Jun-05 ecoprcom [--same--] changed order of $f hypotheses 21-Jun-05 nn0ltlem1 nn0ltlem1t 21-Jun-05 subsub subsub23 17-Jun-05 ecoprdist --- obsolete; use ecoprdi 16-Jun-05 binom binom2 12-Jun-05 oel orabs 30-May-05 ltdiv23t [--same--] conjoined antecedents 30-May-05 ledivt lediv1t 23-May-05 rcla42v [--same--] swapped antecedents 23-May-05 rcla4v [--same--] swapped antecedents 23-May-05 rcla4 [--same--] swapped antecedents 10-May-05 mpbiranr mpbiran2 8-May-05 funfv2 [--same--] changed to A F y instead of <. A , y >. e. F 8-May-05 imasn --- obsolete; use relimasn (A R y instead of o.p.) 3-May-05 nndiv nndivt 2-May-05 subaddeq pncan3 2-May-05 subaddeqt pncan3t 1-May-05 divne0bt [--same--] changed antecedent to triple conjunction 1-May-05 divcan2t [--same--] changed antecedent to triple conjunction 1-May-05 divcan1t [--same--] changed antecedent to triple conjunction 30-Apr-05 divnegt [--same--] changed antecedent to triple conjunction 30-Apr-05 divrect [--same--] changed antecedent to triple conjunction 30-Apr-05 divcan3t [--same--] changed antecedent to triple conjunction 30-Apr-05 divcan4t [--same--] changed antecedent to triple conjunction 29-Apr-05 crut [--same--] generalized -> to <-> 29-Apr-05 cru [--same--] generalized -> to <-> 29-Apr-05 isqm1 itimesi 29-Apr-05 crmult crmul changed hypotheses from real to complex 29-Apr-05 redivclt [--same--] changed antecedent to triple conjunction 29-Apr-05 divclt [--same--] changed antecedent to triple conjunction 28-Apr-05 ine0 [--same--] changed -. and = to =/= 27-Apr-05 ltdivt ltdiv1t 27-Apr-05 ltdiv ltdiv1 27-Apr-05 ltdivi ltdiv1i 24-Apr-05 prodgt0 [--same--] strengthened 0 < A to 0 <_ A 24-Apr-05 prodgt0i prodgt0lem 7-Apr-05 equs2 --- obsolete; use equs5 7-Apr-05 equs1 --- obsolete; use equs4 6-Apr-05 absltt [--same--] swapped & contraposed conjunct with -u 6-Apr-05 absle [--same--] swapped & contraposed conjunct with -u 6-Apr-05 abslt [--same--] swapped & contraposed conjunct with -u 26-Mar-05 abscj [--same--] swapped arguments of = sign 18-Mar-05 reim0 reim0b 18-Mar-05 rere rereb 18-Mar-05 cjre cjreb 18-Mar-05 negre negreb 11-Mar-05 frsuc frsuc 10-Mar-05 nn0addge2 [--same--] Generalized 1st hyp from NN0 to RR 10-Mar-05 nn0addge1 [--same--] Generalized 1st hyp from NN0 to RR 5-Mar-05 chv chvarv 5-Mar-05 chv2 chvar 4-Mar-05 divdistr divdir 4-Mar-05 divdistrz divdirz 4-Mar-05 divge0t [--same--] conjoined the two left-most antecedents 4-Mar-05 divgt0t [--same--] conjoined the two left-most antecedents 4-Mar-05 absgt0t [--same--] changed -. A = 0 to A =/= 0 4-Mar-05 absgt0 [--same--] changed -. A = 0 to A =/= 0 24-Feb-05 absidt [--same--] conjoined the two left-most antecedents 27-Feb-05 del34 --- obsolete; use dral1 instead 27-Feb-05 del35 --- obsolete; use dral1 instead 27-Feb-05 del34b dral1 27-Feb-05 del36 --- obsolete; use dral2 instead 27-Feb-05 del40 --- obsolete; use drex1 instead 27-Feb-05 del41 --- obsolete; use drex1 instead 27-Feb-05 del42 --- obsolete; use drex2 instead 27-Feb-05 del43 --- obsolete; use drsb1 instead 27-Feb-05 del43b drsb1 27-Feb-05 del44 --- obsolete; use drsb2 instead 27-Feb-05 del45 --- obsolete; use drsb2 instead 27-Feb-05 ddelimf2 dvelimf2 27-Feb-05 ddelimf dvelimf 27-Feb-05 ddelimdf dvelimdf 27-Feb-05 ddelim dvelim 27-Feb-05 ddeeq1 dveeq1 27-Feb-05 ddeeq2 dveeq2 27-Feb-05 ddeel1 dveel1 27-Feb-05 ddeel2 dveel2 24-Feb-05 bi3ord 3orbi123d 24-Feb-05 im3ord 3orim123d 24-Feb-05 bi3or 3orbi123i 24-Feb-05 bi3an 3anbi123i 24-Feb-05 bi3and 3anbi123d 24-Feb-05 im3an 3anim123i 24-Feb-05 divdistrt divdirt 24-Feb-05 ltdiv1t [--same--] conjoined the two left-most antecedents 24-Feb-05 lediv1t [--same--] conjoined the two left-most antecedents 24-Feb-05 ltmuldivt [--same--] conjoined the two left-most antecedents 24-Feb-05 ltdivmult [--same--] conjoined the two left-most antecedents 24-Feb-05 ltmuldiv2t [--same--] conjoined the two left-most antecedents 24-Feb-05 gt0ne0t [--same--] conjoined the two left-most antecedents 24-Feb-05 ltrect [--same--] conjoined the two left-most antecedents 24-Feb-05 recgt0t [--same--] conjoined the two left-most antecedents 24-Feb-05 lerect [--same--] conjoined the two left-most antecedents 21-Feb-05 nn0ge0i nn0ge0 21-Feb-05 rdgzer rdg0 21-Feb-05 rdgzert rdg0g 21-Feb-05 frzer fr0g 21-Feb-05 mulzer1 mul01 21-Feb-05 mulzer2 mul02 21-Feb-05 mulzer1t mul01t 21-Feb-05 mulzer2t mul02t 21-Feb-05 divzer div0 19-Feb-05 ax0re 0re 13-Feb-05 cardcard cardidm 13-Feb-05 exp2t sqvalt 13-Feb-05 uzind2 --- Obsolete; use uzind3 5-Feb-05 --- --- We will adopt "equ" (vs. old "eq") for 5-Feb-05 --- --- set variable equality and "eq" (vs. old 5-Feb-05 --- --- "cleq") for class equality. (Remember it 5-Feb-05 --- --- is important to do these in REVERSE order 5-Feb-05 --- --- below!) 5-Feb-05 cleqri eqri 5-Feb-05 cleqrd eqrd 5-Feb-05 cleqid eqid 5-Feb-05 cleqcom eqcom 5-Feb-05 cleqcomi eqcomi 5-Feb-05 cleqcomd eqcomd 5-Feb-05 cleq1 eqeq1 5-Feb-05 cleq2 eqeq2 5-Feb-05 cleq1i eqeq1i 5-Feb-05 cleq2i eqeq2i 5-Feb-05 cleq1d eqeq1d 5-Feb-05 cleq2d eqeq2d 5-Feb-05 cleq12 eqeq12 5-Feb-05 cleq12i eqeq12i 5-Feb-05 cleq12d eqeq12d 5-Feb-05 cleqan12d eqeqan12d 5-Feb-05 cleqan12rd eqeqan12rd 5-Feb-05 cleqtr eqtr 5-Feb-05 cleq2tr eq2tri 5-Feb-05 cleqab abeqbi2 5-Feb-05 cleqabi abeqbi2i 5-Feb-05 cleqabr abeqbi1 5-Feb-05 cleqabd abeqbi2d 5-Feb-05 cleqabri abeqbi1i 5-Feb-05 cleq2ab eq2ab 5-Feb-05 cleqrabi rabeqbi2i 5-Feb-05 clneq nelneq 5-Feb-05 clneq2 nelneq2 5-Feb-05 sbeq2 equsb2 5-Feb-05 sbeq1 equsb1 5-Feb-05 eqvin.l2 --- obsolete; use equvin instead 5-Feb-05 eqvin equvin 5-Feb-05 eqvin.l1 equvini 5-Feb-05 eqsal equsal 5-Feb-05 eqsex equsex 5-Feb-05 eqs5 equs5 5-Feb-05 eqs4 equs4 5-Feb-05 eqs3 equs3 5-Feb-05 eqs2 equs2 5-Feb-05 eqs1 equs1 5-Feb-05 eq6s hbnaes 5-Feb-05 eq6 hbnae 5-Feb-05 eq5s hbaes 5-Feb-05 eq5 hbae 5-Feb-05 eq4ds nalequcoms 5-Feb-05 eq4s alequcoms 5-Feb-05 eq4 ax-10 5-Feb-05 a14b elequ2 5-Feb-05 a13b elequ1 5-Feb-05 eqt2b equequ2 5-Feb-05 a8b equequ1 5-Feb-05 eqt equtr 5-Feb-05 eqt2 equtrr 5-Feb-05 eqan equtr2 5-Feb-05 eqcom equcomi 5-Feb-05 eqcomb equcom 5-Feb-05 eqcoms equcoms 5-Feb-05 eqid equid 3-Feb-05 sb5f1 sb6rf 21-Jan-05 mulcanxx mulcant2 21-Jan-05 mulcant2 mulcant 21-Jan-05 mulcant mulcanxx 10-Jan-05 add41r3 add42 10-Jan-05 caopr41r3 caopr42 10-Jan-05 an41r3s an42s 10-Jan-05 an41r3 an42 8-Jan-05 --- --- The imxx series was changed analogously 8-Jan-05 --- --- to the bixx series change. 8-Jan-05 im2an anim12i 8-Jan-05 imran anim1i 8-Jan-05 imlan anim2i 8-Jan-05 im2or orim12i 8-Jan-05 imror orim1i 8-Jan-05 imlor orim2i 8-Jan-05 im2and anim12d 8-Jan-05 imrand anim1d 8-Jan-05 imland anim2d 8-Jan-05 im2ord orim12d 8-Jan-05 imrord orim1d 8-Jan-05 imlord orim2d 8-Jan-05 --- --- The bixx series was changed to be analogous 8-Jan-05 --- --- to the xxeqx series e.g. uneq12d. 8-Jan-05 --- --- (Suggested by Raph Levien.) 8-Jan-05 bi2and anbi12d 8-Jan-05 birand anbi1d 8-Jan-05 biland anbi2d 8-Jan-05 bi2imd imbi12d 8-Jan-05 birimd imbi1d 8-Jan-05 bilimd imbi2d 8-Jan-05 bi2ord orbi12d 8-Jan-05 birord orbi1d 8-Jan-05 bilord orbi2d 8-Jan-05 bi2bid bibi12d 8-Jan-05 birbid bibi1d 8-Jan-05 bilbid bibi2d 8-Jan-05 binegd negbid 8-Jan-05 bi2an anbi12i 8-Jan-05 biran anbi1i 8-Jan-05 bilan anbi2i 8-Jan-05 bi2im imbi12i 8-Jan-05 birim imbi1i 8-Jan-05 bilim imbi2i 8-Jan-05 bi2or orbi12i 8-Jan-05 biror orbi1i 8-Jan-05 bilor orbi2i 8-Jan-05 bi2bi bibi12i 8-Jan-05 birbi bibi1i 8-Jan-05 bilbi bibi2i 8-Jan-05 bineg negbii 3-Jan-05 pm5.41 imdi 1-Jan-05 iundif iundif2 1-Jan-05 iindif iindif2 1-Jan-05 iunin iunin2 1-Jan-05 iinin iinin2 1-Jan-05 sylan13br sylancbr 1-Jan-05 sylan13b sylancb 1-Jan-05 sylan13 sylanc 1-Jan-05 syl13 sylc 26-Dec-04 0ne1o --- obsolete; use 1ne0 19-Dec-04 sbequ6 [--same--] swapped biconditional order 19-Dec-04 sbequ5 [--same--] swapped biconditional order 15-Dec-04 syl2and syl2ani 15-Dec-04 sylan2d sylan2i 15-Dec-04 syland sylani 12-Dec-04 nnordex nnaordex 12-Dec-04 nnwordex nnawordex 12-Dec-04 mpand mpdan 12-Dec-04 ontr ontr1 6-Dec-04 on0eqel on0eqelt 30-Nov-04 exp2 sqvalt 30-Nov-04 1exp 1expt 30-Nov-04 0exp 0expt 30-Nov-04 exp1 exp1t 30-Nov-04 expp1 expp1t 18-Nov-04 divrclz redivclz 18-Nov-04 divrclt redivclt 18-Nov-04 subrclt resubclt 18-Nov-04 negrclt renegclt 18-Nov-04 mulrclt remulclt 18-Nov-04 divrcl redivcl 18-Nov-04 subrcl resubcl 18-Nov-04 negrcl renegcl 18-Nov-04 mulrcl remulcl 18-Nov-04 addrcl readdcl 18-Nov-04 ltdivmul --- obsolete; use ltmuldiv instead 18-Nov-04 ltdivmult --- obsolete; use ltmuldivt instead (note: there is a new ltdivmult that is unrelated) 18-Nov-04 distr2t adddirt 18-Nov-04 distr2 adddir 18-Nov-04 distr adddi 18-Nov-04 subdistr subdir 17-Nov-04 nnrect nnrecgt0t 17-Nov-04 posdif [--same--] swapped biconditional and variable order 15-Nov-04 negdistt3 negdi3t 15-Nov-04 negdistt2 negdi2t 15-Nov-04 negdistt negdit 15-Nov-04 negdist3 negdi3 15-Nov-04 negdist2 negdi2 11-Nov-04 reuunis reuuni2 11-Nov-04 reuuni reuuni1 9-Nov-04 zlelt1 zleltp1t 9-Nov-04 zltle1 zltp1let 7-Sep-04 arch [--same--] removed quantifier, changed set var. to class 2-Nov-04 dfom2 dfom3 2-Nov-04 dfom3 dfom4 29-Oct-04 df-ded df-if 29-Oct-04 dedeq1 ifeq1 29-Oct-04 dedeq2 ifeq2 29-Oct-04 dedeq12 ifeq12 29-Oct-04 dedbi ifbi 29-Oct-04 dedlem1 iftrue 29-Oct-04 dedlem2 iffalse 29-Oct-04 dedex ifex 29-Oct-04 cded cif 29-Oct-04 ---SYMBOL CHANGE---- Changed math symbol 'ded' to 'if' 28-Oct-04 cmulc cmul 20-Oct-04 oprabex oprabex2 14-Oct-04 nn0lelt1 nn0leltp1t 14-Oct-04 nn0ltle1 nn0ltp1let 14-Oct-04 nnlelt1 nnleltp1t 14-Oct-04 nnltle1 nnltp1let 14-Oct-04 rnoel3 rabn0 14-Oct-04 noel3 abn0 14-Oct-04 noel2 n0i 14-Oct-04 peano2c peano2nn 12-Oct-04 supeu supeui 12-Oct-04 supcl supcli 12-Oct-04 supub supubi 12-Oct-04 suplub suplubi 12-Oct-04 supnub supnubi 12-Oct-04 suprcl suprcli 12-Oct-04 suprub suprubi 12-Oct-04 pm4.12 con2bi 12-Oct-04 bicon4 con4bii 12-Oct-04 con2bi con2bii 12-Oct-04 bicon1 con1bii 12-Oct-04 pm2.11 exmid 11-Oct-04 sbf1 --- obsolete; use sbf instead 11-Oct-04 ceqsexg ceqex 9-Oct-04 fvco2 fvco3 8-Oct-04 indif0 difdisj 8-Oct-04 biopab opabbii.2 8-Oct-04 bioprab oprabbieqi 7-Oct-04 ssii sselii 6-Oct-04 op2nd op2ndb 6-Oct-04 op1st op1stb 3-Oct-04 ind nnind 3-Oct-04 sylan5 sylan2 3-Oct-04 sylan5b sylan2b 3-Oct-04 sylan5br sylan2br 3-Oct-04 sylan5d sylan2i 3-Oct-04 zind --- obsolete; use uzind 30-Sep-04 fvop funfvop 30-Sep-04 funfvop funopfv 30-Sep-04 pm4.21 bicom 30-Sep-04 bicom bicomi 30-Sep-04 entr entri 30-Sep-04 sstr2qqq sstr 30-Sep-04 sstr sstr2 30-Sep-04 sstr2 sstr2qqq 29-Sep-04 xp0qqq xp0r 29-Sep-04 xp0r xp0 29-Sep-04 xp0 xp0qqq 28-Sep-04 xpdom xpdom2 changed variable names 28-Sep-04 xpdom2 xpdom3 26-Sep-04 xpindi inxp 26-Sep-04 xpun1 xpundi 26-Sep-04 xpun2 xpundir 25-Sep-04 entr entrt 23-Sep-04 ssfnres --- obsolete; use fnssres instead 23-Sep-04 resun resundi 21-Sep-04 f11 [--same--] changed o.p. membership to binary relation 21-Sep-04 unisuc [--same--] swapped arguments of = sign 21-Sep-04 onunisuc [--same--] swapped arguments of = sign 21-Sep-04 undif3 --- obsolete; use undif 21-Sep-04 ssequn2 [--same--] swapped arguments of = sign 21-Sep-04 sseqin2 [--same--] swapped arguments of = sign 21-Sep-04 onelun [--same--] swapped arguments of = sign 21-Sep-04 dfss4 [--same--] swapped arguments of = sign 21-Sep-04 ordunisuc ordunisssuc 21-Sep-04 ssfun funss 15-Sep-04 19.6 alex 15-Sep-04 alex alexeq 15-Sep-04 19.11 excom 15-Sep-04 19.11a excomim 15-Sep-04 19.5 alcom 15-Sep-04 19.7 alnex 15-Sep-04 19.14 exnal 15-Sep-04 alnex alinexa 15-Sep-04 exnal exanali 15-Sep-04 dmsn dmsnop 15-Sep-04 rnsn rnsnop 13-Sep-04 ppnull pwpw0 13-Sep-04 pwnull pw0 13-Sep-04 zfnull2 zfnul 13-Sep-04 nullpss 0pss 13-Sep-04 nullss 0ss 13-Sep-04 nulleq eq0 13-Sep-04 nnull n0 13-Sep-04 nnullf n0f 13-Sep-04 xpdisj xpsndisj 13-Sep-04 subdist subdi 13-Sep-04 negdist negdi 13-Sep-04 nndist nndi 13-Sep-04 xpindist inxp 11-Sep-04 ssd sseld 11-Sep-04 ssi sseli 11-Sep-04 vtoclab elab2 11-Sep-04 vtoclabg elab2g 11-Sep-04 elab2g elab3g 6-Sep-04 comm com12 4-Sep-04 opabval fvopab3 4-Sep-04 opabvalig fvopab3ig 4-Sep-04 opabval2g fvopab4g 4-Sep-04 opabval2 fvopab4 3-Sep-04 undif2 difun2 1-Sep-04 dedlem2 [--same--] swapped arguments of = sign 1-Sep-04 dedlem1 [--same--] swapped arguments of = sign 31-Aug-04 pm2.16d con3d 31-Aug-04 pm2.03d con2d 31-Aug-04 pm2.15d con1d 31-Aug-04 pm2.16 con3 31-Aug-04 pm2.03 con2 31-Aug-04 pm2.15 con1 31-Aug-04 con3 con3i 31-Aug-04 con2 con2i 31-Aug-04 con1 con1i 29-Aug-04 oprabelrn elrnoprab 27-Aug-04 ssequn1 [--same--] swapped arguments of = sign 27-Aug-04 df-ss dfss 27-Aug-04 imdistanb --- obsolete; use imdistan 27-Aug-04 imdistan [--same--] now includes converse 17-Aug-04 difun2 [--same--] swapped arguments of = sign 17-Aug-04 undif1 [--same--] swapped arguments of = sign and union 17-Aug-04 difin [--same--] swapped arguments of = sign 17-Aug-04 unindistr undir 17-Aug-04 unindist undi 17-Aug-04 inundistr indir 17-Aug-04 inundist indi 17-Aug-04 indist inindi 16-Aug-04 ss2un unss12 order of variables changed 15-Aug-04 funmo,dffunmof,dffunmo [--same--] ordered pair membership -> binary relation 15-Aug-04 dfrel2 [--same--] swapped arguments of = sign 12-Aug-04 unxp xpundir 11-Aug-04 elima2 elima3 11-Aug-04 reluni [--same--] restricted quantifier and added converse 9-Aug-04 imun imaun 3-Aug-04 1id om1 3-Aug-04 oalim [--same--] conjoined antecedents; now uses indexed union 3-Aug-04 divdiv23 divdiv23z 3-Aug-04 divdiv23i divdiv23 2-Aug-04 divrec,divrecz [--same--] swapped A and B 2-Aug-04 zq zqt 2-Aug-04 qre qret 1-Aug-04 mulcant [--same--] swapped conjunct in antecedent 1-Aug-04 axrecex,axrrecex,divclt,divcan1t,divcan2t,recidt,divdistrt,divrclt [--same--] conjoined the two left-most antecedents 1-Aug-04 peano1c 1nn 1-Aug-04 1nn 1onn 28-Jul-04 sbco0 sbid2 28-Jul-04 sbid2 sbid2v 26-Jul-04 cardonval oncardval 15-Jun-04 ssin [--same--] swapped biconditional order 15-Jun-04 unss [--same--] swapped biconditional order 11-Jun-04 dfun2 df-un 11-Jun-04 df-un dfun2 11-Jun-04 dfin2 df-in 11-Jun-04 df-in dfin2 3-Jun-04 ssintss intss 3-Jun-04 intss intss1 30-May-04 r1clos r1pwcl now uses antecedent instead of hypothesis 30-May-04 r1powt r1pw 28-May-04 sqvalt --- obsolete; use exp2 28-May-04 expntwo exp2 28-May-04 expnone --- obsolete; use expp1t 28-May-04 expnsuc --- obsolete; use expp1t 28-May-04 expnzer --- obsolete; use exp0t 26-May-04 ontrt --- obsolete; use onelon instead 26-May-04 ddelim* [--same--] (*=wildcard) changed order of hypotheses 21-May-04 fvcnvb f1ocnvfvb 21-May-04 fvcnv f1ocnvfv 21-May-04 sbcb sbcbidig now uses antecedent instead of hypothesis 21-May-04 sbci sbcimg 21-May-04 sbb sbbi 21-May-04 sbo sbor 21-May-04 sbi sbim 21-May-04 sbim sbimi 21-May-04 sba sban 21-May-04 fvelrn [--same--] changed to restricted quantifier 8-Feb-04 zfpowb pwexb 8-Feb-04 zfpowcl pwex 8-Feb-04 zfnull 0ex 8-Feb-04 limelon [--same--] changed first -> to /\ in antecedent =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 2. Finding shorter proofs =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= I like shorter proofs, and any shorter proof I accept will be acknowledged. Usually I will automatically accept shorter proofs that (1) shorten the set.mm file (with compressed proofs), (2) reduce the size of the HTML file generated with SHOW STATEMENT xx / HTML, (3) use only existing, unmodified theorems in the database (the order of theorems may be changed though), (4) use no additional axioms, and (5) involve none of the special cases listed below. Usually I will also automatically accept a _new_ theorem that is used to shorten multiple proofs, if the total size of set.mm (including the comment of the new theorem) decreases as a result. In borderline cases, I may choose to look primarily at the number of compressed proof steps with less weight on the length of the label section (since the names are in principal arbitrary). If two proofs have the same number of compressed proof steps, I will typically give preference to the one with the smaller number of different labels, or if these are the same, the proof with the fewest number of characters that the proofs happen to have by chance when label lengths are included. The remainder of this section lists theorems that purposely do not have shortest proofs for various reasons. It is primarily a reminder to myself and normally you don't have to worry about it. In the list, theorem names are surrounded by whitespace to facilitate future label changes. The proofs of id1 , snex , sbth , ordon , ltso and several other theorems (in particular ones avoiding ax-reg and ax-ac ) could be made shorter but are longer to illustrate specific points or to avoid specific axioms. The following proofs should not be MINIMIZE_WITH'ed in the Proof Assistant, since they are for illustrative purposes, have proofs that avoid certain axioms, or involve areas I want to rework in the future. " id1 " using anything " dfbi1gb " using anything " con3th " using " con3 " " merlem1 " through " ax3 " using anything " ax4-* " using " ax-4 " " ax6-* " using " ax-6o " " ax7-* " using " ax-7 " " hbequid " using " equid " " dvelimf " using " dvelimfALT " anything using " om0x " (i.e. don't use om0x - use om0 instead) " dtruALT " , " dtru " , " ax16 " using anything " pwpw0 " using " pwsn " " omex " using " inf3 " " pjpji " using " pjpj0i " " pjomli " using " omlsi " " pjococi " using " omlsii " " pjococi " using " ococi " " pjpjth " using " pjth " " pjpjthi " using " pjthi " In set theory, don't use equequ1 , equequ2 , elequ1 , elequ2 - use the set theory versions eqeq1 , eqeq2 , eleq1 , eleq2 instead. Don't use ax17eq or ax17el - use ax-17 instead. Don't use elirr if efrirr , ordirr , or onirr can be used (to avoid the Axiom of Regularity when it is not needed). Always use weq, wel, wsb instead of wceq, wcel, wsbc in predicate calculus. The opposite applies to set theory. If e.g. weq is accidentally used in set theory, "minimize_with wceq / allow_growth" in the Proof Assistant will replace it with wceq. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 3. Bibliography =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Bibliographical references are made by bracketing an identifer in a theorem's comment, such as [RussellWhitehead]. These refer to HTML tags on the following web pages: Logic and set theory - see http://us.metamath.org/mpegif/mmset.html#bib Hilbert space - see http://us.metamath.org/mpegif/mmhil.html#ref =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 4. Quick "How To" =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= How to use this file under Windows 95/98/NT/2K/XP/Vista: 1. Download the program metamath.exe per the instructions on the Metamath home page (http://us.metamath.org) and put it in the same directory as this file (set.mm). 2. In Windows Explorer, double-click on metamath.exe. 3. Type "read set.mm" and press Enter. 4. Type "help" for a list of help topics, and "help demo" for some command examples. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= 5. Metamath syntax summary =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= The HELP LANGUAGE command in the Metamath program will give you a quick overview of Metamath. Syntax summary: $c ... $. - Constant declaration $v ... $. - Variable declaration $d ... $. - Disjoint (distinct) variable restriction