| PositiveInteger(正整数) | |
| appearance as argument number 1 |
|
|
| (documentation PositiveInteger ChineseLanguage "这是一个大于零的 Integer。") | chinese_format.kif 1754-1754 | |
| (documentation PositiveInteger EnglishLanguage "An Integer that is greater than zero.") | Merge.kif 1905-1905 | |
| (subclass PositiveInteger NonnegativeInteger) | Merge.kif 1902-1902 | 正整数 是 非负整数 的 subclass |
| (subclass PositiveInteger PositiveRealNumber) | Merge.kif 1903-1903 | 正整数 是 正实数 的 subclass |
| appearance as argument number 2 |
|
|
| (termFormat ChineseLanguage PositiveInteger "正整数") | chinese_format.kif 872-872 | |
| (termFormat EnglishLanguage PositiveInteger "positive integer") | english_format.kif 951-951 |
| appearance as argument number 3 |
|
|
| antecedent |
|
|
| (=> (and (viewedItemList ?USER ?LIST) (instance ?ACCESSING1 AccessingWebPage) (instance ?ACCESSING2 AccessingWebPage) (agent ?ACCESSING1 ?USER) (agent ?ACCESSING2 ?USER) (instance ?INDEX1 PositiveInteger) (instance ?INDEX2 PositiveInteger) (equal (ListOrderFn ?LIST ?INDEX1) ?ACCESSING1) (equal (ListOrderFn ?LIST ?INDEX2) ?ACCESSING2) (greaterThan ?INDEX1 ?INDEX2)) (earlier (WhenFn ?ACCESSING2) (WhenFn ?ACCESSING1))) |
UXExperimentalTerms.kif 985-1003 |
|
| (=> (instance ?X PositiveInteger) (greaterThan ?X 0)) |
Merge.kif 1907-1909 |
|
| consequent |
|
|
| (<=> (and (equal ?LIST3 (ListConcatenateFn ?LIST1 ?LIST2)) (not (equal ?LIST1 NullList)) (not (equal ?LIST2 NullList))) (forall (?NUMBER1 ?NUMBER2) (=> (and (lessThanOrEqualTo ?NUMBER1 (ListLengthFn ?LIST1)) (lessThanOrEqualTo ?NUMBER2 (ListLengthFn ?LIST2)) (instance ?NUMBER1 PositiveInteger) (instance ?NUMBER2 PositiveInteger)) (and (equal (ListOrderFn ?LIST3 ?NUMBER1) (ListOrderFn ?LIST1 ?NUMBER1)) (equal (ListOrderFn ?LIST3 (AdditionFn (ListLengthFn ?LIST1) ?NUMBER2)) (ListOrderFn ?LIST2 ?NUMBER2)))))) |
Merge.kif 2972-2988 | 串列 equal List包含 另一个 串列 和 第三 串列 和 那个 另外 串列 不 equal 空列表 和 那个 第三 串列 不 equal 空列表 若且唯若 对所有 正整数 和 另一个 正整数 |
|
|
|