greatest common divisor fn (GreatestCommonDivisorFn)

(GreatestCommonDivisorFn number1 number2 ... number) returns the greatest common divisor of number1 through number.

Ontologie

SUMO / NUMERIC-FUNCTIONS

Class(es)

třída

inheritable relation

funkce

relace s proměnným počtem argumentů
is instance of

greatest common divisor fn

Související termín(y)

assignment fn least common multiple fn list fn contrary attribute disjoint decomposition disjoint relation exhaustive attribute exhaustive decomposition holds partition

Axiomy (2)

jestliže "greatest common divisor fn()" se rovná number,
potom pro všechny element platí: jestliže element je a member of "()", potom "element mod number" se rovná

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (forall
            (?ELEMENT)
            (=>
                  (inList
                        ?ELEMENT
                        (ListFn @ROW))
                  (equal
                        (RemainderFn ?ELEMENT ?NUMBER)
                        0))))

jestliže "greatest common divisor fn()" se rovná number,
potom neexistuje greater tak, že greater je větší než number a pro všechny element platí: jestliže element je a member of "()", potom "element mod greater" se rovná

(=>
      (equal
            (GreatestCommonDivisorFn @ROW)
            ?NUMBER)
      (not
            (exists
                  (?GREATER)
                  (and
                        (greaterThan ?GREATER ?NUMBER)
                        (forall
                              (?ELEMENT)
                              (=>
                                    (inList
                                          ?ELEMENT
                                          (ListFn @ROW))
                                    (equal
                                          (RemainderFn ?ELEMENT ?GREATER)
                                          0)))))))