greatest common divisor fn (GreatestCommonDivisorFn)

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

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

class

inheritable relation

function

variable arity relation
is instance of

greatest common divisor fn

Coordinate term(s)

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

Axioms (2)

if "the greatest common divisor of " is equal to number,
then for all element holds: if element is a member of "()", then "element mod number" is equal to

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

if "the greatest common divisor of " is equal to number,
then there doesn't exist greater so that greater is greater than number and for all element holds: if element is a member of "()", then "element mod greater" is equal to

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