Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
| RemainderFn |
| appearance as argument number 1 |
|
| (instance RemainderFn BinaryFunction) | Merge.kif 5205-5205 | Remainder is an instance of binary function |
| (instance RemainderFn PartialValuedRelation) | Merge.kif 5207-5207 | Remainder is an instance of partial valued relation |
| (domain RemainderFn 1 Integer) | Merge.kif 5208-5208 | The number 1 argument of remainder is an instance of integer |
| (domain RemainderFn 2 Integer) | Merge.kif 5209-5209 | The number 2 argument of remainder is an instance of integer |
| (range RemainderFn Integer) | Merge.kif 5210-5210 | The range of remainder is an instance of integer |
| (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 5212-5214 | The range of remainder is an instance of integer |
| appearance as argument number 2 |
|
|
| antecedent |
|
|
| (=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) |
Merge.kif 5216-5227 | If equal X mod Y and Z and equal Y and 0, then equal (the largest integer less than or equal to X and Y and Y and Z) and X |
| (=> (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 5242-5254 | If equal X mod Y and Z, equal Z and 0, equal X and 0, and equal Y and 0, then equal the sign of Y and the sign of Z |
| consequent |
|
|
| (=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0)))) |
Merge.kif 4973-4984 | If equal the greatest common divisor of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Z mod Y and 0 |
| (=> (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 4986-5000 | If equal the greatest common divisor of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is greater than Y and W W is a member of (@ROW)equal W mod Z and 0 |
| (=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0)))) |
Merge.kif 5058-5068 | If equal the least common multiple of @ROW and Y and equal Y and 0, then For all Integer Z: if Z is a member of (@ROW), then equal Y mod Z and 0 |
| (=> (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 5070-5084 | If equal the least common multiple of @ROW and Y and equal Y and 0, then there doesn't exist Z such that Z is less than Y and W W is a member of (@ROW)equal Z mod W and 0 |
| (=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER)) |
Merge.kif 5229-5240 | If equal X and 0 and equal (the largest integer less than or equal to Y and X and X and Z) and Y, then equal Y mod X and Z |
| (=> (instance ?NUMBER EvenInteger) (equal (RemainderFn ?NUMBER 2) 0)) |
Merge.kif 5256-5259 | If X is an instance of even integer, then equal X mod 2 and 0 |
| (=> (instance ?NUMBER OddInteger) (equal (RemainderFn ?NUMBER 2) 1)) |
Merge.kif 5261-5264 | If X is an instance of odd integer, then equal X mod 2 and 1 |
| (=> (instance ?PRIME PrimeNumber) (forall (?NUMBER) (=> (and (equal (RemainderFn ?PRIME ?NUMBER) 0) (not (equal ?NUMBER 0))) (or (equal ?NUMBER 1) (equal ?NUMBER ?PRIME))))) |
Merge.kif 5266-5277 | If X is an instance of prime number, then For all Integer Y: if equal X mod Y and 0 and equal Y and 0, then equal Y and 1 or equal Y and X |
| (=> (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 9203-9211 | If X is an instance of leap year and X is an instance of the year Y, then equal Y mod 4 and 0 and equal Y mod 100 and 0 or equal Y mod 400 and 0 |
|