zui4 da4 gong1 yue1 shu4 han2 shu4 (GreatestCommonDivisorFn)

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

Ontology

SUMO / NUMERIC-FUNCTIONS

Class(es)

zhong3 lei4

ke3 ji4 cheng2 guan1 xi4

han2 shu4

bian4 yi4 yuan2 shu4 guan1 xi4
is instance of

zui4 da4 gong1 yue1 shu4 han2 shu4

Coordinate term(s)

zhi3 ding4 han2 shu4 zui4 xiao3 gong1 bei4 shu4 han2 shu4 xu4 lie4 han2 shu4 mao2 dun4 shu3 xing4 wu2 jiao1 ji2 fen1 jie3 wu2 jiao1 ji2 guan1 xi4 qiong2 jin4 de5 shu3 xing4 qiong2 jin4 de5 fen1 jie3 cheng2 li4 fen1 ge1

Axioms (2)

if " de5 zui4 da4 gong1 yue1 shu4" deng3 yu1 number,
then for all element holds: if element shi4 "()" de5 yi1 cheng2 yuan2, then "element qu3 yu2 shu4 number" deng3 yu1

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

if " de5 zui4 da4 gong1 yue1 shu4" deng3 yu1 number,
then there doesn't exist greater so_that_not greater (bu2) da4 yu1 number and for all element holds: if element shi4 "()" de5 yi1 cheng2 yuan2, then "element qu3 yu2 shu4 greater" deng3 yu1

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