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