The Theory gst-fun
 Parents

 gst-ax
 Children

 gst-lists gst-rec gst-fixp gst-sumprod
 Constants
 \$ 'a GS 'a GS 'a GS snd 'a GS 'a GS fst 'a GS 'a GS \$ 'a GS 'a GS 'a GS \$ 'a GS 'a GS 'a GS rel 'a GS BOOL \$o 'a GS 'a GS 'a GS dom 'a GS 'a GS ran 'a GS 'a GS field 'a GS 'a GS fun 'a GS BOOL \$ 'a GS 'a GS 'a GS \$ 'a GS 'a GS 'a GS \$g ('a GS 'a GS) 'a GS 'a GS \$g 'a GS 'a GS 'a GS id 'a GS 'a GS
 Fixity

 Binder: g Infix 240: Infix 250: o g
 Definitions
 s t u v s t = u v s = u t = v fst snd s t fst (s t) = s snd (s t) = t s t e e s t ( l r l s r t e = l r) s t s t = (s t) rel x rel x ( y y x ( s t y = s t)) o f g f o g = Image ( p fst (fst p) snd (snd p)) (Sep (g f) ( p snd (fst p) = fst (snd p))) dom x dom x = Image fst x ran x ran x = Image snd x field s e e field s e dom s e ran s fun x fun x rel x ( s t u s u x s t x u = t) s t s t = Sep (s t) fun s t s t = Sep (s t) ( r dom r = s) g f s \$g f s = Sep (s Image f s) ( p snd p = f (fst p)) g f x f g x = (if y x y f then y x y f else f) id s id s = Sep (s s) ( x fst x = snd x)
 Theorems
 fs_thm s t p p s t fst p snd p = p v_thm p s t p s t fst p s snd p t _thm l r s t l r s t l s r t _thm s t r r s t r s t _thm s t s t fs_thm1 p r s t p r r s t fst p snd p = p _thm p r s t p r r s t fst p s snd p t rel__thm rel dom__thm dom = ran__thm ran = field__thm field = fun__thm fun _thm s t s t _thm s t f f s t _thm s t t _thm s t ( x x t) ( f f s t) app_thm1 f x (1 y x y f) x f g x f app_thm2 f x y fun f x y f f g x = y g_thm f s t u f s t u dom f f g u t g_thm1 f s t u f s t u s f g u t _thm f s t u f s t f dom f t id_thm1 s x x id s ( y y s x = y y) id_ap_thm s x x s id s g x = x id_thm1 s t u s t u id s t u id_thm2 s t u s t id s t t