Specification forall-indexWhere

[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
   filter-count
with
   functions 
       . indexWhere ( . ) : List[A] × (A → Bool) → Nat;
   
   predicates 
       . forall ( . ) : List[A] × (A → Bool);
       . exists ( . ) : List[A] × (A → Bool);
   
   variables 
       p : A → Bool;
       x : List[A];
       a : A;
   
   axioms 
      forall-base: [].forall(p);
      used for: s, ls;
      
      forall-rec: (a ' + x).forall(p) ↔ p(a) ∧ x.forall(p);
      used for: s, ls;
      
      exists-base: ¬ [].exists(p);
      used for: s, ls;
      
      exists-rec: (a ' + x).exists(p) ↔ p(a) ∨ x.exists(p);
      used for: s, ls;
      
      indexWhere-base: [].indexWhere(p) = 0;
      used for: s, ls;
      
      indexWhere-rec1: p(a) → (a ' + x).indexWhere(p) = 0;
      used for: s, ls;
      
      indexWhere-rec2: ¬ p(a) → (a ' + x).indexWhere(p) = 1 + x.indexWhere(p);
      used for: s, ls;
   
   
end enrich