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