[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 approx-fixpoint
enrich
   monotone-set-fixpoint, 
   nat
with
   functions 
       . ^ . : ((A → Bool) → A → Bool) × Nat → (A → Bool) → A → Bool;
   
   predicates 
       cont : ((A → Bool) → A → Bool);
       chain : (Nat → A → Bool);
   
   variables 
       chn : Nat → A → Bool;
       iset : A → Bool;
       m : Nat;
       n : Nat;
       f : (A → Bool) → A → Bool;
       x : A;
   
   axioms 
      chain-def: chain(chn) ↔ (∀ m, n. chn(m) ⊆ chn(n) ∨ chn(n) ⊆ chn(m));
      
      iterate-base: (f ^ 0)(iset) = iset;
      
      iterate-rec: (f ^ (n + 1))(iset) = f((f ^ n)(iset));
      
      cont-def: cont(f) ↔ (∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))));
   
   
end enrich