The Theory gst-fixp
Parents

gst-fun
Children

gst
Constants
bnd_mono
'a GS ('a GS 'a GS) BOOL
closed
'a GS ('a GS 'a GS) BOOL
fixed_point
'a GS ('a GS 'a GS) BOOL
least_closed
'a GS 'a GS ('a GS 'a GS) BOOL
iclosed
'a GS ('a GS 'a GS) 'a GS
lfp
'a GS ('a GS 'a GS) 'a GS
Definitions
bnd_mono
D h
bnd_mono D h
h D D ( x y x y y D h x h y)
closed
A h closed A h h A A
fixed_point
A h fixed_point A h A = h A
least_closed
D A h
least_closed D A h
A D
closed A h
( B B D closed B h A B)
iclosed
D h iclosed D h = (Sep ( D) ( X h X X))
lfp
D h
bnd_mono D h
lfp D h D
fixed_point (lfp D h) h
least_closed D (lfp D h) h
Theorems
bnd_monoI
D h
h D D
( W X W D X D W X h W h X)
bnd_mono D h
bnd_monoD1
D h bnd_mono D h h D D
bnd_monoD2
D h bnd_mono D h W X X D h W h X
bnd_mono_subset
D h bnd_mono D h X D h X D
bnd_mono_
D A B h
bnd_mono D h A D B D
h A h B h (A B)
def_lfp_subset
A D h A = iclosed D h A D
lfp_greatest
A D h
h D D ( X h X X X D A X)
A iclosed D h
lfp_lemma1
A D h
bnd_mono D h h A A A D
h (iclosed D h) A
lfp_lemma2
A D h bnd_mono D h h (iclosed D h) iclosed D h
lfp_lemma3
A D h bnd_mono D h iclosed D h h (iclosed D h)
lfp_Tarski
A D h bnd_mono D h iclosed D h = h (iclosed D h)
lemp_lemma
D h bnd_mono D h least_closed D (iclosed D h) h
Tarski_thm
D h
bnd_mono D h
( A
A D fixed_point A h least_closed D A h)
lfp_subset
D h bnd_mono D h lfp D h D
lfp_fixp
D h bnd_mono D h h (lfp D h) = lfp D h
lfp_lowerbound
D h
bnd_mono D h
( A X h A A A D lfp D h A)
Collect_is_pre_fixedpt
D h p
bnd_mono D h ( x x h (Sep (lfp D h) p) p x)
closed (Sep (lfp D h) p) h
induct
D h p a
bnd_mono D h
( x x h (Sep (lfp D h) p) p x)
a lfp D h
p a

up quick index © RBJ