The Theory gst-sumprod
Parents
gst-fun
Constants
Σ
GS → GS
Π
GS → GS
Definitions
Σ
⊢ ∀ f
fill• fun f
fill⇒ (∀ e
fill• e ∈g Σ f
fill⇔ (∃ i v
fill• e = i ↦g v ∧ i ∈g dom f ∧ v ∈g f g i))
Π
⊢ ConstSpec
fill(λ $"Π'"
fill• ∀ f
fill• fun f
fill⇒ (∀ e
fill• e ∈g $"Π'" f
fill⇔ dom e = dom f ∧ e ⊆g Σ f))
fillΠ

up quick index

privacy policy

Created:

V