Specification map-ops

[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
   map+set
with
   functions 
       . map ( . ) : Map[A, B] × (B → C) → Map[A, C];
       . map ( . ) : Map[A, B] × (A × B → C) → Map[A, C];
       . filter ( . ) : Map[A, B] × (A × B → Bool) → Map[A, B];
       . filter ( . ) : Map[A, B] × (A → Bool) → Map[A, B];
   
   predicates 
       . forall ( . ) : Map[A, B] × (A × B → Bool);
       . forall ( . ) : Map[A, B] × (A → Bool);
       . exists ( . ) : Map[A, B] × (A × B → Bool);
       . exists ( . ) : Map[A, B] × (A → Bool);
   
   variables 
       f : B → C;
       g : A × B → C;
       a : A;
       b : B;
       c : C;
       p : A → Bool;
       q : A × B → Bool;
   
   axioms 
      forallk-base: ∅.forall(p);
      
      forallk-rec: ¬ a ∈ st → (st(a := b).forall(p) ↔ st.forall(p) ∧ p(a));
      
      forallkv-base: ∅.forall(q);
      
      forallkv-rec: ¬ a ∈ st → (st(a := b).forall(q) ↔ st.forall(q) ∧ q(a, b));
      
      existsk-base: ∅.exists(p);
      
      existsk-rec: ¬ a ∈ st → (st(a := b).exists(p) ↔ st.exists(p) ∨ p(a));
      
      existskv-base: ∅.exists(q);
      
      existskv-rec: ¬ a ∈ st → (st(a := b).exists(q) ↔ st.exists(q) ∨ q(a, b));
      
      map-in: a ∈ st.map(f) ↔ a ∈ st;
      used for: s, ls;
      
      map-at: a ∈ st → st.map(f)(a) = f(st(a));
      used for: ls;
      
      mapi-in: a ∈ st.map(g) ↔ a ∈ st;
      used for: s, ls;
      
      mapi-at: a ∈ st → st.map(g)(a) = g(a, st(a));
      used for: ls;
   
   
end enrich