Skip to content

Commit 16bc0ae

Browse files
jkingdonjkingdon
committed
Remove fisum from iset.mm
No longer used and replaced by fsum3 .
1 parent ec2260a commit 16bc0ae

File tree

2 files changed

+6
-79
lines changed

2 files changed

+6
-79
lines changed

‎iset-discouraged‎

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,6 @@
171171
"iseqcaopr" is used by "iseradd".
172172
"iseqcaopr2" is used by "iseqcaopr".
173173
"iseqcaopr3" is used by "iseqcaopr2".
174-
"iseqcl" is used by "fisum".
175174
"iseqcl" is used by "iseqcaopr2".
176175
"iseqcl" is used by "iseqcoll".
177176
"iseqcl" is used by "iseqp1".
@@ -183,7 +182,6 @@
183182
"iseqeq1" is used by "zisum".
184183
"iseqeq2" is used by "seqeq2".
185184
"iseqeq3" is used by "cbvsum".
186-
"iseqeq3" is used by "fisum".
187185
"iseqeq3" is used by "isummo".
188186
"iseqeq3" is used by "seqeq3".
189187
"iseqeq3" is used by "sumeq1".
@@ -202,7 +200,6 @@
202200
"iseqfeq" is used by "fisumcvg2".
203201
"iseqfeq" is used by "zisum".
204202
"iseqfeq2" is used by "iseqid".
205-
"iseqfveq" is used by "fisum".
206203
"iseqfveq" is used by "fisumser".
207204
"iseqfveq" is used by "iseqfeq".
208205
"iseqfveq2" is used by "iseqfeq2".
@@ -235,7 +232,6 @@
235232
"iseradd" is used by "ser3add".
236233
"iserf" is used by "fisumcvg".
237234
"iserf" is used by "ser0f".
238-
"isummo" is used by "fisum".
239235
"isummolem2" is used by "isummo".
240236
"isummolem2a" is used by "isummolem2".
241237
"isummolem2a" is used by "zisum".
@@ -388,7 +384,6 @@ New usage of "elirr" is discouraged (16 uses).
388384
New usage of "equsalh" is discouraged (5 uses).
389385
New usage of "eu3h" is discouraged (3 uses).
390386
New usage of "exmidfodomrlemrALT" is discouraged (0 uses).
391-
New usage of "fisum" is discouraged (0 uses).
392387
New usage of "fisumcvg" is discouraged (2 uses).
393388
New usage of "fisumcvg2" is discouraged (1 uses).
394389
New usage of "fisumser" is discouraged (2 uses).
@@ -400,17 +395,17 @@ New usage of "iseq1t" is discouraged (1 uses).
400395
New usage of "iseqcaopr" is discouraged (1 uses).
401396
New usage of "iseqcaopr2" is discouraged (1 uses).
402397
New usage of "iseqcaopr3" is discouraged (1 uses).
403-
New usage of "iseqcl" is discouraged (4 uses).
398+
New usage of "iseqcl" is discouraged (3 uses).
404399
New usage of "iseqcoll" is discouraged (1 uses).
405400
New usage of "iseqeq1" is discouraged (5 uses).
406401
New usage of "iseqeq2" is discouraged (1 uses).
407-
New usage of "iseqeq3" is discouraged (7 uses).
402+
New usage of "iseqeq3" is discouraged (6 uses).
408403
New usage of "iseqex" is discouraged (4 uses).
409404
New usage of "iseqfcl" is discouraged (4 uses).
410405
New usage of "iseqfclt" is discouraged (2 uses).
411406
New usage of "iseqfeq" is discouraged (2 uses).
412407
New usage of "iseqfeq2" is discouraged (1 uses).
413-
New usage of "iseqfveq" is discouraged (3 uses).
408+
New usage of "iseqfveq" is discouraged (2 uses).
414409
New usage of "iseqfveq2" is discouraged (2 uses).
415410
New usage of "iseqid" is discouraged (2 uses).
416411
New usage of "iseqid2" is discouraged (2 uses).
@@ -423,7 +418,7 @@ New usage of "iseqvalt" is discouraged (3 uses).
423418
New usage of "iser0" is discouraged (1 uses).
424419
New usage of "iseradd" is discouraged (1 uses).
425420
New usage of "iserf" is discouraged (2 uses).
426-
New usage of "isummo" is discouraged (1 uses).
421+
New usage of "isummo" is discouraged (0 uses).
427422
New usage of "isummolem2" is discouraged (1 uses).
428423
New usage of "isummolem2a" is discouraged (2 uses).
429424
New usage of "isummolem3" is discouraged (2 uses).

‎iset.mm‎

Lines changed: 2 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -115662,75 +115662,6 @@ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
115662115662
GAVEBGUFVEBGUGLVEBGUJUKUHZEOVHSZCDSVGJUIULVGVHBRCQRZEBUMZVIQRZVJAVMVFAVLE
115663115663
BMTUNVLVNEVHBEVIQEVHCUOUPVKCVIQEVHCUQURVAVBUSUTT $.
115664115664

115665-
$( The value of a sum over a nonempty finite set. (Contributed by Mario
115666-
Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 14-Sep-2022.) Use
115667-
~ fsum3 instead. (New usage is discouraged.) $)
115668-
fisum $p |- ( ph -> sum_ k e. A B = ( seq 1 ( + ,
115669-
( n e. NN |-> if ( n <_ M , ( G ` n ) , 0 ) ) , CC ) ` M ) ) $=
115670-
( wcel cc cc0 c1 cn wceq vm vj vx vf vy vu vi csu cv cuz cfv wss wdc wral
115671-
caddc cz csb cif cmpt cseq4 cli wbr w3a wrex cfz co cle wa wex wo df-isum
115672-
wf1o cio syl6eleq eqimss2i sseli adantl weq fveq2 eleq1d fsumgcl ad2antrr
115673-
nnuz 1zzd nnzd eluzelz ad2antlr 3jca eluzle simpr jca sylanbrc rspcdva wn
115674-
elfz2 0cnd adantr syl2anc ifcldadc breq1 ifbieq1d eqid fvmptg eqeltrd wmo
115675-
wb chash eleq1w cbvmptv ralrimiva nfcsb1v csbeq1a rspc csbeq1d cfn fzfigd
115676-
nfel1 syl ifbid mpteq2dv iseqeq3 fveq1d eqeq2d exbidv cvv cbvral r19.21bi
115677-
sylib nfv iftrued eqtrd csbied sylc nfcv fvmptf vex anbi12d breq2 rexbidv
115678-
nfif zdcle addcl iseqcl csbeq1 mpan9 csbco syl6eqr isummo cbvralv 3anbi2i
115679-
dcbid rexbii nnz fihasheqf1oi sylan nnnn0 hashfz1 eqtr3d pm5.32da rexbiia
115680-
cn0 breq2d orbi12i mobii f1of fex nfeq2 eqeq12d elfznn ffvelrnda eqeltrrd
115681-
elfzle2 3eqtr4d iseqfveq f1oeq1 fveq1 fvex syl6eqelr ifeq1d spcegv f1oeq2
115682-
wf oveq2 fveq12d rspcev olcd 3anbi3d eqeq1 anbi2d orbi12d moi2 syl5ibrcom
115683-
id syl22anc ex impbid iota5 mpdan syl5eq ) ABCEUHBUAUIZUJUKZULZUBUIZBOZUM
115684-
ZUBUXAUNZUOPFUPFUIZBOZEUXGCUQZQURZUSZUWTUTZUCUIZVAVBZVCZUAUPVDZRUWTVEVFZB
115685-
UDUIZVLZUXMUWTUOPFSUXGUWTVGVBZEUXGUXRUKZCUQZQURZUSZRUTZUKZTZVHZUDVIZUASVD
115686-
ZVJZUCVMZIUOPFSUXGIVGVBZUXGHUKZQURZUSZRUTUKZUCBCUDUBEUAFVKAUYQPOZUYLUYQTA
115687-
UCUEUOPUYPRIAISRUJUKZKWCVNZAUXMUYSOZVHZUXMUYPUKZUXMIVGVBZUXMHUKZQURZPVUBU
115688-
XMSOZVUFPOVUCVUFTVUAVUGAUYSSUXMSUYSWCVOVPVQZVUBVUDVUEQPVUBVUDVHZUYNPOZVUE
115689-
POFRIVEVFZUXMFUCVRZUYNVUEPUXGUXMHVSZVTAVUJFVUKUNZVUAVUDABCDEFGHIJKLMNWAZW
115690-
BVUIRUPOZIUPOZUXMUPOZVCRUXMVGVBZVUDVHUXMVUKOZVUIVUPVUQVURVUIWDAVUQVUAVUDA
115691-
IKWEZWBVUAVURAVUDRUXMWFWGWHVUIVUSVUDVUAVUSAVUDRUXMWIWGVUBVUDWJWKUXMRIWOWL
115692-
ZWMVUBVUDWNVHWPZVUBVURVUQVUDUMVUBUXMVUHWEAVUQVUAVVAWQUXMIUUAWRZWSZFUXMUYO
115693-
VUFSPUYPVULUYMVUDUYNVUEQUXGUXMIVGWTZVUMXAUYPXBZXCWRVVEXDZUXMPOUEUIZPOVHUX
115694-
MVVIUOVFPOAUXMVVIUUBVQZUUCZAUYKUCUYQPAUYKUXMUYQTZXFUYRAUYKVVLAUYKVVLAUYKV
115695-
HUYRUYKUCXEZUYKUXBUXFUXLUYQVAVBZVCZUAUPVDZUXSUYQUYFTZVHZUDVIZUASVDZVJZVVL
115696-
AUYRUYKVVKWQAVVMUYKAUXBUFUIBOZUMZUFUXAUNZUXNVCZUAUPVDZUXSUXMUWTUOPFSUXGBX
115697-
GUKZVGVBZUYBQURZUSZRUTZUKZTZVHZUDVIZUASVDZVJZUCXEVVMAUCBEUXCCUQZUDUFUBUAU
115698-
GUXKVWJFUBUPUXJUXDVWRQURFUBVRUXHUXDUXIVWRQFUBBXHEUXGUXCCUUDXAXIACPOZEBUNZ
115699-
UXDVWRPOZAVWSEBMXJZVWSVXAEUXCBEVWRPEUXCCXKXQEUBVRCVWRPEUXCCXLVTXMUUEFUGSV
115700-
WIUGUIZVWGVGVBZUBVXCUXRUKZVWRUQZQURFUGVRZVWHVXDUYBVXFQUXGVXCVWGVGWTVXGUYB
115701-
EVXECUQVXFVXGEUYAVXECUXGVXCUXRVSXNEUBVXECUUFUUGXAXIUUHVWQUYKUCVWFUXPVWPUY
115702-
JVWEUXOUAUPVWDUXFUXBUXNVWCUXEUFUBUXAUFUBVRVWBUXDUFUBBXHUUKUUIUUJUULVWOUYI
115703-
UASUWTSOZVWNUYHUDVXHUXSVWMUYGVXHUXSVHZVWLUYFUXMVXIUWTVWKUYEVXIVWJUYDTVWKU
115704-
YETVXIFSVWIUYCVXIVWHUXTUYBQVXIVWGUWTUXGVGVXIUXQXGUKZVWGUWTVXHUXQXOOUXSVXJ
115705-
VWGTVXHRUWTVXHWDUWTUUMXPUXQBUXRUUNUUOVXIUWTUVAOZVXJUWTTVXHVXKUXSUWTUUPWQU
115706-
WTUUQXRUURUVBXSXTUOPVWJUYDRYAXRYBYCUUSYDUUTUVCUVDYHWQAUYKWJAVWAUYKAVVTVVP
115707-
AISOVUKBUXRVLZUYQIUOPFSUYMUYBQURZUSZRUTZUKZTZVHZUDVIZVVTKAGYEOZVUKBGVLZUY
115708-
QIUOPFSUYMDQURZUSZRUTZUKZTZVHZVXSAVUKBGUWBZVUKXOOVXTAVYAVYHLVUKBGUVEXRZAR
115709-
IAWDVVAXPVUKBXOGUVFWRAVYAVYFLAUCUEUOPEUYPVYCRIUYTAEUIZVUKOZVHZVYJHUKZFVYJ
115710-
DUQZVYJUYPUKZVYJVYCUKZAVYMVYNTZEVUKAUYNDTZFVUKUNVYQEVUKUNAVYRFVUKNXJVYRVY
115711-
QFEVUKVYREYIFVYMVYNFVYJDXKZUVGFEVRZUYNVYMDVYNUXGVYJHVSZFVYJDXLZUVHYFYHYGV
115712-
YLVYOVYJIVGVBZVYMQURZVYMVYLVYJSOZWUDPOVYOWUDTVYKWUEAVYJIUVIVQZVYLWUDVYMPV
115713-
YLWUCVYMQVYKWUCAVYJRIUVLVQZYJZVYLVUJVYMPOFVUKVYJVYTUYNVYMPWUAVTAVUNVYKVUO
115714-
WQAVYKWJWMXDFVYJUYOWUDSPUYPVYTUYMWUCUYNVYMQUXGVYJIVGWTZWUAXAVVGXCWRWUHYKV
115715-
YLVYPWUCVYNQURZVYNVYLWUEWUJPOVYPWUJTWUFVYLWUJVYNPVYLWUCVYNQWUGYJZAVYNPOZE
115716-
VUKADPOZFVUKUNZWULEVUKUNAWUMFVUKAUXGVUKOZVHZEUXGGUKZCUQZDPWUPEWUQCDBAVUKB
115717-
UXGGVYIUVJZVYJWUQTZCDTZWUPJVQYLWUPWUQBOVWTWURPOZWUSAVWTWUOVXBWQVWSWVBEWUQ
115718-
BEWURPEWUQCXKXQWUTCWURPEWUQCXLVTXMYMUVKXJZWUMWULFEVUKWUMEYIFVYNPVYSXQVYTD
115719-
VYNPWUBVTYFYHYGXDFVYJVYBWUJSVYCPFVYJYNWUCFVYNQWUCFYIVYSFQYNZYTVYTUYMWUCDV
115720-
YNQWUIWUBXAVYCXBZYOWRWUKYKUVMVVHVUBUXMVYCUKZVUDFUXMDUQZQURZPVUBVUGWVHPOWV
115721-
FWVHTVUHVUBVUDWVGQPVUIVUTWUNWVGPOZVVBAWUNVUAVUDWVCWBWUMWVIFUXMVUKFWVGPFUX
115722-
MDXKZXQVULDWVGPFUXMDXLZVTXMYMVVCVVDWSZFUXMVYBWVHSVYCPFUXMYNVUDFWVGQVUDFYI
115723-
WVJWVDYTVULUYMVUDDWVGQVVFWVKXAWVEYOWRWVLXDVVJUVNWKVXRVYGUDGYEUXRGTZVXLVYA
115724-
VXQVYFVUKBUXRGUVOWVMVXPVYEUYQWVMIVXOVYDWVMVXNVYCTVXOVYDTWVMFSVXMVYBWVMUYM
115725-
UYBDQWVMUYBWURDWVMEUYAWUQCUXGUXRGUVPZXNWVMEWUQCDYEWVMWUQUYAYEWVNUXGUXRYEY
115726-
EUDYPFYPUVQUVRWUTWVAWVMJVQYLYKUVSXTUOPVXNVYCRYAXRYBYCYQUVTYMVVSVXSUAISUWT
115727-
ITZVVRVXRUDWVOUXSVXLVVQVXQWVOUXQVUKTUXSVXLXFUWTIRVEUWCUXQVUKBUXRUWAXRWVOU
115728-
YFVXPUYQWVOUWTIUYEVXOWVOUYDVXNTUYEVXOTWVOFSUYCVXMWVOUXTUYMUYBQUWTIUXGVGYR
115729-
XSXTUOPUYDVXNRYAXRWVOUWMUWDYCYQYDUWEWRUWFZWQUYKVWAUCUYQPVVLUXPVVPUYJVVTVV
115730-
LUXOVVOUAUPVVLUXNVVNUXBUXFUXMUYQUXLVAYRUWGYSVVLUYIVVSUASVVLUYHVVRUDVVLUYG
115731-
VVQUXSUXMUYQUYFUWHUWIYDYSUWJZUWKUWNUWOAUYKVVLVWAWVPWVQUWLUWPWQUWQUWRUWS
115732-
$.
115733-
115734115665
${
115735115666
$d A f i j k m n u x $. $d B f i j m n u x $. $d C f k m x $.
115736115667
$d C k x y $. $d F f k n $. $d G f k m n x $. $d G k n x y $.
@@ -135637,7 +135568,8 @@ different should be named differently (we do have a small number of
135637135568
<tr><td>seq3, sum3</td><td>recursive sequence</td><td> ~ df-seq3 </td>
135638135569
<td> </td><td>Yes</td><td> ~ seq3-1 , ~ fsum3 </td></tr>
135639135570
<tr><td>iseq , isum</td><td>recursive sequence</td><td> ~ df-iseq </td>
135640-
<td> </td><td>Yes</td><td> ~ iseq1 , ~ fisum </td></tr>
135571+
<td> </td><td>Yes</td>
135572+
<td><i>subject to change as this is being replaced by seq3</td></tr>
135641135573
</table>
135642135574
</HTML>
135643135575

0 commit comments

Comments
 (0)