Specification map-maplet

[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-sep
with
   functions 
       . => . : A × B → Map[A, B] → Bool prio 11 right;
       _∃ . : (C → Map[A, B] → Bool) → Map[A, B] → Bool;
       _∃ . : (C × D → Map[A, B] → Bool) → Map[A, B] → Bool;
   
   variables 
       cP : C → Map[A, B] → Bool;
       cdP : C × D → Map[A, B] → Bool;
       hP : Map[A, B] → Bool;
       h : Map[A, B];
       o : B;
       c : C;
       d : D;
       r : A;
   
   
   axioms 
      ex: (_∃ cP)(h) ↔ (∃ c. cP(c)(h));
      used for: s, ls;
      
      ex2: (_∃ cdP)(h) ↔ (∃ c, d. cdP(c, d)(h));
      used for: s, ls;
      
      maplet: (r => o)(h) ↔ h = ∅(r := o);
      used for: ls, ss;
   
   
end enrich