| 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) Pair 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 p fst (fst p) g snd (snd p)) 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 g Imagep f s) ( p snd p = f (fst p))
|
|
g
|
f x f g x y x g y g f y x g y g 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 g g_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
|
g g![]() 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
g g_thm1
|
s t u s g t g u id s g t g u
|
|
id
g g_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
|