greatest common divisor fn (GreatestCommonDivisorFn)

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

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

Classe

inheritable relation

Funzione

RelazioneAdAritáVariabile
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)

se "il massimo comune divisore di" is uguale a number,
allora per ogni element vale: se element é un é membro di "(", allora "element mod number" is uguale a

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

se "il massimo comune divisore di" is uguale a number,
allora non esiste greater tale che greater é più grande di number e per ogni element vale: se element é un é membro di "(", allora "element mod greater" is uguale a

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