The Theory gst-fixp
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
fill• bnd_mono D h
fill⇔ h D ⊆g D
fill∧ (∀ 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
fill• least_closed D A h
fill⇔ A ⊆g D
fill∧ closed A h
fill∧ (∀ B• B ⊆g D ∧ closed B h ⇒ A ⊆g B)
iclosed
⊢ ∀ D h
fill• iclosed D h = ⋂g (Sep (℘g D) (λ X• h X ⊆g X))
lfp
⊢ ∀ D h
fill• bnd_mono D h
fill⇒ lfp D h ⊆g D
fill∧ fixed_point (lfp D h) h
fill∧ least_closed D (lfp D h) h
Theorems
bnd_monoI
⊢ ∀ D h
fill• h D ⊆g D
fill∧ (∀ W X
fill• W ⊆g D ∧ X ⊆g D ∧ W ⊆g X ⇒ h W ⊆g h X)
fill⇒ 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
fill• bnd_mono D h ∧ A ⊆g D ∧ B ⊆g D
fill⇒ 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
fill• h D ⊆g D ∧ (∀ X• h X ⊆g X ∧ X ⊆g D ⇒ A ⊆g X)
fill⇒ A ⊆g iclosed D h
lfp_lemma1
⊢ ∀ A D h
fill• bnd_mono D h ∧ h A ⊆g A ∧ A ⊆g D
fill⇒ h (iclosed D h) ⊆g A
lfp_lemma2
⊢ ∀ A D h
fill• bnd_mono D h ⇒ h (iclosed D h) ⊆g iclosed D h
lfp_lemma3
⊢ ∀ A D h
fill• 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
fill• bnd_mono D h
fill⇒ (∃ A
fill• 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
fill• bnd_mono D h
fill⇒ (∀ A X• h A ⊆g A ∧ A ⊆g D ⇒ lfp D h ⊆g A)
Collect_is_pre_fixedpt
⊢ ∀ D h p
fill• bnd_mono D h
fill∧ (∀ x• x ∈g h (Sep (lfp D h) p) ⇒ p x)
fill⇒ closed (Sep (lfp D h) p) h
induct
⊢ ∀ D h p a
fill• bnd_mono D h
fill∧ (∀ x• x ∈g h (Sep (lfp D h) p) ⇒ p x)
fill∧ a ∈g lfp D h
fill⇒ p a

up quick index

privacy policy

Created:

V