Specification approx-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,

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