[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
instantiate parameter
   obj
< 
   heap-fun
with 
   gobj, 
   gaux

   
by mapping
      : obj → obj × aux; 
      o → o, a; 
      o0 → o0, a0; 
      o1 → o1, a1
   rename 
      :heap → heap-aux; 
      ∅ → ∅; 
      ] → [ ]o, [ ]a; 
      => → ==>; 
      =>_ → ==>_; 
      =>? → ==>?; 
      ++ → ++; 
      -- → --; 
      [ ] → [ ]; 
      # → #; 
      ∪ → ∪; 
      \ → \; 
      \ → \; 
      * → *; 
      ⊗ → ⊗; 
      -* → -*; 
      -⊗ → -⊗; 
      ¬ → not; 
      ∧ → and; 
      ∨ → or; 
      → → ->; 
      ⌜ ⌝ → ⌜ ⌝; 
      { } → { }; 
      ite → ite; 
      _∃ → _∃; 
      _∃ → _∃; 
      _∃ → _∃; 
      mk → mk; 
      ∈ → ∈; 
      ⊆ → ⊆; 
      ⊥ → ⊥; 
      emp → emp; 
      true → true; 
      false → false; 
      precise → precise; 
      ⊆ → ⊆; 
      [ ] → [ ]; 
      H → Ha; 
      H0 → Ha0; 
      H1 → Ha1; 
      H2 → Ha2; 
      P → R; 
      P0 → R0; 
      P1 → R1; 
      P2 → R2; 
      rP → rR; 
      rrP → rrR; 
      oP → oR; 
      f → f, g
end instantiate