| Parents |
| gst-fun |
| Constants |
|
bnd_mono
|
GS  (GS GS) BOOL
|
|
closed
|
GS (GS GS) BOOL
|
|
fixed_point
|
GS (GS GS) BOOL
|
|
least_closed
|
GS GS (GS GS) BOOL
|
|
iclosed
|
GS (GS GS) GS
|
|
lfp
|
GS (GS GS) GS
|
| Definitions |
|
bnd_mono
|
  D h   bnd_mono D h  h D  g D  ( x y x g y y g D  h x g h y)
|
|
closed
|
A h closed A h h A g A
|
|
fixed_point
|
A h fixed_point A h A = h A
|
|
least_closed
|
D A h least_closed D A h A g D closed A h ( B B g D closed B h A g B)
|
|
iclosed
|
D h iclosed D h =  g (Sep ( g D) ( X h X g X))
|
|
lfp
|
D h bnd_mono D h lfp D h g D fixed_point (lfp D h) h least_closed D (lfp D h) h
|
| Theorems |
|
bnd_monoI
|
D h h D g D ( W X W g D X g D W g X h W g h X) bnd_mono D h
|
|
bnd_monoD1
|
D h bnd_mono D h h D g D
|
|
bnd_monoD2
|
D h bnd_mono D h W g X X g D h W g h X
|
|
bnd_mono_subset
|
D h bnd_mono D h X g D h X g D
|
|
bnd_mono_
 g |
D A B h bnd_mono D h A g D B g D h A g h B g h (A g B)
|
|
def_lfp_subset
|
A D h A = iclosed D h A g D
|
|
lfp_greatest
|
A D h h D g D ( X h X g X X g D A g X) A g iclosed D h
|
|
lfp_lemma1
|
A D h bnd_mono D h h A g A A g D h (iclosed D h) g A
|
|
lfp_lemma2
|
A D h bnd_mono D h h (iclosed D h) g iclosed D h
|
|
lfp_lemma3
|
A D h bnd_mono D h iclosed D h g 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 g D fixed_point A h least_closed D A h)
|
|
lfp_subset
|
D h bnd_mono D h lfp D h g 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 g A A g D lfp D h g A)
|
|
Collect_is_pre_fixedpt
|
D h p
bnd_mono D h ( x x  g 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 g h (Sep (lfp D h) p) p x) a g lfp D h p a
|
