Constant | Type |
---|---|
gcdset | :(num -> bool) -> num |
|- ∀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})
|- ∀e. e ∈ s ⇒ divides (gcdset s) e
|- (∀e. e ∈ s ⇒ divides g e) ⇒ divides g (gcdset s)
|- gcdset ∅ = 0
|- gcdset (x INSERT s) = gcd x (gcdset s)