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 
       . ^ . : ((elem → bool) → elem → bool) × nat → (elem → bool) → elem → bool;
   
   predicates 
       ∅ : elem;
       cont : ((elem → bool) → elem → bool);
       chain : (nat → elem → bool);
   
   variables 
       chn : nat → elem → bool;
       iset : elem → bool;
       m : nat;
       n : nat;
       f : (elem → bool) → elem → bool;
       x : elem;
   
   
   axioms 
      empty-def: ¬ ∅(x);
      used for: s, ls;
      
      chain-def: chain(chn) ↔ (∀ m, n. chn(m) ⊆ chn(n) ∨ chn(n) ⊆ chn(m));
      
      iterate-base: ((f ^ 0))(iset) = iset;
      used for: s, ls;
      
      iterate-rec: ((f ^ (n + 1)))(iset) = f(((f ^ n))(iset));
      used for: s, ls;
      
      cont-def: cont(f) ↔ (∀ chn. chain(chn) → (∀ x. f(λ x0. ∃ n. chn(n)(x0))(x) ↔ (∃ n. f(chn(n))(x))));
   
   
end enrich