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