stanford-oval/wikipedia huggingface dataset:
馬斯科吉縣 (喬治亞州)

此条目页的主題是美國喬治亞州的一個縣。同名的縣，請見「」。
| 馬斯科吉縣 Muscogee County |
| --- | --- |
市县合一
哥倫布聯合行政中心
 馬斯科吉縣于佐治亚州中的位置
 佐治亚州于美国的位置
坐标： 32°31′N 84°52′W﻿ / ﻿32.51°N 84.87°W﻿ / 32.51; -84.87
国家:  美国
州:  佐治亚州
设立日期: 1826年6月9日，​198年前​（1826-06-09）
語源: 馬斯科吉人
县治: 哥伦布
最大城市: 哥伦布
面积
 • 总计: 221 平方英里（600 平方公里）
 • 陸地: 216 平方英里（600 平方公里）
 • 水域: 4.6 平方英里（10 平方公里）  2.1%
人口（2020年）
 • 總計: 206,922人
 • 密度: 958人/平方英里（370人/平方公里）
时区: 东部时区（UTC−5）
 • 夏时制: 东部时区（UTC−4）
包含的国会选区: 第2選區、​第3選區
網站: www.columbusga.gov
馬斯科吉縣（英語：）是美国喬治亞州西部的一個縣，西鄰亚拉巴马州，面積572平方公里。根據2020年美國人口普查，共有人口20萬6,922人。該縣成立於1826年12月11日，縣政府成立於1827年12月24日；1971年與原縣治哥倫布（）合併。縣名是克里克语（）的自稱。
特雷泽勒

| 特雷泽勒 Trézelles |
| --- | --- |
 法國市镇

特雷泽勒的位置  
特雷泽勒显示法国的地图特雷泽勒显示阿列省的地图
坐标：46°19′44″N 3°35′32″E﻿ / ﻿46.3289°N 3.5922°E﻿ / 46.3289; 3.5922
国家:  法國
大区:  
省:  阿列省
面积1
 • 市镇: 18.14 平方公里（7.00 平方英里）
人口（2021年）
 • 市镇: 400人
 • 密度: 22.1人/平方公里（57.1人/平方英里）
时区: CET（UTC+01:00）
 • 夏时制: CEST（UTC+02:00）
邮政编码: 03220
INSEE: 03291 
省级选区: 穆兰第二县（英语：）
海拔: 250—330（820—1,083英尺） （平均：290米）
網站: http://trezelles.interco-abl.eu
1法國統計部門在計算土地面積時，不計算面積大於1平方公里的湖泊、池塘、冰川和河口。 2「人口不重複計算」：擁有多重居住地的居民（如：學生和軍人）僅計算一次。
特雷泽勒（法語：，法语发音：[tʁezɛl]）是法国阿列省的一个市镇，位于该省东部，属于维希区。
地理

特雷泽勒（46°19'44"N, 3°35'32"E）面积18.14 平方千米，位于法国奥弗涅-罗讷-阿尔卑斯大区阿列省，该省份为法国中部省份，北起涅夫勒省、西北接谢尔省，西南至克勒兹省，南至多姆山省，东南临卢瓦尔省，东临索恩-卢瓦尔省。
与特雷泽勒接壤的市镇（或旧市镇、城区）包括：沙夫罗什、桑德雷、塞尔维利、泰什河畔瓦雷讷。
特雷泽勒的时区为UTC+01:00、UTC+02:00（夏令时）。
行政

特雷泽勒的邮政编码为03220，INSEE市镇编码为03291。
政治

特雷泽勒所属的省级选区为穆兰第二县（英语：）。
人口

特雷泽勒于2021年1月1日时的人口数量为400人。
特雷泽勒的OSM定位图
1962-2008年间特雷泽勒人口变化图示
塞斯蒂诺

| 塞斯蒂诺 |
| --- | --- |
市镇
Sestino
塞斯蒂诺塞斯蒂诺在意大利的位置
坐标：43°42′38″N 12°17′56″E﻿ / ﻿43.7106°N 12.2989°E﻿ / 43.7106; 12.2989
国家:  義大利
省份或广域市: 阿雷佐省
面积
 • 总计: 80.46 平方公里（31.07 平方英里）
人口（2009）
 • 總計: 1,463人
 • 密度: 18.2人/平方公里（47.1人/平方英里）
时区: CET（UTC+1）
 • 夏时制: CEST（UTC+2）
邮编: 52038
塞斯蒂诺（義大利語：），是意大利阿雷佐省的一个市镇。总面积80.46平方公里，人口1463人，人口密度18.2人/平方公里（2009年）。ISTAT代码为051035。
前10世紀月食列表

月食的產生：地球遮挡了太阳的直射光线，导致月食出现。在本影区，直射阳光全部被地球遮挡，无法照到月球上出现月全食；在半影区，则仅有部分阳光被遮挡，出现月偏食或半影月食。
前10世紀月食列表為月食列表的其中之一，本表依照月食發生的年度排序。藉由下方數據的列表統計，前10世紀月食發生次數，一共是228次。其中月全食87次，半影月食61次，月偏食80次。由各年度月食發生的列表中發覺到每一年的出現次數至少兩次（發生時間幾乎接近農曆的十五日）。
公元前1000年至公元前901年月食列表

| 02643 | 46 | 26 | 76 | -907年4月16日 | 3:48:01 | 半影月食 | A | 0.9069 | 0.2129 | 263.3 | 99.5 |  | 2:58:16 |  |  | 4:37:46 |  |
| 02644 | 51 | 12 | 73 | -907年10月9日 | 10:04:01 | 半影月食 | D | -0.9817 | 0.0312 | 277.6 | 41.5 |  | 9:43:16 |  |  | 10:24:46 |  |
| 02645 | 18 | 66 | 73 | -906年3月7日 | 3:37:51 | 月偏食 | A | -1.0277 | -0.0527 | 273.1 |  |  |  |  |  |  |  |
| 02646 | 23 | 52 | 73 | -906年8月30日 | 10:02:56 | 月偏食 | D | 1.0475 | -0.0468 | 236.9 |  |  |  |  |  |  |  |
| 02647 | 28 | 56 | 74 | -905年2月24日 | 5:19:57 | 月全食 | A | -0.3149 | 1.2374 | 369.1 | 223.4 | 74.7 | 3:28:15 | 4:42:36 | 5:57:18 | 7:11:39 |  |
| 02648 | 33 | 43 | 73 | -905年8月20日 | 2:31:31 | 月全食 | D | 0.3474 | 1.2416 | 311.4 | 199.2 | 68.2 | 0:51:55 | 1:57:25 | 3:05:37 | 4:11:07 |  |
| 02649 | 38 | 28 | 72 | -904年2月13日 | 5:33:26 | 月全食 | A | 0.4057 | 1.0776 | 356.4 | 211.9 | 44.4 | 3:47:29 | 5:11:14 | 5:55:38 | 7:19:23 |  |
| 02650 | 43 | 32 | 85 | -904年8月8日 | 17:15:34 | 月全食 | D | -0.3825 | 1.1600 | 325.1 | 202.7 | 58.8 | 15:34:13 | 16:46:10 | 17:44:58 | 18:56:55 |  |
| 02651 | 48 | 19 | 75 | -903年2月1日 | 11:18:55 | 月偏食 | A | 1.0957 | -0.1637 | 246.1 |  |  |  |  |  |  |  |
| 02652 | 53 | 6 | 72 | -903年7月29日 | 2:03:46 | 月偏食 | D | -1.1765 | -0.3230 | 238.3 |  |  |  |  |  |  |  |
| 02653 | 20 | 59 | 72 | -903年12月23日 | 13:34:06 | 半影月食 | A | -0.9414 | 0.1451 | 254 | 81.3 |  | 12:53:27 |  |  | 14:14:45 |  |
| 02654 | 25 | 64 | 87 | -902年6月18日 | 12:52:50 | 半影月食 | D | 0.9031 | 0.1674 | 306.3 | 98.6 |  | 12:03:32 |  |  | 13:42:08 |  |
| 02655 | 30 | 51 | 74 | -902年12月13日 | 5:06:01 | 月全食 | A | -0.2853 | 1.3418 | 320 | 204.5 | 78.7 | 3:23:46 | 4:26:40 | 5:45:22 | 6:48:16 |  |
| 02656 | 35 | 36 | 72 | -901年6月7日 | 15:59:41 | 月全食 | D | 0.1139 | 1.6347 | 355.1 | 227.1 | 101.3 | 14:06:08 | 15:09:02 | 16:50:20 | 17:53:14 |  |
| 02657 | 40 | 27 | 73 | -901年12月2日 | 16:56:59 | 月全食 | A | 0.4139 | 1.0801 | 335.1 | 202.4 | 43.2 | 15:15:47 | 16:35:23 | 17:18:35 | 18:38:11 |  |
| 02658 | 45 | 26 | 85 | -900年5月27日 | 2:12:10 | 半影月食 | D | -0.6564 | 0.6662 | 300.5 | 166.9 |  | 0:48:43 |  |  | 3:35:37 |  |
| 02659 | 50 | 14 | 73 | -900年11月20日 | 21:40:24 | 月偏食 | A | 1.1444 | -0.2871 | 256.8 |  |  |  |  |  |  |  |
註釋

↑  當整個月球進入地球的本影內時，在其前後均會發生月偏食與半影月食。
↑  此時月球只是掠過地球的半影區，造成月面的光度極輕微減弱，所以較不易為人注意。
↑  當月球只有部份進入地球的本影時，在其前後均會發生半影月食。
↑  本列表採用天文計年，例如：-999年相當於公元前1000年，-900年相當於公元前901年。
哲羅魚屬

| 哲罗鱼属 |
| --- | --- |

多瑙哲羅魚 Hucho hucho

科学分类 
界：: 动物界 Animalia
门：: 脊索动物门 Chordata
纲：: 綱 Actinopteri
目：: 鮭形目 Salmoniformes
科：: 鮭科 Salmonidae
亚科：: 鲑亚科 Salmoninae
属：: 哲罗鱼属 Hucho Günther, 1866

模式種
多瑙哲羅魚 Hucho hucho (Linnaeus, 1758)
种
 虎嘉哲羅魚 H. bleekeri  多瑙哲羅魚 H. hucho  石川哲羅魚 H. ishikawae  遠東哲羅魚 H. perryi  哲羅魚 H. taimen
哲羅魚屬（学名：）是鲑形目鮭科的一属。
分類

本属属于鲑亚科，共包含5个现存物种：
虎嘉哲羅魚 Hucho bleekeri：又稱四川哲罗鱼。
多瑙哲羅魚 Hucho hucho
石川哲羅魚 Hucho ishikawae
哲羅鮭 Hucho taimen
遠東哲羅魚（Parahucho perryi）原先也被归于哲罗鱼属（学名为Hucho perryi），但是基因学研究和证据表明它其实应该单独属于另外一个叫作副哲罗鱼属（Parahucho）的新属。
參考文献

↑  Froese, R. & Pauly, D. (eds.) (2012). Species of Hucho. FishBase. Version 2012-02.
↑  Oleinik, A.G.; and Skurikhina, L.A. (2008). Phylogenetic relationships of Sakhalin taimen Parahucho perryi inferred from PCR-RFLP analysis of mitochondrial DNA. Russian Journal of Genetics, 44:767. doi:10.1134/S102279540807003X
↑  Matveev, V.; Nishihara, H.; & Okada, N. (2007). Novel SINE families from salmons validate Parahucho (Salmonidae) as a distinct genus and give evidence that SINEs can incorporate LINE-related 3′-tails of other SINEs. Molecular Biology and Evolution 24(8): 1656-1666. doi: 10.1093/molbev/msm083
↑  Froese, R. & Pauly, D. (eds.) (2016). Species of Parahucho. FishBase. Version 2016-08.
馬斯特蘭德

| Marstrand |
| --- | --- |
Marstrand from above
Marstrand
坐标：57°53′09″N 11°34′51″E﻿ / ﻿57.885769°N 11.580886°E﻿ / 57.885769; 11.580886
Country: Sweden
Province: Bohuslän
County: Västra Götaland County
Municipality: Kungälv Municipality
面积
 • 总计: 0.88 平方公里（0.34 平方英里）
人口（31 December 2010）
 • 總計: 1,319人
 • 密度: 1,507人/平方公里（3,900人/平方英里）
时区: CET（UTC+1）
 • 夏时制: CEST（UTC+2）
馬斯特蘭德（Marstrand）是瑞典的一座城市。2010年，有人口1,319人。
參考資料

1 2  . Statistics Sweden. 14 December 2011  [10 January 2012]. （原始内容存档于2012-01-10） （瑞典语）.  （页面存档备份，存于）
外部連結

Marstrand （页面存档备份，存于） - From Kungälv Municipality official page
（瑞典文） article Marstrand （页面存档备份，存于） from Nordisk Familjebok (1912)
格特鲁德·鲍登维沙

格特鲁德·鲍登维沙（Gertrud Bodenwieser，1890年2月3日—1959年11月10日，出生於维也纳；逝世於悉尼），是一名舞蹈员、编舞者、舞蹈老师和表现派舞蹈的先驱。
生平

她是西奥多和玛丽亚·邦迪這對富裕犹太夫妇的女儿，以「格特鲁德·鲍登维沙」的化名开始她的舞蹈生涯，並在维也纳成名。鲍登维沙的芭蕾舞团风格是古典芭蕾，这种舞蹈受到觀众、评论家和青年学生欢迎。她的灵感癞子艾莎道拉·邓肯（Isadora Duncan）和露丝·圣·丹尼斯（Ruth St. Denis）的工作。她最成功的表演之一是‘妖机’，一种看起來像是一群舞者變成一台机器的特殊舞蹈表演。
格特鲁德·鲍登维沙被维也纳的音乐和行为艺术学院任命為教授。她在音乐厅的地下室建立她自己的舞蹈工作室。她的学生散居欧洲各處，形成‘鲍登维沙舞蹈团’。
她的舞蹈作品‘路西弗的面具’，描述陰謀、恐怖和憎恨是政治极权主义的化身，作品在不祥时期因具象体现而著名。
在第二次世界大战以前，格特鲁德·鲍登维沙在1938年和极少数学生一起逃到了哥伦比亚，在那里为了庆祝波哥大建市400周年，她進行了一場表演，觀眾足以塞滿一座斗牛竞技场。后来她移民到澳大利亚，在悉尼從事舞蹈教學。她培育出了澳大利亚最杰出的一些编舞及舞蹈员，其中包括阿妮塔·尔德勒(Anita Ardell)，基思·贝恩(Keith Bain)和玛格丽特·查普尔(Margaret Chapple)。
Emmy Towsey (Taussig)和Evelyn Ippen，鲍登维沙芭蕾舞团在悉尼， 澳大利亚1939.年
北埃斯特雷拉 (聖保羅州)

22°29′18″S 51°39′38″W﻿ / ﻿22.48833°S 51.66056°W﻿ / -22.48833; -51.66056
北埃斯特雷拉（葡萄牙語：），是巴西的城鎮，位於該國南部，由聖保羅州負責管轄，始建於1953年12月30日，面積263平方公里，海拔高度409米，2010年人口2,661，人口密度每平方公里10.11人。
王小军 (1969年)

名为王小军的其他人物，請見「」。
王小军（1969年4月—），男，汉族，中华人民共和国政治人物。曾任中国运载火箭技术研究院院长兼党委副书记、第十四届全国政协委员。
2024年1月29日被撤销全国政协委员资格，此前中国运载火箭技术研究院的院长一职已改由中国航天科技集团总经理张忠阳兼任。
参考资料

↑  . 新华网.   [2023-01-24]. （原始内容存档于2023-02-02）.
↑  . 北京青年报-政知见. 2024-01-29  [2024-01-29]. （原始内容存档于2024-01-29）.
柯里-霍华德同构

以函數式編程寫作的：在Coq軟件中自然數加法交換性的證明。nat_ind 代表數學归纳，eq_ind 代替等於，f_equal 代表在等式兩邊取同樣的函數。 前面的定理參照顯示 m = m + 0和S（m + y）= m + S y。
柯里-霍華德对应（英語：）是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和数学运算之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德（William Alvin Howard）独立发现的。
對應的起源、范围和結論

对应可以在两个层面上看到，首先是类比层次，它声称對一个函数计算出的值的类型的断言可类比于一个逻辑定理，计算这个值的程序可类比于这个定理的证明。在理论计算机科学中，这是连接λ演算和类型论的毗邻领域的一个重要的底层原理。它被经常以下列形式陈述为“证明是程序”。一个可选择的形式化为“命题为类型”。其次，更加正式的，它指定了在两个数学领域之间的同构，就是以一种特定方式形式化的自然演绎和简单类型λ演算之间是双射，首先是证明和项，其次是证明归约步骤和beta归约。
有多种方式考虑柯里-霍華德对应。在一个方向上，它工作于“把证明编译为程序”级别上。这裡的“证明”最初被限定为在构造性逻辑中—典型的是直觉逻辑系统中的证明。而“程序”是在常规的函数式编程的意义上的；从语法的观点上看，这种程序是用某种λ演算表达的。所以柯里-霍華德同构的具体实现是详细研究如何把来自直觉逻辑的证明写成λ项。（这是霍華德的贡献；柯里贡献了组合子，它是相对于是高级语言的λ演算是能写所有东西的机器语言）。最近，同样处理经典逻辑的柯里-霍華德对应的扩展可被公式化了，通过对经典有效规则比如双重否定除去和皮尔士定律关联上明确的用续体比如call/cc（英语：）处理的一类项。
还有一个相反的方向，对一个程序的正确性关联上“证明提取”的可能性。这在非常丰富的类型论环境中是可行的。实际上理论家对推进非常丰富类型的函数式编程语言的开发的动机，已经部分地混合了希望带给柯里-霍華德对应更加显著的地位的因素。
类型

依据λ演算，我们将使用λx.E来指示带有形式参数x和函数体E的函数。在应用于参数比如a的时候，这个函数生成E，并带有x的所有自由出现都被替换为a。有效的λ演算表达式有如下形式之一：
v（这裡的v是个变量）
λv.E（这裡的v是个变量，而E是个λ演算表达式）
(E F)（这裡的E和F是λ演算表达式）
通常我们将缩写(（A B）C)为(A B C)，缩写λa.λb.E为λab.E。一个表达式被称为是“闭合的”，如果它不包含自由变量。
类型 > 類型確定規則

类型可以依赖于类型变量，它被指示为小写的希腊字母α, β等等。在我们概念中类型变量是被隐含的全称量化的，就是说，如果一个值有包括类型变量的一个类型，则它必须由这个类型变量的所有可能实例组成。我们可以定义任意表达式的类型为如下：
一个变量比如x可以有任意类型。
如果变量x有类型α，而表达式E有类型β，则λx.E有指示为α→β的类型；就是说，它是取类型α的值，并映射到类型β的值。
在表达式(E F)中，如果F有类型α，则E必须有类型α→β（就是说它必须是期望类型α的参数的函数）并且这个表达式有类型β。
例如，考虑函数K = λa.λb.a。假定a有类型α而b有类型β。则λb.a有类型
β→α，而λa.λb.a有类型α→(β→α)。我们接受→是右结合的约定，所以这个类型也可以写为α→β→α。这意味着K函数接受类型α的参数并返回一个函数，它接受类型β的参数并返回类型α的值。
类似的，考虑函数B = λa.λb.λc.(a (b c))。假定c有类型γ，则b必须有形如γ→β的某种类型，表达式(b c)有类型β。a必须有形如β→α的某种类型，表达式(a (b c))有类型α。那么λc.(a (b c))有类型γ→α；λb.λc.(a (b c))有类型(γ→β)→γ→α，而λa.λb.λc.(a (b c))有类型(β→α)→(γ→β)→γ→α。你可以把这解释为意味着B函数接受类型(β→α)的参数和类型(γ→β)的参数并返回一个函数，它接受类型γ的参数并返回类型α的结果。
类型 > 类型居留问题

很明显λ-表达式可以有非常复杂的类型。你可能要问是否有带有给定类型的λ-表达式。找到带有特定类型的λ-表达式的问题叫做类型居留问题。
答案是非常引人注目的：有带有特定类型的闭合λ-表达式，当且仅当这个类型对应于一个逻辑定理，在这裡的→符号再次解释为意味着逻辑蕴涵的时候。
例如，考虑恒等函数λx.x，它接受类型ξ的参数并返回类型ξ的结果，所以有类型ξ→ξ。ξ→ξ当然是逻辑定理：给定一个公式ξ，你可以结论出ξ。
K函数的类型α→β→α也是一个定理。如果已知α为真，则你可以结论出如果β为真就能推出α。这有时也叫做重复规则。B的类型是 (β→α)→(γ→β)→γ→α。你可类似的把它解释为逻辑重言式；如果已知(β→α)为真，则如果已知(γ→β)为真，你就能推出γ蕴涵α。
在另一方面，考虑α→β，它不是定理。明显的没有这种类型的λ-项；它必定是接受类型α的参数并返回某个完全无关的和未约束类型的结果的函数。这是不可能的，因为你不能从这种函数里得到什么东西，除非把它放到其他什么地方之中。
尽管有类型β→(α→α)的函数（比如，λb.λa.a，它接受一个参数b，忽略参数，并返回恒等函数），却没有类型(α→α)→β的函数，如果存在的话，它会是转换恒等函数到任意值的函数。
类型 > 直觉逻辑

尽管所有居留类型对应于逻辑定理为真，逆命题却不为真。即使我们限制我们的尝试到只包含→运算的逻辑公式，所谓的逻辑的蕴涵片段，不是所有经典有效的逻辑公式是居留类型。例如，类型((α→β)→α)→α是非居留的，尽管叫做皮尔士定律的对应逻辑公式是重言式。
直觉逻辑是比经典逻辑弱的系统。经典逻辑把自身关注于在抽象的、柏拉图主义意义上为真的公式，而直觉逻辑只在可以为它构造一个证明的时候认为公式为真。公式α ∨ ¬α示例了这种区别；它是经典逻辑的一个定理而不是直觉逻辑的定理。尽管它是经典的真的，在直觉逻辑中这个公式断言了我们要么证明α要么证明¬α。因为我们不是总能做到这些事情之一，它不是直觉逻辑的一个定理。
在居留类型和有效逻辑公式之间的对应完全是双向的，如果我们限制我们的注意力到直觉逻辑的蕴涵片段（这也叫做希尔伯特代数）。
希尔伯特演繹系統和組合子邏輯的對應

形式上刻画直觉逻辑的一个简单方式是希尔伯特演繹系統。它有两个公理模式。所有形式为
的公式都是公理，所有形式为
的公式都是公理。
唯一的演绎规则是肯定前件，它声称如果我们已经证明了两个定理，一个有形式α→β而另一个有形式α，我们可以结论出β也是定理。以这种方式推导出来的公式的集合正好是直觉逻辑的集合。特别的是，皮爾士定律不能以这种方式演绎。（对皮爾士定律不能以这种方式演绎的证明请参见海廷代数条目）。
如果我们增加皮爾士定律为第三个公理模式，这个系统就有能力证明在经典逻辑的蕴涵片段中的所有定理。
考虑λ-表达式的下列两个函数：
可以证明任何函数都可以通过适当的K和S相互应用来建立。（有关证明请参见组合子逻辑）。例如，上面定义的函数B等价于(S(K S)K)。如果一个函数比如B，可以表达为S和K的复合，则这个表达式可以直接转换成类型B的一个证明，它被解释为逻辑公式，是直觉逻辑的一个定理。本质上，K的外观对应于第一个公理模式的使用，S的外观对应于第二个公理模式的使用，而函数应用对应于肯定前件演绎规则的使用。
第一个公理模式是α→β→α，并且它精确的是K函数的类型；类似的第二个公理模式(α→β→γ)→(α→β)→α→γ，是S函数的类型。肯定前件声称如果我们有两个表达式，一个类型是α→β（就是说，接受类型α的值并返回类型β的值）而另一个类型是α（就是说，类型α的值），则我们应当能够找到类型β的值；明显的，我们可以通过应用这个函数到这个值之上来得到；结果会有类型β。
| 希爾伯特式直覺蘊含邏輯 | 簡單類型的組合子邏輯 |
| --- | --- |
 {\frac {}{\Gamma _{1},\alpha ,\Gamma _{2}\vdash \alpha }}Assum:  {\frac {}{\Gamma _{1},x:\alpha ,\Gamma _{2}\vdash x:\alpha }}
 {\frac {}{\Gamma \vdash \alpha \rightarrow (\beta \rightarrow \alpha )}}Ax_{1}:  {\frac {}{\Gamma \vdash K:\alpha \rightarrow (\beta \rightarrow \alpha )}}
 {\frac {}{\Gamma \vdash (\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}Ax_{2}:  {\frac {}{\Gamma \vdash S:(\alpha \!\rightarrow \!(\beta \!\rightarrow \!\gamma ))\!\rightarrow \!((\alpha \!\rightarrow \!\beta )\!\rightarrow \!(\alpha \!\rightarrow \!\gamma ))}}
 {\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}{\textit {Modus~Ponens}}:  {\frac {\Gamma \vdash E_{1}:\alpha \rightarrow \beta \qquad \Gamma \vdash E_{2}:\alpha }{\Gamma \vdash E_{1}\;E_{2}:\beta }}
希尔伯特演繹系統和組合子邏輯的對應 > 证明α→α

作为一个简单的例子，我们将构造定理α→α的证明。这是恒等函数I = λx.x的类型。函数((S K)K)等价于恒等函数。作为对证明的描述，它声称了我们需要首先应用S到K。我们做如下：
如果我们在S中设γ = α，我们得到：
因为这个公式的前件(α→β→α)是一个已知定理，并且实际上正好是K，我们可以应用肯定前件并推导出后件：
这是函数(S K)的类型。现在我们需要应用这个函数到K。我们再次操纵公式使得前件看起来像K，这次我们替代β为(β→α):
我们再次应用肯定前件来推出后件：
我们完成了。
一般的说，这个过程是只要程序包含形如(P Q)的应用，我们应当首先证明对应于P和Q的类型的定理。因为P要被应用于Q，对于某种α和β，P的类型必定有形式α→β而Q的类型必定有形式α。我们可以通过肯定前件规则推出β。
希尔伯特演繹系統和組合子邏輯的對應 > 证明 (β→α)→(γ→β)→γ→α

作为一个更加复杂的例子，我们看对应于函数B的定理的证明。B的类型是(β→α)→(γ→β)→γ→α。B等价于(S(K S)K)。这是对证明定理(β→α)→(γ→β)→γ→α的指引。
首先我们需要构造(K S)。我要使K公理的前件看起来像S公理，通过设置α等于(α→β→γ)→(α→β)→α→γ，和β等于δ:
因为前件正好是S，我们可以推出后件：
这是对应于(K S)的定理。现在我们要应用S到这个表达式。取得S
我们设置α = δ，β = (α→β→γ)和γ = ((α→β)→α→γ)，生成
我们可以接着推出后件：
这是类型(S(K S))的公式。这个定理的一个特殊情况有δ = (β→γ):
我们需要应用最后这个公式到K。我们再次特殊化K，这次是替代α为(β→γ)，替代β为α:
这同于前者公式的前件，所以我们推出后件：
交换变量α和γ的名字得到
这就是我们要证明的。
自然演繹和lambda演算的對應

在下表第一列中的推导规则定义了直觉蕴涵自然演绎（为蕴涵连结词准备一个介入和一个除去规则）的标准系统。在第二列中给出 \lambda -演算的标准类型指派（赋值）系统。
| 直觉蕴涵自然演绎 | lambda演算类型指派规则 |
| --- | --- |
 {{} \over \Gamma ,\alpha \vdash \alpha }\quad {\rm {(Ax)}}:  {{} \over \Gamma ,x{:}\alpha \vdash x:\alpha }\quad {\rm {(Ax)}}
 {\Gamma ,\alpha \vdash \beta  \over \Gamma \vdash \alpha \rightarrow \beta }\quad (\rightarrow {\rm {I}}):  {\Gamma ,x{:}\alpha \vdash E:\beta  \over \Gamma \vdash \lambda x.E:\alpha \rightarrow \beta }\quad (\rightarrow {\rm {I}})
 {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha  \over \Gamma \vdash \beta }\quad (\rightarrow {\rm {E}}):  {\Gamma \vdash E:\alpha \rightarrow \beta \qquad \Gamma \vdash F:\alpha  \over \Gamma \vdash (E\ F):\beta }\quad (\rightarrow {\rm {E}})
相继式演算

希尔伯特式证明是很难构造的。证明逻辑定理的更加直觉的方式是根岑的相继式演算。相继式演算以同希尔伯特式证明对应于组合子表达式一样的方式对应于λ-表达式程序。
直觉逻辑的蕴涵片段的相继式演算规则是：
Γ表示上下文，它是假设的集合。 \Gamma \vdash a指示假定上下文Γ我们可以证明a。逻辑定理完全由其证明不需要假设的那些公式t组成的；就是说，t是一个定理，当且仅当我们可以证明 \vdash t。详情请参见相继式演算。
在相继式演算中的证明是树，它的根是我们要证明的定理，而它的叶子是公理模式实例；每个内部节点必须标记为要么Right →要么Left →，并且必须包含依据指定规则从子节点推出的一个公式。
相继式演算证明紧密的对应于λ-演算表达式。断言 \Gamma \vdash a可以被解释为意味着，给定带有在Γ中列出类型的值，我们可以制造带有类型a的一个值。公理对应于带有新的无约束的类型的新变量介入。
Right →规则对应于函数抽象：
什么时候我们能结论出某个程序Γ包含类型α→β的函数?在Γ加上类型α的一个值的时候，包含了足够的机械来允许我们制造类型β的一个值。
Left →规则对应于函数应用：
如果我们可以制造类型α的一个值，并且如果给出类型β的一个值，我们还可以制造类型γ的一个值，则类型α→β的一个函数将允许我们制造类型γ的一个值：首先我们可以制造α，接着应用α→β函数于它，并接着使用结果的β值来制造类型γ的一个值。
相继式演算 > 例子

例如，(β→α)→(γ→β)→γ→α的相继式演算如下：
(β→α)→(γ→β)→γ→α的证明告诉我们如何制造带有这个类型的一个λ-表达式。首先，介入分别带有类型α和β的变量a和b。Left →规则声称制造程序 (λb.a b)，它构造类型α的一个值。我们再次使用Left →来构造(λb.a (λg.b g))，它仍有类型α。
引用 > 開創性引用

Curry, Haskell, ,  20: 584–590, 1934 .
Curry, Haskell B.; Feys, Robert, , William Craig, Amsterdam: North-Holland, 1958 , with 2 sections by William Craig, see paragraph 9E.
De Bruijn, Nicolaas (1968), Automath, a language for mathematics, Department of Mathematics, Eindhoven University of Technology, TH-report 68-WSK-05. Reprinted in revised form, with two pages commentary, in: Automation and Reasoning, vol 2, Classical papers on computational logic 1967-1970, Springer Verlag, 1983, pp. 159-200.
Howard, William A., , Seldin, Jonathan P.; Hindley, J. Roger  (编), , Boston, MA: Academic Press: 479–490, 1980年9月 [1969], ISBN 978-0-12-349050-6  (original manuscript from 1969).
引用 > 對應的擴展

Griffin, Timothy G., , : 47–57, 1990 .
Parigot, Michel, , , Lecture Notes in Computer Science 624, Berlin, New York: Springer-Verlag: 190–201, 1992, ISBN 978-3-540-55727-2 .
Herbelin, Hugo, , Pacholski, Leszek; Tiuryn, Jerzy  (编), , Lecture Notes in Computer Science 933, Springer-Verlag: 61–75, 1995, ISBN 978-3-540-60017-6 .
Gabbay, Dov; de Queiroz, Ruy, ,  57: 1319–1365, 1992 . (Full version of the paper presented at Logic Colloquium '90, Helsinki. Abstract in JSL 56(3):1139-1140, 1991.)
de Queiroz, Ruy; Gabbay, Dov, , Dekker, Paul; Stokhof, Martin  (编), , ILLC/Department of Philosophy, University of Amsterdam: 547–565, 1994, ISBN 9074795072 .
de Queiroz, Ruy; Gabbay, Dov, ,  3(2–3): 243–290, 1995 . (Full version of a paper presented at Logic Colloquium '91, Uppsala. Abstract in JSL 58(2):753-754, 1993.)
de Queiroz, Ruy; Gabbay, Dov, , de Rijke, Maarten  (编), , Applied Logic Series 7, Springer-Verlag: 61–91, 1997, ISBN 978-0-7923-4711-8 .
de Oliveira, Anjolina; de Queiroz, Ruy, ,  7(2), Oxford Univ Press: 173–215, 1999 . (Full version of a paper presented at 2nd WoLLIC'95, Recife. Abstract in Journal of the Interest Group in Pure and Applied Logics 4(2):330-332, 1996.)
引用 > 綜合性論文

De Bruijn, Nicolaas Govert,  (PDF), Groote, Philippe de  (编), , Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 27–54,   [2008-08-28], ISBN 978-2-87209-363-2, （原始内容存档 (PDF)于2021-03-06） , the contribution of de Bruijn by himself.
Geuvers, Herman, , Groote, Philippe de  (编), , Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 139–191, ISBN 978-2-87209-363-2 , contains a synthetic introduction to the Curry-Howard correspondence.
Gallier, Jean H.,  (PDF), Groote, Philippe de  (编), , Cahiers du Centre de logique (Université catholique de Louvain) 8, Academia-Bruyland: 55–138, ISBN 978-2-87209-363-2 , contains a synthetic introduction to the Curry-Howard correspondence.
引用 > 書籍

De Groote, Philippe (编), , Cahiers du Centre de Logique (Université catholique de Louvain) 8, Academia-Bruylant, 1995, ISBN 978-2-87209-363-2 , reproduces the seminal papers of Curry-Feys and Howard, a paper by de Bruijn and a few other papers.
Sörensen, Morten Heine; Urzyczyn, Paweł, , Studies in Logic and the Foundations of Mathematics 149, Elsevier Science, 2006 [1998], ISBN 978-0-44452-077-7 , notes on proof theory and type theory, that includes a presentation of the Curry-Howard correspondence, with a focus on the formulae-as-types correspondence
Girard, Jean-Yves (1987-90). Proof and Types （页面存档备份，存于）. Translated by and with appendices by Lafont, Yves and Taylor, Paul. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0-521-37181-3, notes on proof theory with a presentation of the Curry-Howard correspondence.
Thompson, Simon (1991). Type Theory and Functional Programming （页面存档备份，存于） Addison-Wesley. ISBN 0-201-41667-0.
格特鲁德·蒙盖拉

| 格特鲁德·蒙盖拉 Gertrude Ibengwe Mongella |
| --- | --- |
摄于2005年

第1任泛非议会主席
任期 2004年5月—2009年5月
继任: 伊德里斯·恩德莱·穆萨（英语：）
选区: 坦桑尼亚
 
个人资料
性别: 女
出生: Gertrude Makanza  (1945-09-13) 1945年9月13日（79歲）  坦噶尼喀烏凱雷豐島
国籍:  坦桑尼亚
政党: 坦桑尼亚革命党
配偶: Silvin
儿女: 3人
居住地: 达累斯萨拉姆
母校: 达累斯萨拉姆大学
获奖: 达美环球理解奖（2005年）
格特鲁德·蒙盖拉（斯瓦希里語：，1945年9月13日—），中文通称“蒙盖拉夫人”，又译“戈特鲁特·蒙盖拉”、“杰楚德·蒙盖拉”，是坦桑尼亚的一名女性政治人物、教育家和社会活动家，曾任1995年联合国第四次世界妇女大会秘书长（提高妇女地位司司长），也是泛非议会首任主席。
生平

格特鲁德·蒙盖拉旧姓马坎扎，1945年9月13日出生于維多利亞湖南部烏凱雷豐島Murutunguru村一个农民家庭，1970年毕业于达累斯萨拉姆大学（原东非大学（英语：）），获文学学士学位，此后在达累斯萨拉姆师范学院担任教师兼督导，1974年起担任达累斯萨拉姆教育学院课程设计师，其间于1977年当选为坦桑尼亚革命党中央执行委员会委员，是当时坦桑尼亚最高决策层中的三位女性之一，1978年起担任督学。
蒙盖拉夫人1982年至1985年担任坦桑尼亚总理府妇女事务部部长，1985年起担任坦桑尼亚土地、自然资源和旅游部部长，1987年至1990年担任总统办公室不管部长，1989年被任命为聯合國婦女地位委員會坦桑尼亚代表，1991年被任命为坦桑尼亚驻印度高級專員（大使级），1992年12月被联合国秘书长加利任命为第四次世界妇女大会秘书长。1995年北京世妇会取得成功后，蒙盖拉夫人因对世妇会的突出贡献而被称为“北京妈妈”（Mama Beijing），1996年至1997年担任联合国秘书长妇女问题特使。
2004年3月18日，蒙盖拉夫人在泛非议会成立大会上以唯一候选人的身份当选为泛非议会首任主席，2005年获得佐治亚大学颁发的达美环球理解奖。
参考资料

↑  . 新华社. 2020-10-04  [2021-09-11]. （原始内容存档于2021-09-11）.
↑  . 人民日报. 1995-09-05: 1.
↑  . 北京市妇女联合会. 2015-07-28  [2021-09-11]. （原始内容存档于2021-09-11）.
↑  . 人民日报. 1995-03-04: 7.
↑  刘伯红; 吴华. . 百科知识 (中国大百科全书出版社). 1995, (09): 43. ISSN 1002-9567.
↑  . 联合国.   [2021-09-11]. （原始内容存档于2020-04-06）. 1993年—1995年：格特鲁德·蒙盖拉女士（坦桑尼亚联合共和国），担任助理秘书长及第四次妇女问题世界会议秘书长职务，同时指导提高妇女地位司的工作
1 2 3  闻平. . 西亚非洲 (中国社会科学院西亚非洲研究所). 1995, (05): 55–57. ISSN 1002-7122.
1 2  . 达累斯萨拉姆大学.   [2021-09-12]. （原始内容存档于2021-09-11）.
↑  . Africa Renewal. 2020-10-30  [2021-09-12]. （原始内容存档于2020-12-12）.
↑  . 人民日报. 2004-09-22  [2021-09-12]. （原始内容存档于2021-09-11）.
↑  . 新华网. 2004-03-18  [2021-09-12]. （原始内容存档于2021-09-11）.
南大仙林校区站

南大仙林校区站是南京地铁2号线上一座车站，位于南京市栖霞区仙林大道南侧，为高架二层鱼腹式岛式车站。
车站结构 > 站台

本站设2个岛式站台，有一条电动扶梯，一条上行电动扶梯和一条垂直电梯连接楼下站厅和楼上站台。其中从市区方向驶来的列车B2B号车门正好停在下行电动扶梯旁，故常有乘客在列车停靠前行走至此门等待下车以节省时间。站厅东侧有商铺。
出口

本站设东西两个出口，由东出口向北过地下通道通往南京大学仙林校区，西出口向南通往南京大学教职工公寓南大和园。
车站周边

南京大学仙林校区
南大和园
九乡河生态公园
接驳交通 > 公交车

| 南大仙林校区（近4出口）> 编号 | 南大仙林校区（近4出口）> 路线 | 南大仙林校区（近4出口）> 路线 | 南大仙林校区（近4出口）> 路线 | 南大仙林校区（近4出口）> 备注 |
| --- | --- | --- | --- | --- |
| B3 | 南大仙林校区 | ↻ | 南大仙林校区 |  |
| D1 | 元化路 | ⇆ | 中保村 |  |
| Y34 | 经天路地铁站南 | → | 南京站·南广场东 |  |
| Y34 | 经天路地铁站西 | ← | 南京站·南广场东 |  |
| 178 | 尤山路·摄山星城 | ⇆ | 仙林中心站 |  |
| 321 | 元化路 | ⇆ | 仙居雅苑 |  |
| 322 | 元化路 | → | 尧化门总站东 |  |
| 322 | 元化路 | ← | 尧化门总站 |  |
| 325 | 羊山北路总站 | ⇆ | 西岗果牧场 |  |
| 342 | 经天路地铁站南 | → | 石埠桥总站 | 合并原 326 |
| 342 | 经天路地铁站西 | ← | 石埠桥总站 | 合并原 326 |
| 743 | 东山总站 | → | 经天路地铁站西 | 定时班车；原 东上线 |
| 743 | 东山总站 | ← | 经天路地铁站南 | 定时班车；原 东上线 |
图集

| 0 | 1 | 2 |
| --- | --- | --- |
|  | 出站闸机 |  |
王小佳

王小佳（1956年3月17日—），男，四川南溪人，中国园艺学家，曾任西南农业大学、西南大学校长。
生平

1990年毕业于西南农业大学，获蔬菜专业博士学位，后留校任教。1994年至1995年间公派瑞典隆德大学进修。回国后曾出任西南农业大学校长。2005年起任西南大学校长。
参考资料

↑  . 中华人民共和国教育部.   [2021-07-11]. （原始内容存档于2021-07-15）.
中醫「症」解

| 中醫「症」解 Knowing Chinese Medicine |
| --- | --- |
类型: 資訊節目
导演: 秋璇
主持: 陳子豐、羅沛琪、王頌茵、沈殷怡
制作国家／地区:  香港
语言: 粵語
集数: 13
每集长度: 30分鐘（連廣告）
制作
监制: R-NO
编审: 秋璇
拍攝地點:  香港
制作公司: 香港電視娛樂
播出 
首播频道: ViuTV
图像制式: 高清電視 1080i
声音制式: 立體聲
播出国家／地区:  香港
播出日期: 2019年5月11日—8月3日
播出时间: 逢星期六 20:00－20:30
 

官方网站
《中醫「症」解》（Knowing Chinese Medicine）是香港電視娛樂製作的健康資訊節目，主持為陳子豐、羅沛琪、王頌茵及沈殷怡，由2019年5月11日至8月3日逢星期六20:00-20:30於ViuTV播出，由香港賽馬會「擁抱健康」中醫計劃贊助。節目中以中醫角度介紹多種治未病方法，幫助所有年齡層的朋友，達到未病防病、已病防變的目標。
每集一覽

| 0 | 1 | 2 |
| --- | --- | --- |
| 集數 | 播映日期 | 主題 |
| 1 | 5月11日 | 腸易激綜合症 |
| 2 | 5月18日 | 彈弓指 |
| 3 | 5月25日 | 中風 |
| 4 | 6月1日 | 更年期綜合徵 |
| 5 | 6月8日 | 不孕症 |
| 6 | 6月15日 | 咳嗽 |
| 7 | 6月22日 | 癌症 |
| 8 | 6月29日 | 兒童生長發育遲緩 |
| 9 | 7月6日 | 眼中風 |
| 10 | 7月13日 | 高血壓 |
| 11 | 7月20日 | 鼻敏感 |
| 12 | 7月27日 | 抑鬱症 |
| 13 | 8月3日 | 體質養生 |
參考資料

↑  .   [2019-06-14]. （原始内容存档于2020-05-26）.
↑  《中醫「症」解》解構都巿病　簡易花茶有效改善胃痛關節炎及中風 （页面存档备份，存于），香港01，2019-06-01
↑  密密篤手機 患彈弓指伸唔直，晴報，2018-06-29
外部連結

ViuTV：中醫「症」解
丹东边境经济合作区

丹东边境经济合作区，简称“合作区”，是辽宁省丹东市的国家级开发区。辖区沿鸭绿江右岸黄金坪岛对面：北起金河大街、安民河，南至台南路，东至鸭绿江，西至黄海大道。面积6.3km2，10万人。
行政区划

下辖
浪头镇
安民镇（已划归高新区）
江海街道
历史

1992年7月7日国务院批准设立。
沃斯克列先斯克

55°19′N 38°42′E﻿ / ﻿55.317°N 38.700°E﻿ / 55.317; 38.700
| 沃斯克列先斯克 Воскресенск |
| --- | --- |
城鎮

   旗幟 圖章
沃斯克列先斯克沃斯克列先斯克位于俄罗斯的位置
坐标：55°19′N 38°41′E﻿ / ﻿55.32°N 38.68°E﻿ / 55.32; 38.68
国家:  俄羅斯
州: 莫斯科州
区: 沃斯克列先斯克区
建立: 1862
设市: 1938
面积
 • 总计: 24.5 平方公里（9.5 平方英里）
海拔: 120 公尺（390 英尺）
人口（2010）
 • 總計: 91,464人
 • 排名: 第180位
时区: 莫斯科时间（UTC+3）
網站: 
沃斯克列先斯克（俄语：）是俄羅斯莫斯科州的一個城市，隶属于沃斯克列先斯克區。2010年人口为91464。
历史

沃斯克列先斯克建立于1862年，后于1938年设市。
地理

沃斯克列先斯克地处莫斯科東南約88公里處莫斯科河畔。在俄罗斯行政区划中，该市是沃斯克列先斯克區的行政中心。
地理 > 气候

沃斯克列先斯克属于温带内陆气候（俄语：）。冬季较冷，1月的平均气温为-9°C至-10°C，夏季温度适中，平均气温为18°C至19°C。四季分明，其中冬季约为150天，夏季约为90天，春秋两季各持续约2个月。
经济

经济有轻工业、化工、建筑材料和农业。
參考文獻

1 2  . Moscow: Большая Российская Энциклопедия. 2003: 93. ISBN 5-7107-7399-9.
1 2  俄羅斯聯邦國家統計局.  [2010 All-Russian Population Census, vol. 1]. Всероссийская перепись населения 2010 года [2010 All-Russia Population Census]. 俄羅斯聯邦國家統計局. 2011 （俄语）.
↑  В. А. Дударев, Н. А. Елисеева; Президиум Верховного Совета СССР. . 苏联. 1980-01-01: 172.  引文使用过时参数coauthors (帮助)
↑  Климат: Воскресенск （页面存档备份，存于） // climate-data.org
柯西乘积

在数学上，以法国数学家奧古斯丁·路易·柯西命名的柯西乘积，是指两组数列 a_{n},b_{n}的离散卷积。
该数列乘积被认为是自然数 R[\mathbb {N} ]的半群环的元素。
级数

一个特别重要的例子是考虑两个严格的形式级数（不需要收敛） a_{n},b_{n}：
一般地，对于实数和复数，柯西乘积定义为如下的离散卷积形式：
“形式”是指我们对级数运算时不考虑是否收敛，参见形式幂级数。
人们希望，通过对两组级数做实际卷积的有限和的类推，得到无穷级数
等于如下乘积：
就如同两个数列的和是有限范围一样做乘法。
在充分良态的情况下，上述式子成立。而更重要的一点，尽管这两个无穷级数可能不收敛，它们的柯西乘积仍可能存在。
示例 > 有穷级数

对于 i>n、 i>m，有 x_{i}=0， y_{i}=0 即为有穷级数，则 \sum x和  \sum y 柯西乘积可以展开为 (x_{0}+\cdots +x_{n})(y_{0}+\cdots +y_{m})，因此可以直接计算乘积。
示例 > 无穷级数

对某些 a,b\in \mathbb {R} ，构造 x_{n}=a^{n}/n!\,和 y_{n}=b^{n}/n!\,，由定义和二项式展开可知：
形式上，  \exp(a)=\sum x， \exp(b)=\sum y，我们已表明 \exp(a+b)=\sum C(x,y)。由于该两个绝对收敛数列的柯西乘积等于两个数列极限的乘积，（见下面的证明），因此我们就可证明这个表达式对于  a,b\in \mathbb {R} 有 \exp(a+b)=\exp(a)\exp(b)
另外一个例子，令 x(n)=1（ n\in \mathbb {N} ），则  C(x,x)(n)=n+1对所有 n\in \mathbb {N} 成立，则柯西乘积  \sum C(x,x)=(1,1+2,1+2+3,1+2+3+4,\dots ) ，该乘积不收敛。
收敛和梅尔滕斯定理

令x, y为实数数列，弗兰兹·梅尔滕斯（Franz Mertens）提出，如果级数 \sum y收敛到Y，且级数 \sum x绝对收敛到X，则他们的柯西乘积  \sum C(x,y)收敛到XY。
对于两个级数为条件收敛时，结论未必成立。如下反例所示：
收敛和梅尔滕斯定理 > 例子

考虑下述两交错级数：
它们都是收敛的（其绝对值构成的级数因比较审敛法和调和级数的发散性而发散）。其柯西乘积的项由下式给出：
其中整数 n ≥ 0。因为对于所有 k ∈ {0, 1, ..., n} 我们都有不等式 k + 1 ≤ n + 1 及 n – k + 1 ≤ n + 1，故对分母中的根式有 √(k + 1)(n − k + 1) ≤ n +1。因此，由于共有 n + 1 个被加项，故对于所有的整数 n ≥ 0有
因此，cn 在 n → ∞ 时并不趋于 0，级数 ∑ cn 发散（项测试）。