@[reducible, inline]

abbrev DY.Kleene.Set (α : Type u) : Type u

Equations

• DY.Kleene.Set α = (α → Prop)

@[instance_reducible]

instance DY.Kleene.instHasSubsetSet {α : Type u_1} : HasSubset (Set α)

Equations

• DY.Kleene.instHasSubsetSet = { Subset := fun (set1 set2 : DY.Kleene.Set α) => ∀ (x : α), set1 x → set2 x }

def DY.Kleene.Chain (α : Type u) : Type u

Equations

• DY.Kleene.Chain α = (Nat → DY.Kleene.Set α)

def DY.Kleene.Chain.IsDirected {α : Type u} (chain : Chain α) : Prop

Equations

• chain.IsDirected = ∀ (i j : Nat), i ≤ j → chain i ⊆ chain j

def DY.Kleene.Chain.union {α : Type u_1} (chain : Chain α) : Set α

Equations

• chain.union x = ∃ (n : Nat), chain n x

def DY.Kleene.Chain.map {α : Type u_1} (f : Set α → Set α) (chain : Chain α) : Chain α

Equations

• DY.Kleene.Chain.map f chain n x = f (chain n) x

def DY.Kleene.IsScottContinuous {α : Type u} (f : Set α → Set α) : Prop

Equations

• DY.Kleene.IsScottContinuous f = ∀ (chain : DY.Kleene.Chain α), chain.IsDirected → f chain.union = (DY.Kleene.Chain.map f chain).union

def DY.Kleene.mkWeakestFixpoint {α : Type u} (f : Set α → Set α) : Set α

Equations

• DY.Kleene.mkWeakestFixpoint f = (DY.Kleene.mkWeakestFixpointAux✝ f).union

theorem DY.Kleene.mkWeakestFixpoint_is_fixpoint {α : Type u} (f : Set α → Set α) (h_scott : IsScottContinuous f) : f (mkWeakestFixpoint f) = mkWeakestFixpoint f

theorem DY.Kleene.mkWeakestFixpoint_is_weakest {α : Type u} (f : Set α → Set α) (h_scott : IsScottContinuous f) (set : Set α) : f set ⊆ set → mkWeakestFixpoint f ⊆ set

def DY.Kleene.combine {α : Type u} {Id : Type} (fs : Id → Set α → Set α) (set : Set α) : Set α

Equations

• DY.Kleene.combine fs set x = ∃ (id : Id), fs id set x

theorem DY.Kleene.combine_isScottContinuous {α : Type u} {Id : Type} (fs : Id → Set α → Set α) (h_fs : ∀ (id : Id), IsScottContinuous (fs id)) : IsScottContinuous (combine fs)

def DY.Kleene.Forall {α : Type u} (p : α → Prop) (l : List α) : Prop

Equations

• DY.Kleene.Forall p l = ∀ (x : α), x ∈ l → p x

theorem DY.Kleene.isScottContinuous_Forall_lemma {α : Type u} (chain : Chain α) (h_chain : chain.IsDirected) (l : List α) : Forall chain.union l = ∃ (n : Nat), Forall (chain n) l