The Theory gst-fun
 Parents
 gst-ax
 Constants
 \$↦g GS → GS → GS snd GS → GS fst GS → GS \$×g GS → GS → GS \$↔g GS → GS → GS rel GS → BOOL \$og GS → GS → GS dom GS → GS ran GS → GS field GS → GS fun GS → BOOL \$g GS → GS → GS \$→g GS → GS → GS \$λg (GS → GS) → GS → GS \$g GS → GS → GS id GS → GS
 Fixity
 Binder: λg Right Infix 240: ↔g →g ×g g ↦g Right Infix 250: og g
 Definitions
 ↦g ⊢ ∀ s t u v • (s ↦g t = u ↦g v ⇔ s = u ∧ t = v) ∧ Pairg s t ∈g Gx (s ↦g t) fst snd ⊢ ∀ s t• fst (s ↦g t) = s ∧ snd (s ↦g t) = t ×g ⊢ ∀ s t e • e ∈g s ×g t ⇔ (∃ l r• l ∈g s ∧ r ∈g t ∧ e = l ↦g r) ↔g ⊢ ∀ s t• s ↔g t = ℘g (s ×g t) rel ⊢ ∀ x• rel x ⇔ (∀ y• y ∈g x ⇒ (∃ s t• y = s ↦g t)) og ⊢ ∀ f g • f og g = Imagep (λ p• fst (fst p) ↦g snd (snd p)) (Sep (g ×g f) (λ p• ∃ q r s• p = (q ↦g r) ↦g r ↦g s)) dom ⊢ ∀ x• dom x = Sep (Gx x) (λ w• ∃ v• w ↦g v ∈g x) ran ⊢ ∀ x• ran x = Sep (Gx x) (λ w• ∃ v• v ↦g w ∈g x) field ⊢ ∀ s e• e ∈g field s ⇔ e ∈g dom s ∨ e ∈g ran s fun ⊢ ∀ x • fun x ⇔ rel x ∧ (∀ s t u • s ↦g u ∈g x ∧ s ↦g t ∈g x ⇒ u = t) g ⊢ ∀ s t• s g t = Sep (s ↔g t) fun →g ⊢ ∀ s t• s →g t = Sep (s g t) (λ r• dom r = s) λg ⊢ ∀ f s • \$λg f s = Sep (s ×g Imagep f s) (λ p• snd p = f (fst p)) g ⊢ ∀ f x • f g x = (if ∃ y• x ↦g y ∈g f then ε y• x ↦g y ∈g f else f) id ⊢ ∀ s• id s = Sep (s ×g s) (λ x• fst x = snd x)
 Theorems
 f↦gs_thm ⊢ ∀ s t p• p ∈g s ×g t ⇒ fst p ↦g snd p = p v∈g×g_thm ⊢ ∀ p s t• p ∈g s ×g t ⇒ fst p ∈g s ∧ snd p ∈g t ↦g∈g×g_thm ⊢ ∀ l r s t• l ↦g r ∈g s ×g t ⇔ l ∈g s ∧ r ∈g t ↔g⊆g×g_thm ⊢ ∀ s t r• r ∈g s ↔g t ⇔ r ⊆g s ×g t ∅g∈g↔g_thm ⊢ ∀ s t• ∅g ∈g s ↔g t f↦gs_thm1 ⊢ ∀ p r s t • p ∈g r ∧ r ∈g s ↔g t ⇒ fst p ↦g snd p = p ∈g↔g_thm ⊢ ∀ p r s t • p ∈g r ∧ r ∈g s ↔g t ⇒ fst p ∈g s ∧ snd p ∈g t rel_∅g_thm ⊢ rel ∅g og_thm ⊢ ∀ f g x • x ∈g f og g ⇔ (∃ q r s • q ↦g r ∈g g ∧ r ↦g s ∈g f ∧ x = q ↦g s) og_thm2 ⊢ ∀ f g x y • x ↦g y ∈g f og g ⇔ (∃ z• x ↦g z ∈g g ∧ z ↦g y ∈g f) og_rel_thm ⊢ ∀ r s• rel r ∧ rel s ⇒ rel (r og s) og_associative_thm ⊢ ∀ f g h• (f og g) og h = f og g og h dom_∅g_thm ⊢ dom ∅g = ∅g dom_thm ⊢ ∀ r y• y ∈g dom r ⇔ (∃ x• y ↦g x ∈g r) ran_∅g_thm ⊢ ran ∅g = ∅g ran_thm ⊢ ∀ r y• y ∈g ran r ⇔ (∃ x• x ↦g y ∈g r) rel_sub_cp_thm ⊢ ∀ x• rel x ⇔ (∃ s t• x ⊆g s ×g t) field_∅g_thm ⊢ field ∅g = ∅g fun_∅g_thm ⊢ fun ∅g og_fun_thm ⊢ ∀ f g• fun f ∧ fun g ⇒ fun (f og g) ran_og_thm ⊢ ∀ f g• ran (f og g) ⊆g ran f dom_og_thm ⊢ ∀ f g• dom (f og g) ⊆g dom g dom_og_thm2 ⊢ ∀ f g• ran g ⊆g dom f ⇒ dom (f og g) = dom g ∅g∈gg_thm ⊢ ∀ s t• ∅g ∈g s g t ∃g_thm ⊢ ∀ s t• ∃ f• f ∈g s g t ∅g∈g∅g→g_thm ⊢ ∀ s t• ∅g ∈g ∅g →g t ∃→g_thm ⊢ ∀ s t• (∃ x• x ∈g t) ⇒ (∃ f• f ∈g s →g t) app_thm1 ⊢ ∀ f x• (∃1 y• x ↦g y ∈g f) ⇒ x ↦g f g x ∈g f app_thm2 ⊢ ∀ f x y• fun f ∧ x ↦g y ∈g f ⇒ f g x = y app_thm3 ⊢ ∀ f x• fun f ∧ x ∈g dom f ⇒ x ↦g f g x ∈g f og_g_thm ⊢ ∀ f g x • fun f ∧ fun g ∧ x ∈g dom g ∧ ran g ⊆g dom f ⇒ (f og g) g x = f g g g x g∈g_thm ⊢ ∀ f s t u• f ∈g s g t ∧ u ∈g dom f ⇒ f g u ∈g t g∈g_thm1 ⊢ ∀ f s t u• f ∈g s →g t ∧ u ∈g s ⇒ f g u ∈g t ∈gg⇒∈g→g_thm ⊢ ∀ f s t u• f ∈g s g t ⇒ f ∈g dom f →g t id_thm1 ⊢ ∀ s x• x ∈g id s ⇔ (∃ y• y ∈g s ∧ x = y ↦g y) id_ap_thm ⊢ ∀ s x• x ∈g s ⇒ id s g x = x id∈gg_thm1 ⊢ ∀ s t u• s ⊆g t ∩g u ⇒ id s ∈g t g u id∈gg_thm2 ⊢ ∀ s t u• s ⊆g t ⇒ id s ∈g t g t id_clauses ⊢ ∀ s • rel (id s) ∧ fun (id s) ∧ dom (id s) = s ∧ ran (id s) = s