Theory "gcdset"

Parents pred_set gcd

Signature

Constant	Type
gcdset	:(num -> bool) -> num

Definitions

gcdset_def

⊢ ∀s.
      gcdset s = if s = ∅ ∨ s = {0} then 0
      else
        MAX_SET
          ({n | n ≤ MIN_SET (s DELETE 0)} ∩ {d | ∀e. e ∈ s ⇒ divides d e})

Theorems

gcdset_divides

⊢ ∀e. e ∈ s ⇒ divides (gcdset s) e

gcdset_greatest

⊢ (∀e. e ∈ s ⇒ divides g e) ⇒ divides g (gcdset s)

gcdset_EMPTY

⊢ gcdset ∅ = 0

gcdset_INSERT

⊢ gcdset (x INSERT s) = gcd x (gcdset s)