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