Specification assoclist

[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
   assoclista
with
   

   
   
   functions  . [ . ] : assoclist × elem → data;
              . [ . ] : assoclist × data → elem;
              . [ . ] : assoclist × elem × data → assoclist;
   predicates  . ∈ . : elem × assoclist;
               unique_al : assoclist;
   
   
   
   

   

   axioms assoc-yes :  ⊦ ((a × d)' + ax)[a] = d;
          used for: s, ls;
          assoc-no :  ⊦ a ≠ b → ((b × d)' + ax)[a] = ax[a];
          used for: s, ls;
          rassoc-yes :  ⊦ ((a × d)' + ax)[d] = a;
          used for: s, ls;
          rassoc-no :  ⊦ d ≠ d0 → ((a × d0)' + ax)[d] = ax[d];
          used for: s, ls;
          inassoc :  ⊦ a ∈ ax ↔ (∃ d. a × d ∈ ax);
          used for: ls;
          put-empty :  ⊦ ([])[a, d] = (a × d)';
          used for: s, ls;
          put-yes :  ⊦ ((a × d0)' + ax)[a, d] = (a × d)' + ax;
          used for: s, ls;
          put-no :  ⊦ a ≠ b → ((b × d0)' + ax)[a, d] = (b × d0)' + ax[a, d];
          used for: s, ls;
          unique-e :  ⊦ unique_al([]);
          used for: s, ls, nokodkodax;
          unique-r :  ⊦ unique_al((a × d) + ax) ↔ ¬ a ∈ ax ∧ unique_al(ax);
          used for: s, ls, nokodkodax;

   

   
end enrich