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
$o_g	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:

o_g

_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))
o_g	f g f o_g 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
o_g_thm	f g x x _g f o_g g ( q r s q _g r _g g r _g s _g f x = q _g s)
o_g_thm2	f g x y x _g y _g f o_g g ( z x _g z _g g z _g y _g f)
o_g_rel_thm	r s rel r rel s rel (r o_g s)
o_g_associative_thm	f g h (f o_g g) o_g h = f o_g g o_g 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
o_g_fun_thm	f g fun f fun g fun (f o_g g)
ran_o_g_thm	f g ran (f o_g g) _g ran f
dom_o_g_thm	f g dom (f o_g g) _g dom g
dom_o_g_thm2	f g ran g _g dom f dom (f o_g 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 (₁ 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
o_g__g_thm	f g x fun f fun g x _g dom g ran g _g dom f (f o_g 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

V