actualize store-union with volid , nat by morphism :elem → volid; :data → nat; :store → vtbl; ∅ → ∅; [ ] → [ ]; # → #; -- → --; ∪ → ∪; ∈ → ∈; ⊆ → ⊆; ⊥ → ⊥; st → vtbl; st0 → vtbl0; st1 → vtbl1; st2 → vtbl2; a → v; b → v1; c → v2; d → n2; d0 → n3; d1 → n4; d2 → n5; [ ] → [ ] end actualize