Specification monotone-set-fixpoint

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

specification
   functions 
       UN : ((A → Bool) → Bool) → A → Bool;
       IS : ((A → Bool) → Bool) → A → Bool;
       compl : ((A → Bool) → A → Bool) → (A → Bool) → A → Bool;
      comment: compl(f)(S) = X \ f(X \ S);
   
   predicates 
       . ⊆ . : (A → Bool) × (A → Bool);
       monotone : ((A → Bool) → A → Bool);
   
   variables 
       x : A;
       x0 : A;
       x1 : A;
       iset : A → Bool;
       iset0 : A → Bool;
       iset1 : A → Bool;
       f : (A → Bool) → A → Bool;
       isetset : (A → Bool) → Bool;
   
   partial functions 
       μ : ((A → Bool) → A → Bool) → A → Bool with λ f. λ x. monotone(f);
       ν : ((A → Bool) → A → Bool) → A → Bool with λ f. λ x. monotone(f);
   axioms 
      union-def: UN(isetset)(x) ↔ (∃ iset. isetset(iset) ∧ iset(x));
      
      intersection-def: IS(isetset)(x) ↔ (∀ iset. isetset(iset) → iset(x));
      
      subseteq-def: iset ⊆ iset0 ↔ (∀ x. iset(x) → iset0(x));
      
      monotone-def: monotone(f) ↔ (∀ iset, iset0. iset ⊆ iset0 → f(iset) ⊆ f(iset0));
      
      least-prefixpoint-def: monotone(f) → (μ(f)(x) ↔ (∀ iset. f(iset) ⊆ iset → iset(x)));
      
      greatest-prefixpoint-def: monotone(f) → (ν(f)(x) ↔ ¬ μ(compl(f))(x));
      
      compl-def: compl(f)(iset)(x) ↔ ¬ f(λ x0. ¬ iset(x0))(x);
   
end specification