[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 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; => → ==> prio 16; =>_ → ==>_; =>? → ==>?; ++ → ++; -- → --; [ ] → [ ]; # → #; ∪ → ∪; \ → \; 
          \ → \; * → *; ⊗ → ⊗; -* → -*; -⊗ → -⊗; ¬ → ¬; ∧ → ∧; ∨ → ∨; → → →; ⌜ ⌝ → ⌜ ⌝; { } → { }; _∃ → _∃; _∃ → _∃; _∃ → _∃; 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