[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,

Specification heap-aux-inst
instantiate parameter
   obj
< 
   heap-fun
with 
   obj-aux

   
by mapping
      : obj → objaux
   rename 
      :heap → heap-aux; 
      ∅ → ∅; 
      => → __=>; 
      =>_ → ==>_; 
      =>? → ==>?; 
      ] → [ ]__; 
      ] → [ ]__; 
      mk → __mk; 
      _∃ → __∃; 
      ++ → ++; 
      -- → --; 
      # → #; 
      ∪ → ∪; 
      \ → \; 
      \ → \; 
      dom → dom; 
      * → *; 
      ⊗ → ⊗; 
      -* → -*; 
      -⊗ → -⊗; 
      ¬ → ¬; 
      ∧ → ∧; 
      ∨ → ∨; 
      → → →; 
      ⌜ ⌝ → ⌜ ⌝; 
      { } → { }; 
      ite → ite; 
      _∃ → _∃; 
      _∃ → _∃; 
      ] → [ ]__; 
      ∈ → ∈; 
      ⊆ → ⊆; 
      ⊥ → ⊥; 
      emp → emp; 
      true → true; 
      false → false; 
      precise → precise; 
      ⊆ → ⊆
end instantiate