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