ValuedCSP.Term.inΓ

theorem ValuedCSP.Term.inΓ : ∀ {D : Type u_1} {C : Type u_2} [inst : OrderedAddCommMonoid C] {Γ : ValuedCSP D C} {ι : Type u_3} (self : Γ.Term ι), ⟨self.n, self.f⟩ ∈ Γ

The theorem `ValuedCSP.Term.inΓ` states that for any given types `D` and `C`, where `C` is an ordered additive commutative monoid, and any valued constraint satisfaction problem (CSP) `Γ` over domain `D` with costs in `C`, for any term `self` of `Γ`, the pair consisting of `self.n` and `self.f` is an element of `Γ`. Here, `self.n` is a natural number and `self.f` is a cost function from finite sequences of elements of `D` of length `self.n` to `C`. In other words, the cost function of any term in a valued CSP comes from the CSP's template.

More concisely: For any valued constraint satisfaction problem (CSP) Γ over domain D with costs in an ordered additive commutative monoid C, the cost function of each term (n, f) in Γ is an element of Γ, where n is a natural number and f is a function from finite sequences of length n in D to C.