RemainderFn |
appearance as argument number 1 |
(documentation RemainderFn ChineseLanguage "(RemainderFn ?NUMBER ?DIVISOR)是数字 ?NUMBER 除以数字 ?DIVISOR 的余数,商数的正负值与 ?DIVISOR 相同。") | chinese_format.kif 2267-2268 | |
(documentation RemainderFn EnglishLanguage "(RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR.") | Merge.kif 5101-5103 | |
(documentation RemainderFn JapaneseLanguage "(RemainderFn ?NUMBER ?DIVISOR) は、数値?NUMBER の残りを数値?DIVISORで割った値である。結果の符号は?DIVISOR と同じである。") | japanese_format.kif 932-933 | |
(domain RemainderFn 1 Integer) | Merge.kif 5097-5097 | The number 1 argument of remainder is an instance of integer |
(domain RemainderFn 2 Integer) | Merge.kif 5098-5098 | The number 2 argument of remainder is an instance of integer |
(instance RemainderFn BinaryFunction) | Merge.kif 5094-5094 | Remainder is an instance of binary function |
(instance RemainderFn PartialValuedRelation) | Merge.kif 5096-5096 | Remainder is an instance of partial valued relation |
(range RemainderFn Integer) | Merge.kif 5099-5099 | The range of remainder is an instance of integer |
appearance as argument number 2 |
(format ChineseLanguage RemainderFn "%1 模除 %2") | chinese_format.kif 722-722 | |
(format EnglishLanguage RemainderFn "%1 mod %2") | english_format.kif 724-724 | |
(format FrenchLanguage RemainderFn "%1 reste %2") | french_format.kif 434-434 | |
(format ItalianLanguage RemainderFn "%1 mod %2") | relations-it.txt 252-252 | |
(format JapaneseLanguage RemainderFn "%1 を %2 で割った剰余数") | japanese_format.kif 2151-2151 | |
(format PortugueseLanguage RemainderFn "%1 mod %2") | portuguese_format.kif 386-386 | |
(format cz RemainderFn "%1 mod %2") | relations-cz.txt 446-446 | |
(format de RemainderFn "%1 betrag %2") | relations-de.txt 935-935 | |
(format hi RemainderFn "%1 aura %2 kaa sheshhaphala") | relations-hindi.txt 289-289 | |
(format ro RemainderFn "%1 mod%t{modulo} %2") | relations-ro.kif 456-456 | |
(format sv RemainderFn "%1 modulo %2") | relations-sv.txt 496-496 | |
(termFormat ChineseLanguage RemainderFn "余函数") | chinese_format.kif 723-723 | |
(termFormat ChineseLanguage RemainderFn "剩余") | domainEnglishFormat.kif 49444-49444 | |
(termFormat ChineseTraditionalLanguage RemainderFn "剩餘") | domainEnglishFormat.kif 49443-49443 | |
(termFormat EnglishLanguage RemainderFn "remainder") | domainEnglishFormat.kif 49442-49442 |
antecedent |
(=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER 0)) (not (equal ?NUMBER1 0)) (not (equal ?NUMBER2 0))) (equal (SignumFn ?NUMBER2) (SignumFn ?NUMBER))) |
Merge.kif 5131-5143 |
|
(=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5105-5116 |
|
consequent |
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4862-4873 |
|
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0))))))) |
Merge.kif 4875-4889 |
|
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 4947-4957 |
|
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0))))))) |
Merge.kif 4959-4973 |
|
(=> (and (instance ?LEAP LeapYear) (instance ?LEAP (YearFn ?NUMBER))) (or (and (equal (RemainderFn ?NUMBER 4) 0) (not (equal (RemainderFn ?NUMBER 100) 0))) (equal (RemainderFn ?NUMBER 400) 0))) |
Merge.kif 9037-9045 |
|
(=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5118-5129 |
|
(=> (instance ?NUMBER EvenInteger) (equal (RemainderFn ?NUMBER 2) 0)) |
Merge.kif 5145-5148 |
|
(=> (instance ?NUMBER OddInteger) (equal (RemainderFn ?NUMBER 2) 1)) |
Merge.kif 5150-5153 |
|
(=> (instance ?PRIME PrimeNumber) (forall (?NUMBER) (=> (and (equal (RemainderFn ?PRIME ?NUMBER) 0) (not (equal ?NUMBER 0))) (or (equal ?NUMBER 1) (equal ?NUMBER ?PRIME))))) |
Merge.kif 5155-5166 |
|