namespace http://mathhub.info/MitM/core/numbertheory ❚

import base http://mathhub.info/MitM/Foundation ❚
import sets http://mathhub.info/MitM/core/typedsets ❚

theory AdditiveBases : base:?Logic =
    include ☞sets:?FiniteSets ❙
    include ☞sets:?SetQuantifiers ❙
    include ☞sets:?LeastMost ❙
    include ?NatIntervals ❙

    isAdditiveBasisFor : set ℕ ⟶ set ℕ ⟶ prop ❘
        = [A,T] ∀ ∈ T . [t] ∃ ∈ A . [a1] ∃ ∈ A . [a2] a1 + a2 ≐ t ❙

    isRestrictedAdditiveBasisFor : set ℕ ⟶ set ℕ ⟶ prop ❘
       = [A,T] (isAdditiveBasisFor A T) ∧ (∀ ∈ A . [x:ℕ] ∀ ∈ T . [y:ℕ] (2 ⋅ x) ≤ y) ∧
          ∃ [b] T ≐ natInterval 0 b ❙

    include ☞sets:?LeastMost ❙

    isSymmetricAdditiveBasis : set ℕ ⟶ set ℕ ⟶ prop ❙
        // = [A,T] (isAdditiveBasisFor A T) ∧ ∀ ∈ A . [a] ((greatest ([x:ℕ] x ∈ A) ([x:ℕ,y:ℕ] x ≤ y) - a) ∈ A) ❙
❚